[PL-sem-jr] Aug 13th Summary + Chap 2.7 for Aug 20th

[Julia Belyakova]

Dear all,

Today we went through sections 2.4 and 2.5 (products and examples).
Next time, we'll start with 2.7.

We left wondering about "Curry-Howard non-isomorphism" (the book claims
there is a functor from the category of proofs to the category of types,
but not an isomorphism unless extra restrictions are imposed).
It appears that the category of types has a lot of equivalences between
terms, i.e. beta-eta equivalent terms correspond to the same arrow. This,
in particular, is important for the uniqueness of identity. But in the
category of proofs, different proofs of the same proposition represent
different arrows. Can we not build multiple identities then? Hmm.

--
Kind regards, Julia
-------------- next part --------------
HTML attachment scrubbed and removed