The atmosphere was OK but not great, at points I struggled to understand what the question was about, especially when the questions were very vague. ---- ====== Propositions as Types ====== * 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? ====== Dependent Pairs and Sums ====== * 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. ====== MLTT ====== * 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. ===== Guest Contribution: MLTT ===== (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"? - Terms which also serve as types - Typing judgements - Judgemental equality - Contexts and well-formed context judgements * What is the elimination rule for the bottom type? * (See HOTT slides) ====== Agda ====== * 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. ====== Closing Notes ====== * 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.