Now I do see the pictures. (but this is a different computer)
slide 11 - thank you for the pullback diagram! It really clarified it for me. (even though three more arrows are missing, and the definition of the pullback, too)
slide 16 - Disjunction diagram is a bit unexpected - U was not introduced.
slide 15: I do get the idea (p1 and ∈ interpret A×AA (can't use A, because ∈ codomain is Ω) Ω×ΩΩ in an incompatible manner, so there is no Equalizer for this pair, so the type of Equalizers for this pair is empty), but the types are still not right (and I am not sure what the diagram shows).
no subject
slide 11 - thank you for the pullback diagram! It really clarified it for me. (even though three more arrows are missing, and the definition of the pullback, too)
slide 16 - Disjunction diagram is a bit unexpected - U was not introduced.
slide 15: I do get the idea (p1 and ∈ interpret
A×AA(can't use A, because ∈ codomain is Ω) Ω×ΩΩ in an incompatible manner, so there is no Equalizer for this pair, so the type of Equalizers for this pair is empty), but the types are still not right (and I am not sure what the diagram shows).