#+title: IDenT Summary #+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: $$ \DeclareMathOperator{\inl}{inl} \DeclareMathOperator{\inr}{inr} $$ * References - [[https://github.com/cedille/ial][Iowa Agda Library]] - [[https://www8.cs.fau.de/ext/teaching/sose2021/hott/mltt-intro.pdf][Quick Intro to MLTT]] - [[https://agda.readthedocs.io/en/latest/][Agda Docs]] - [[https://homotopytypetheory.org/book/][The HoTT Book]] - Aaron Stump, Verified Functional Programming in Agda * Programming In Agda ** Modules ([[https://agda.readthedocs.io/en/latest/language/module-system.html][Docs]]) ** Intuitionistic Logic *** Kripke Semantics ** Proof Irrelevance #+begin_src agda2 ⌊log2⌋-wf-irrel : (n m : N) → {p : ↓B _>_ n} → {q : ↓B _>_ m} → n ≡ m → ⌊log2 n ⌋-wf p ≡ ⌊log2 m ⌋-wf q #+end_src Here proof irrelevance is enforced by stating that the proof of ~⌊log2 m ⌋-wf p~ does not depend on the choice of the proof object ~p~. In other words, any proof ~⌊log2 m ⌋-wf p~ is propositionally equal to any other proof ~⌊log2 m ⌋-wf q~. ** Termination ** Without K ([[https://agda.readthedocs.io/en/latest/language/cubical-compatible.html#cubical-compatible][Doc]]) ** Selected Topics *** Braun Trees *** Reflection * Martin-Löf Type Theory (See Chapter 1 in The HoTT Book) ** Principles *** Judgements - $a : A$ asserts that a term $a$ has type $A$ - $a = b : A$ states that two terms $a$ and $b$ are *judgementally equal* (definitionally) at type $A$ *** Rules We have three kinds of judgements: - $\Gamma \mathrm{ctx}$ - $\Gamma\vdash a : A$ - $\Gamma\vdash a = a' : A$ **** Structural Rules *** Propositions as Types #+attr_html: :border 2 | Proposition | Type | |------------------+---------| | $\mathrm{False}$ | $\bot$ | | $\mathrm{True}$ | $\top$ | | $A \land B$ | $A \times B$ | | $A \lor B$ | $A + B$ | | $A \to B$ | $A \to B$ | *** Proofs as Programs *** Induction as Recursion *** Dependent Types *** Proof Relevance In MLTT, proofs are mathematical objects themselves. In contrast to set theory, besides knowing that a proposition has some proof it is relevant to remember the way a given proof is constructed. For example to show an existential proposition $\Sigma_{(x : X)}\ \phi(x)$ we need a pair $(x : X, p : \phi(x))$. A non-constructive proof that shows that $\phi$ is satisfiable without giving a witness $x$ does not suffice. *** (Im-)Predicativity *** Universes Because of [[https://ncatlab.org/nlab/show/Russell%27s+paradox][Russel's paradox]] we cannot have a type of all types $\mathcal{U}$, such that $X : \mathcal{U}$ for every type $X$. Thus, we postulate an infinite hierarchy of type universes $\mathcal{U}_0, \mathcal{U}_1, \dots$. Each $\mathcal{U}_i$ is contained in $\mathcal{U}_{i + 1}$. ** Types *** Formation Rules For each type former the rules are classified as: - a *formation rule*, stating when the type former can be applied - *introduction rules*, stating how to inhabit the type - *elimination rules* or induction principle, stating how to use an element of the type - *computation rules*: judgemental equalities explaining what happens when elimination rules are applied to results of introduction rules - optional *uniqueness principles*: judgemental equalities explainint how every element of the type is uniquely determined by the results of elimination rules applied to it *** Empty Type $\bot$ \[ \dfrac{\Gamma \mathrm{ctx}}{\Gamma \vdash \bot : \mathcal{U}_i} \quad (\bot\text{-FORM})\\ \dfrac{\Gamma,x : \bot \vdash C : \mathcal{U}_i \quad \Gamma \vdash a : \bot}{\Gamma\vdash \mathrm{ind}_\bot (\lambda x \ldotp C, a) : C[a / x]} \quad (\bot\text{-ELIM}) \] *** Unit Type $\top$ \[ \dfrac{\Gamma \mathrm{ctx}}{\Gamma\vdash \top : \mathcal{U}_i} \quad (\top\text{-FORM})\\ \dfrac{\Gamma \mathrm{ctx}}{\Gamma\vdash \star : \top} \quad (\top\text{-INTRO})\\ \dfrac{\Gamma, x :\top \vdash C:\mathcal{U}_i \quad \Gamma\vdash c : C[\star/x]\quad \Gamma\vdash a : \top}{\Gamma\vdash\mathrm{ind}_\top(\lambda x \ldotp C, c, a) : C[a/x]} \quad (\top\text{-ELIM})\\ \dfrac{\Gamma, x :\top \vdash C:\mathcal{U}_i \quad \Gamma\vdash c : C[\star/x]}{\Gamma\vdash\mathrm{ind}_\top(\lambda x \ldotp C, c, \star) = c: C[\star/x]} \quad (\top\text{-COMP})\\ \] *** Dependent Function Types $\Pi$ \[ \dfrac{\Gamma \vdash A :\mathcal{U}_i \quad \Gamma, x : A \vdash B : \mathcal{U}_i}{\Gamma \vdash \Pi_{(x: A)} B :\mathcal{U}_i} \quad (\Pi\text{-FORM})\\ \dfrac{\Gamma, x : A \vdash b : B}{\Gamma \vdash \lambda x : A\ldotp b : \Pi_(x: A) B } \quad (\Pi\text{-INTRO})\\ \dfrac{\Gamma \vdash f :\Pi_{(x: A)} B \quad \Gamma\vdash a : A }{\Gamma\vdash f(a) : B[a/x]} \quad (\Pi\text{-ELIM})\\ \dfrac{\Gamma,x:A\vdash b : B \qquad \Gamma\vdash a : A}{\Gamma\vdash (\lambda x : A\ldotp b)(a) = b[a/x] : B[a/x]} \quad (\Pi\text{-COMP})\\ \dfrac{\Gamma\vdash f : \Pi_{(x : A)} B}{\Gamma\vdash f = (\lambda x : A\ldotp f(x)) : \Pi_{(x:A)}B} \quad (\Pi\text{-UNIQ}) \] The regular non-dependent function types are obtained from the rules for dependent function types by eliminating the dependency: \[ \dfrac {\Gamma \vdash A : \mathcal{U}_i \qquad \Gamma \vdash B : \mathcal{U}_i}{\Gamma \vdash (A \to B) : \mathcal{U}_i}\quad (\to\text{-FORM})\\ \dfrac {\Gamma, x : A \vdash b : B}{\Gamma \vdash (\lambda (x : A) \ldotp b) : A \to B}\quad (\to\text{-INTRO})\\ \dfrac {\Gamma \vdash f : A \to B \qquad \Gamma \vdash a : A}{\Gamma \vdash f(a) : B}\quad (\to\text{-ELIM})\\ \dfrac {\Gamma, x : A \vdash b : B \qquad \Gamma \vdash a : A}{\Gamma \vdash (\lambda (x : A) \ldotp b) (a) = b[a / x] : B}\quad (\to\text{-COMP})\\ \dfrac {\Gamma \vdash A \to B}{\Gamma \vdash f = (\lambda (x : A) \ldotp f(x)) : A \to B}\quad (\to\text{-UNIQ}) \] *** Coproduct Types $+$ \[ \dfrac{\Gamma\vdash A : \mathcal{U}_i \quad \Gamma\vdash B : \mathcal{U}_i}{\Gamma\vdash A + B : \mathcal{U}_i} \quad (+\text{-FORM})\\ \dfrac{\Gamma\vdash A : \mathcal{U}_i \quad \Gamma\vdash B : \mathcal{U}_i \quad \Gamma\vdash a : A}{\Gamma\vdash \inl a :A + B } \quad (+\text{-INTRO}_1)\\ \dfrac{\Gamma\vdash A : \mathcal{U}_i \quad \Gamma\vdash B : \mathcal{U}_i \quad \Gamma\vdash b : B}{\Gamma\vdash \inr b :A + B } \quad (+\text{-INTRO}_2)\\ \dfrac{\Gamma,z : A + B \vdash C : \mathcal{U}_i \quad \Gamma, x : A \vdash c : C[\inl x/z] \quad \Gamma,y : B \vdash d : C[\inr y/z] \quad \Gamma\vdash e : A + B}{\Gamma\vdash \mathrm{ind}_{A + B}(\lambda z \ldotp C, \lambda x\ldotp c, \lambda y\ldotp d, e) : C[e/z]} \quad (+\text{-ELIM})\\ \dfrac{\Gamma,z : A + B \vdash C : \mathcal{U}_i \quad \Gamma, x : A \vdash c : C[\inl x/z] \quad \Gamma,y : B \vdash d : C[\inr y/z] \quad \Gamma\vdash a : A}{\Gamma\vdash \mathrm{ind}_{A + B}(\lambda z \ldotp C, \lambda x\ldotp c, \lambda y\ldotp d, \inl a) = c[a/x] : C[\inl a/z]} \quad (+\text{-COMP}_1)\\ \dfrac{\Gamma,z : A + B \vdash C : \mathcal{U}_i \quad \Gamma, x : A \vdash c : C[\inl x/z] \quad \Gamma,y : B \vdash d : C[\inr y/z] \quad \Gamma\vdash b : B}{\Gamma\vdash \mathrm{ind}_{A + B}(\lambda z \ldotp C, \lambda x\ldotp c, \lambda y\ldotp d, \inr b) = c[a/x] : C[\inr b/z]} \quad (+\text{-COMP}_2) \] *** Dependent Pair Types $\Sigma$ #+begin_src agda2 data _≡_ {ℓ} {A : Set ℓ} (x : A) : A → Set ℓ where refl : x ≡ x #+end_src \[ \dfrac{ \Gamma\vdash A : \mathcal{U}_i\quad \Gamma,x : A\vdash B : \mathcal{U}_i } { \Gamma\vdash\Sigma_{(x : A)} B : \mathcal{U}_i } \quad (\Sigma\text{-FORM})\\ \dfrac{ \Gamma , x : A \vdash B : \mathcal{U}_i \quad \Gamma\vdash a : A\quad \Gamma\vdash b : B[a/x] } { \Gamma\vdash(a,b): \Sigma_{(x : A)}B } \quad (\Sigma\text{-INTRO}) \] We can obtain the regular cartesian product if $B$ does not contain free occurences of $x$. \[ \dfrac{ \Gamma , z : \Sigma_{(x : A)}B \vdash C : \mathcal{U}_i\quad \Gamma , x : A, y : B\vdash g : C[(x,y)/z]\quad \Gamma\vdash p : \Sigma_{(x : A)}B } { \Gamma\vdash \mathrm{ind}_{\Sigma_{(x : A)}B}(\lambda z \ldotp C, \lambda x y \ldotp g, p) : C[p/z] } \quad (\Sigma\text{-ELIM})\\ \dfrac{ \Gamma , z : \Sigma_{(x : A)}B \vdash C : \mathcal{U}_i\quad \Gamma , x : A, y : B\vdash g : C[(x,y)/z]\quad \Gamma\vdash a : A\quad \Gamma\vdash b : B[a/x] } { \Gamma\vdash \mathrm{ind}_{\Sigma_{(x : A)}B}(\lambda z \ldotp C, \lambda x y \ldotp g, (a,b)) = g[a/x,b/y] : C[(a,b)/z] } \quad (\Sigma\text{-COMP}) \] ** Identity Types $\equiv$ #+begin_src agda2 data Σ {ℓ ℓ'} (A : Set ℓ) (B : A → Set ℓ') : Set (ℓ ⊔ ℓ') where _,_ : (a : A) → (b : B a) → Σ A B #+end_src *** J-Eliminator *** K-Eliminator \[ \dfrac{\Gamma,p: a \equiv_A a \vdash C : \mathcal{U}_i \quad \Gamma\vdash c : C[\mathrm{refl}_a/p] \quad \Gamma\vdash p' : a \equiv_A a}{\Gamma\vdash K(\lambda p \ldotp C, c, p') : C[p'/p]} \] The K-eliminator enforces that any two identity proofs are equal, or that any identity proof is equal to ~refl~. *** Without K ([[https://agda.readthedocs.io/en/latest/language/cubical-compatible.html#cubical-compatible][Doc]])