#+title: IDenT Braindump SS22
#+author: Florian Guthmann
#+email: florian.guthmann@fau.de
#+options: toc:nil num:nil \n:t html-style:nil html5-fancy:t
#+html_doctype: xhtml5

#+html_head: <link rel="stylesheet" type="text/css" href="/~oc45ujef/style/org.css"/>

* IDenT exam SS22
** Propositions as Types
- 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:

| true        | $\top$      |
| false       | $\bot$      |
| $A \land B$     | $A \times B$     |
| $A \lor B$     | $A + B$     |
| $A \to B$     | $A \to B$     |
| $\exists a . P a$ | $\Sigma\, A P$   |
| $\forall a . P a$ | $\forall\, A \to P A$ |

- 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)$

** MLTT

- 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.

** Intuitionistic Tautologies
- 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)
#+begin_src agda2
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
#+end_src


** J-Eliminator

- 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.

** Closing Notes
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.