• We start with the concept of „Propositions as types“, and what that is all about.
  • The idea is that we can think of a proposition that is satisfiable as a type that can be inhibited.
• Can I give an example?
  • The first one that comes to my mind is that function type (A →

B) correspond to logical implication (ϕ → ψ).

• There is a simpler example?
  • The next one that comes to mind is that the pair type (A \times B) corresponds logical conjunction (ϕ ∧ ψ).
• Even simpler!
  • How about the correspondence between the empty type (⊥) and falsum or the unit type (⊤) and truth?
    • This is what he wanted to hear?

• What to dependent pairs (Π) and dependent sums (Σ) correspond to?
  • Universal and existential quantification. I also add that the thing about existential quantification in constructive logic is that it requires a witness to prove the quantified statement, and this is the first element of the pair.
• Can I show how to create a disjunct union (coproducts, \uplus) using a dependent pair?
  • I misunderstand the question and write down how to create an (independent) product „∃ A (λ _ . B)“, but quickly notice that I was mistaken and write down „∃ Bool (λ b . if b then A else B)“
• Can I show how to create a pair (\times) using a dependent pair?
  • I point to my mistaken previous definition for disjunct unions, but there was some misunderstanding and my answer was not accepted. I insisted in confusion that this should be the solution, and after a moment the confusion is resolved.

• What is MLTT all about?
  • What do you mean?
  • I try to remember the HOTT slides but cannot recall everything correctly.
• How many rules are there?
  • The answer 5 is wrong
• Can I give the rules for contex construction.
  • I fail to guess what he is talking about.

(The following is what the MLTT chapter was supposed to be about, from what a friend told me)

• What is MLTT?
  • It is a formal system.
• What are the „ingredients“?
  1. Terms which also serve as types
  2. Typing judgements
  3. Judgemental equality
  4. Contexts and well-formed context judgements
• What is the elimination rule for the bottom type?
  • (See HOTT slides)

• Can I formalise „(A → ¬ A) → A → B“ in Agda?
  • I translate the proposition into a type and try to prove it but get stuck because I was unnecessarily confused by the „(A → ¬ A)“. I explain that this is actually „(A → A → ⊥)“, but forget to mention ⊥ means you cannot inhibit the type. Before I waste more time I am asked another question
• Can I formalise disjunction elimination „(A → C) → (B → C) → (A ∨ B) → C“?
  • I write down the type and definition without too many issues.

• I am asked if I can write down the definition of the J eliminator.
  • No. (It appears this was just a bonus question)

The final grade is 1.7 (where I had both a 1.7 in the exam and the exercises). I am disappointed but to be fair, I had no idea what the exam will be about and didn't study the stuff that was actually part of the exam, so in practice I went in unprepared. Considering that, 1.7 wasn't that bad.