Okay, not the results I would have expected.

I figured this one would be the most difficult.

Interesting.

Should we go over them or are we fine?

Fair enough.

Yes, right, with a small enough number of students that is actually possible, yes.

I did not think of that.

Okay, I think this one is pretty clear, right?

Conjunction is like product types and product types consist of pairs.

Interesting, why is this one colored and this one, okay.

Universal quantifier is dependent function types and dependent function types are lambda

expressions, i.e. functions.

Universal quantifier is dependent product types, sigma types, and populated by pairs,

dependent pairs, and then there is this one.

And the reason why I figured it would be easiest is if you've done all the stuff before, then

you can now basically just look at this thing and realize, okay, this needs to be a dependent

function.

Implication is a simple function.

Existential is now a sigma type and conjunction is a product.

And then you know, okay, so this needs to be a function.

We have an implication, so we need another function, so another lambda.

Then an existential needs to be a pair, okay, so here we have a pair.

And then we have a conjunction, so another pair.

So it has to be the third one because that's the only one where lambdas and open angle

brackets actually match the proposition out there.

Does that make sense?

Okay.

Then I'm going to spend another, let's say, half an hour at most and tell you some more

fun things.

And after that, we can just go over everything and do some kind of inventory on what is actually

important and to what extent and so on and so forth.

Okay, so we've done Curry-Howard now, which basically means we have for every syntactic

constructor or quantifier of basically higher order logic, we have some corresponding type

constructor.

Notably, for implications, we have simple function types.

For universal quantifiers, we have dependent function types.

We have an empty type, which also gives us negation.

With an empty type, we can also define true.

We can define conjunction as product types.

We have sigma types to get at existentials.

Then there's co-product types, which correspond to disjunctions.

That basically means for every high order logical proposition, we can build a type in

Martin-Loev type theory that corresponds to that proposition.

Now the way that we do things here is that for literally every syntactic construct, we

introduce a dedicated type constructor, or kind of types, like dependent function types,

sigma types, and so on and so forth.

Once we've done all of that, one thing we can do is realize why do we even need to do

that?

If we have type constructors and we can quantify over enough types, then all we need is some

operator that takes a judgment of the logic that we want to model, like for example, higher