update

.gitignore

@@ -1,3 +1,4 @@
 .direnv
 .*.aux
-*.pdf
+*.pdf
+*.agdai

Exercises1.agda

@@ -0,0 +1,27 @@
+module Exercises1 where
+
+open import Agda.Primitive
+
+open import foundation-core.empty-types
+open import foundation-core.equivalences
+open import foundation-core.negation
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.univalence
+open import foundation.sections
+open import foundation.retractions
+
+_≡_ = _＝_
+⊥ = empty
+
+equal-to-zero : {A : Set} (f : ¬ A) → A ≡ ⊥
+equal-to-zero {A} f = eq-equiv A ⊥ eqv 
+  where
+    s : section f
+    s = (λ ()) , λ x → ex-falso x
+
+    r : retraction f
+    r = (λ ()) , λ x → ex-falso (f x)
+
+    eqv : A ≃ ⊥
+    eqv = f , s , r

Exercises1.v

@@ -0,0 +1,56 @@
+Require Import UniMath.Foundations.All.
+
+Inductive empty : Type := .
+
+Definition slide16_exercise (t : empty): bool :=
+  match t with end.
+
+Definition slide18_exercise (t : nat): bool :=
+  match t with
+  | O => true
+  | S _ => false
+  end.
+
+(* Slide 22, Exercise 1*)
+
+Definition fst {A B : Type} (p : A × B): A.
+Proof.
+  induction p.
+  apply pr1.
+Defined.
+(* Show Proof. *)
+
+Definition snd {A B : Type} (p : A × B): B.
+Proof.
+  induction p.
+  apply pr2.
+Defined.
+
+Definition swap {A B : Type} (p : A × B): B × A :=
+  match p with (a ,, b) => (b ,, a) end.
+(* Definition swap {A B : Type} (p : A × B): B × A.
+Proof.
+  induction p.
+  constructor.
+  - apply pr2. 
+  - apply pr1.
+Defined. *)
+
+(* Slide 38, Exercise: transport *)
+
+Definition transport {A : Type} {B : A -> Type}
+  {x y : A} (p : paths x y) (bx : B x): B y.
+  induction p. 
+  apply bx.
+Defined.
+(* Show Proof. *)
+
+(* Slide 39, Exercise: swap involutive *)
+
+Definition slide39_exercise {A B : Type} (t : A × B) : paths (swap (swap t)) t.
+  reflexivity.
+Show Proof.
+
+(* Slide 44, Exercise: neg *)
+
+(* Definition slide44_exercise {A : Type} : not  *)

Lecture1.typ

@@ -11,6 +11,10 @@ Important features in MLTT:
 #let Nat = $sans("Nat")$
 #let Vect = $sans("Vect")$
 
+#let Bool = $sans("Bool")$
+#let tru = $sans("true")$
+#let fls = $sans("false")$
+
 - Dependent types and functions.
   e.g $ "concatenate": Pi_(m,n:"Nat") Vect(m) -> Vect(n) -> Vect(m+n) $
   - Function arrows always associate to the right.
@@ -36,11 +40,13 @@ $ "context" tack.r "conclusion" $
 
 Example:
 
-$ "isZero?"& : Nat -> "Bool" \
-  "isZero?"& (n) :defeq "??"
+#let isZero = $sans("isZero?")$
+
+$ isZero& : Nat -> Bool \
+  isZero& (n) :defeq "??"
 $
 
-At this point, looking for $(n: Nat) tack.r "isZero?"(n) : "Bool"$.
+At this point, looking for $(n: Nat) tack.r isZero(n) : Bool$.
 
 === Inference rules
 
@@ -96,13 +102,16 @@ If $a defeq a'$ then $f @ a defeq f @ a'$.
 
 Example (context $Gamma$ are elided):
 
