From 63f1c282a940ca9edaccfb83dffbd81080edd38e Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Mon, 29 Jul 2024 14:39:10 -0500 Subject: [PATCH] update --- .gitignore | 3 +- Exercises1.agda | 27 ++++++ Exercises1.v | 56 ++++++++++++ Lecture1.typ | 198 ++++++++++++++++++++++++++++++++++++++++--- Lecture2.typ | 7 ++ unimath2024.agda-lib | 2 + 6 files changed, 280 insertions(+), 13 deletions(-) create mode 100644 Exercises1.agda create mode 100644 Exercises1.v create mode 100644 Lecture2.typ create mode 100644 unimath2024.agda-lib diff --git a/.gitignore b/.gitignore index ce0eb4f..40f700d 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,4 @@ .direnv .*.aux -*.pdf \ No newline at end of file +*.pdf +*.agdai \ No newline at end of file diff --git a/Exercises1.agda b/Exercises1.agda new file mode 100644 index 0000000..fdc00a6 --- /dev/null +++ b/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 diff --git a/Exercises1.v b/Exercises1.v new file mode 100644 index 0000000..d9be398 --- /dev/null +++ b/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 *) \ No newline at end of file diff --git a/Lecture1.typ b/Lecture1.typ index ee595d0..af22adf 100644 --- a/Lecture1.typ +++ b/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 $ \ No newline at end of file diff --git a/Lecture2.typ b/Lecture2.typ new file mode 100644 index 0000000..f41e190 --- /dev/null +++ b/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. \ No newline at end of file diff --git a/unimath2024.agda-lib b/unimath2024.agda-lib new file mode 100644 index 0000000..b053ed9 --- /dev/null +++ b/unimath2024.agda-lib @@ -0,0 +1,2 @@ +depend: agda-unimath +include: . \ No newline at end of file