trying to explain intuitionistic logic to students...
Came to a conclusion that it may be easier to use the idea of "evidences"; e.g. a truth table is an evidence; a proof is an evidence; but then we basically have a topos below (an evidence of a conjunction is a tuple, and an evidence of an implication is a function).
So, it's a type theory.
So, it's a type theory.