IDenT Summary

• \(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\)
  

We have three kinds of judgements:

• \(\Gamma \mathrm{ctx}\)
  
• \(\Gamma\vdash a : A\)
  
• \(\Gamma\vdash a = a' : A\)
  

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.

Because of 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}\).

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
  

\[ \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}) \]

\[ \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})\\ \]

\[ \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}) \]

\[ \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) \]

data _≡_ {ℓ} {A : Set ℓ} (x : A) : A → Set ℓ where
  refl : x ≡ x

\[ \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}) \]

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