IDenT Braindump SS22

• Give a general overview of the notion of propositions as types.
  

The idea is to model logical propositions as types.
To proof of a proposition means to give an inhabitant of the corresponding type.

• How do types relate to logical propositions ?
  

I construct a table relating constructs of propositional logic as types:

• Define a binary coproduct using dependent pairs.
  

\(\Sigma\, \mathbb{B}\, (\mathbb{B} \to Set)\)

• Define a binary product using dependent pairs.
  

\(\Sigma\, \mathbb{B}\, (\lambda \_ \to A)\)

• Give a general overview of Martin-Löf Type Theory
  I lay out some general facts about MLTT. I am being nudged to talk about MLTT as a formal system
  
• What kind of things exist in MLTT?
  
  • contexts
    
  • terms/types
    
  • equalities
    
• What kind of equalities exist in MLTT?
  
  • judgemental
    
  • propositional
    
• Can you give examples of rules?
  

I start giving the rules for context, but mess up the notation.
After some time and help I manage to give version of the rules for the empty context and appending to contexts that are at least reminiscant of the actual rules.

• Prove these intuitionistic tautologies in Agda
  

These were given on paper, to be formalised and proven in Agda.
I am asked if I want to code on my own laptop or use Sergey's. I choose my own (superior emacs keybindings)

open import lib

lemma : ∀ {A B : Set] → (A → ¬ A) → (A → B)
lemma a→¬a a = ⊥-elim (a→¬a a a)

lemma' : ∀ {A} → (f : 𝔹 → 𝔹) → (p : 𝔹 → A)  → 
       (p (f (f tt))) ≡ if (f tt) then p tt else p (f ff)
lemma' f p with keep (f tt)
... | tt , p' rewrite p' | p' = refl
... | ff , p' rewrite p'  = refl

• Can you give a version of the J-Eliminator
  Tbh, no. But I start giving a general overview of the identity type in MLTT
  I talk about propositional equalities as paths between points in a topological space.
  I explain what symmetry and transitivity mean in this view.
  Finally I try to give a general notion about how the J-Eliminator works, but fail to give an actual definition.
  

Final Grade is 1.3 (1.3 in exam and 1.7 in homework)
The atmosphere during the exam is fine, but I am often stumped by (imo) very general questions.