+=== Functions
+
 #typeIntroTable(
   [If $A$ and $B$ are types, then $A -> B$ is a type
     #prooftree(axiom($Gamma tack.r A$), axiom($Gamma tack.r B$), rule(n: 2, $Gamma tack.r A -> B$))],
   [If $(x : A) tack.r b : B$, then $tack.r lambda (x : A) . b(x) : A -> B$
     - $b$ is an expression that might involve $x$],
   [If we have a function $f : A -> B$, and $a : A$, then $f @ a : B$ (or $f(a) : B$)],
-  [What is the result of the application? $(lambda(x : A) . b(x)) @ a defeq subst(a, x, b)$
+  [What is the result of the application? \
+  $(lambda(x : A) . b(x)) @ a defeq subst(a, x, b)$
     - Substitution $subst(a, x, b)$ is built-in],
 )
 
@@ -112,9 +121,12 @@ Questions:
 
 Another example: the singleton type
 
+=== Unit type
+
 #let unit = $bb(1)$
-#let tt = $t t$
+#let tt = $star$
 #let rec = $sans("rec")$
+#let ind = $sans("ind")$
 
 #typeIntroTable(
   [$unit$ is a type],
@@ -127,11 +139,7 @@ Another example: the singleton type
 - Question: *How to construct this using lambda abstraction?*
   - (Structural rule: having $tack.r c : C$ means $x : unit tack.r c : C$, which by the lambda introduction rule gives us $lambda x.c : unit -> C$)
 
-Booleans
-
-#let Bool = $sans("Bool")$
-#let tru = $sans("true")$
-#let fls = $sans("false")$
+=== Booleans
 
 #typeIntroTable(
   [$Bool$ is a type],
@@ -140,7 +148,7 @@ Booleans
   [$rec_Bool (C, c, c', tru) defeq c$ and $rec_Bool (C, c, c', fls) defeq c'$],
 )
 
-Empty type
+=== Empty type
 
 #let empty = $bb(0)$
 
@@ -151,7 +159,7 @@ Empty type
   [_(no computation rule)_],
 )
 
-Natural numbers
+=== Natural numbers
 
 #let zero = $sans("zero")$
 #let suc = $sans("suc")$
@@ -166,3 +174,169 @@ Natural numbers
   We can define computation rule on naturals using a universal property],
 )
 
+=== Pattern matching
+
+*Exercise.* Define a function $isZero : Nat -> Bool$.
+
+*Solution.* $isZero :defeq lambda (x : Nat) . rec_Nat (Bool , tru, lambda (x : Bool) . fls , x)$.
+
+This is cumbersome and prone to mistakes. Instead we use pattern matching. A function $A -> C$ is completely specified if it's specified on the *canonical elements* of $A$.
+
+$ isZero& : Nat -> Bool \
+ isZero& zero defeq tru \
+ isZero& suc (n) defeq fls \
+$
+
+=== Pairs
+
+#let pair = $sans("pair")$
+
+#typeIntroTable(
+  [If $A$ and $B$ are types, then $A times B$ is a type],
+  [If $a : A$ and $b : B$, then $pair(a, b) : A times B$],
+  [If $C$ is a type, and $p : A -> B -> C$ and $t : A times B$, then $rec_times (A, B, C, p, t) : C$],
+  [...],
+)
+
+#let fst = $sans("fst")$
+#let snd = $sans("snd")$
+#let swap = $sans("swap")$
+#let assoc = $sans("assoc")$
+
+*Exercise.* Define $snd : A times B -> A$ and $snd : A times B -> B$.
+
+*Exercise.* Given types $A$ and $B$, write a function $swap$ of type $A times B -> B times A$.
+
+*Exercise.* What is the type of $swap @ pair (tt , fls)$?
+
+*Exercise.* Write a function $assoc$ of type $(A times B) times C -> A times (B times C)$
+
+=== Type dependency
+
+In particular: dependent type $B$ over $A$. (read "family $B$ of types indexed by $A$")
+
+Example: type of vectors.
+
+$ n : Nat tack.r Vect(n) $
+
+=== Universes
+
+#let Type = $sans("Type")$
+
+There is a type $Type$. Its elements are types ($A : Type$). The dependent function $x : A tack.r B$ can be considered a function $lambda x . B : A -> Type$.
+
+What is the type of $Type$? $Type$ is in an indexed hierarchy to avoid type-in-type paradox. We usually omit the index: $Type_i : Type_(i + 1)$
+
+=== Dependent functions $product_(x : A) B$
+
+#typeIntroTable(
+  [If $A$ is a type, and $B$ is a type family indexed by $A$, then there is a type $product_(x : A) B$],
+  [If $(x : A) tack.r b : B$, then $lambda (x : A) . b : product_(x : A) B$],
+  [If $f : product_(x : A) B$ and $a : A$, then $f(a) : subst(x, a, B)$],
+  [$(lambda (x : A) . b) ( a) defeq subst(x, a, b)$
+  - The case $A -> B$ is a special case of the dependent function, where $B$ doesn't depend on $x : A$],
+)
+
+=== Dependent pairs $Sigma_(x : A) B$
+
+#typeIntroTable(
+  [If $x : A tack.r B$, then there is a type $Sigma_(x : A) B$],
+  [If $a : A$ and $b : B(a)$, then $pair (a, b) : Sigma_(x : A) B$],
+  [...],
+  [...
+  - The case $A times B$ is a special case of the dependent function, where $B$ doesn't depend on $x : A$],
+)
+
+=== Identity type
+
+#let Id = $sans("Id")$
+#let refl = $sans("refl")$
+#let propeq = $=$
+
+#typeIntroTable(
+  [If $a : A$ and $b : A$, then $Id_A (a, b)$ is a type],
+  [If $a : A$, then $refl(a) : Id_A (a, a)$],
+  [
+    - If $(x, y : A), (p : Id_A (x, y)) tack.r C (x, y, p)$
+    - and $(x : A) tack.r t(x) : C(x, x, refl(x))$
+    - then $(x, y : A), (p : Id_A (x, y)) tack.r ind_Id (t; x, y, p) : C(x, y, p)$],
+  [...],
+)
+
+- (There are dependent versions of each of the previous elimination rules that resulted in $C$)
+- $ind$ "induction" is used more when the $C$ is dependent, while $rec$ is better for non-dependent $C$'s.
+
+For example, to define:
+
+#let sym = $sans("sym")$
+
+$ sym : product_(x, y : A) Id(x, y) -> Id(y, x) $
+
+it suffices to just specify its image on $(x, x, refl)$
+
+#prooftree(
+  axiom($x : A tack.r refl(x) : Id(x, x)$),
+  rule($(x, y : A) , (p : Id(x, y)) tack.r Id(y, x)$),
+  rule($x, y : A tack.r Id(x, y) -> Id(y, x)$),
+  rule($sym : product_(x, y : A) Id(x, y) -> Id(y, x)$)
+)
+
+So $sym(x, x, refl(x)) :defeq refl(x)$
+
+#let transport = $sans("transport")$
+
+*Exercise.* Define $transport^B : product_(x, y : A) Id(x, y) -> B(x) -> B(y)$.
+
+*Exercise: swap is involutive.* Given types $A$ and $B$, write a function $product_(t : A times B) Id(swap(swap(t)), t)$
+
+=== Disjoint sum
+
+#let inl = $sans("inl")$
+#let inr = $sans("inr")$
+
+#typeIntroTable(
+  [If $A$ and $B$ are types, then $A + B$ is a type],
+  [
+    - If $a : A$, then $inl(a) : A + B$
+    - If $b : B$, then $inr(b) : A + B$
+  ],
+  [If $f : A -> C$ and $g : B ->C $ then $rec_+ (C, f, g) : A + B -> C$],
+  [
+    - $rec_+ (C, f, g)( inl(a)) defeq f(a)$
+    - $rec_+ (C, f, g)( inr(b)) defeq g(a)$
+  ],
+)
+
+=== Interpreting types as sets and propositions
+
+#table(
+  columns: 3,
+  stroke: 0in,
+  [$A$], [set $A$], [proposition $A$],
+  [$a:A$], [$a in A$], [$a$ is a proof of $A$],
+  [$unit$], [], [$top$],
+  [$empty$], [], [$bot$],
+  [$A times B$], [cartesian product], [$A and B$],
+  [$A + B$], [disjoint unions $A  B$], [$A or B$],
+  [$A -> B$], [set of functions $A -> B$], [$A => B$],
+  [$x : A tack.r B(x)$], [], [predicate $B$ on $A$],
+  [$sum_(x : A) B(x)$], [], [$exists x in A, B(x)$],
+  [$product_(x : A) B(x)$], [], [$forall x in A, B(x)$],
+  [$Id_A (a, b)$], [], [equality $a = b$],
+)
+
+The connectives $forall$ and $exists$ behave constructively.
+
+The interpretation into propositions is known as the *Curry-Howard correspondence*.
+
+=== Negation
+
+$ not A :defeq A -> empty $
+
+*Exercise.* Construct a term of type $A -> not not A$. 
+
+*Exercise ($tru eq.not fls$).* Construct a term of type $not Id(tru, fls)$.
+
+*Solution.* Let $B :defeq rec_Bool (Type, unit, empty)$. Then $B(tru) defeq unit$ and $B(fls) defeq empty$. Then:
+
+$ lambda (p : Id(tru, fls)) . transport^B (p, tt) : Id(tru, fls) -> empty $

Lecture2.typ

@@ -0,0 +1,7 @@
+= Coq
+
+UniMath is library for univalent math.
+
+Plain coq has general coinductive datatypes and other things we will not use.
+
+Also, univalence axiom is assumed.

unimath2024.agda-lib

@@ -0,0 +1,2 @@
+depend: agda-unimath
+include: .