From c642f472884d855e6851a6fb0e58a1d19138eb72 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Mon, 22 Apr 2024 01:36:03 +0000 Subject: [PATCH] auto gitdoc commit --- src/HottBook/Chapter1.lagda.md | 1 - src/HottBook/Chapter2.lagda.md | 227 +++++++++++++----------- src/HottBook/Chapter2Exercises.lagda.md | 127 +++++++------ src/HottBook/Common.agda | 8 - 4 files changed, 196 insertions(+), 167 deletions(-) delete mode 100644 src/HottBook/Common.agda diff --git a/src/HottBook/Chapter1.lagda.md b/src/HottBook/Chapter1.lagda.md index 313bc10..c23290d 100644 --- a/src/HottBook/Chapter1.lagda.md +++ b/src/HottBook/Chapter1.lagda.md @@ -17,7 +17,6 @@ open import Agda.Primitive ``` data πŸ™ : Set where tt : πŸ™ - ``` ## 1.6 Dependent pair types (Ξ£-types) diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md index d3e3820..8a1997c 100644 --- a/src/HottBook/Chapter2.lagda.md +++ b/src/HottBook/Chapter2.lagda.md @@ -1,13 +1,30 @@ ``` module HottBook.Chapter2 where -open import Relation.Binary.PropositionalEquality -open import Function -open import Data.Product -open import Data.Product.Properties - -open import HottBook.Common +open import Agda.Primitive open import HottBook.Chapter1 +open import HottBook.Util +``` + +## 2.1 Types are higher groupoids + +``` +sym : {l : Level} {A : Set l} {x y : A} + β†’ (x ≑ y) β†’ y ≑ x +sym {l} {A} {x} {y} p = J (Ξ» x y p β†’ y ≑ x) (Ξ» x β†’ refl) x y p +``` + +``` +trans : {l : Level} {A : Set l} {x y z : A} + β†’ (x ≑ y) + β†’ (y ≑ z) + β†’ (x ≑ z) +trans {l} {A} {x} {y} {z} p q = + let + func1 x y p = J (Ξ» a b p β†’ a ≑ b) (Ξ» x β†’ refl) x y p + func2 = J (Ξ» a b p β†’ (z : A) β†’ (q : b ≑ z) β†’ a ≑ z) func1 x y p + in func2 z q +_βˆ™_ = trans ``` ## 2.2 Functions are functors @@ -15,8 +32,11 @@ open import HottBook.Chapter1 ### Lemma 2.2.1 ``` -ap : {A B : Type} (f : A β†’ B) {x y : A} β†’ (x ≑ y) β†’ f x ≑ f y -ap f {x} p = J (Ξ» y p β†’ f x ≑ f y) p refl +ap : {l : Level} {A B : Set l} {x y : A} + β†’ (f : A β†’ B) + β†’ (p : x ≑ y) + β†’ f x ≑ f y +ap {l} {A} {B} {x} {y} f p = J (Ξ» x y p β†’ f x ≑ f y) (Ξ» x β†’ refl) x y p ``` ## 2.3 Type families are fibrations @@ -24,113 +44,115 @@ ap f {x} p = J (Ξ» y p β†’ f x ≑ f y) p refl ### Lemma 2.3.1 (Transport) ``` -transport : {A : Type} (P : A β†’ Type) {x y : A} (p : x ≑ y) β†’ P x β†’ P y -transport P p = J (Ξ» y r β†’ P y) p +transport : {l₁ lβ‚‚ : Level} {A : Set l₁} {x y : A} + β†’ (P : A β†’ Set lβ‚‚) + β†’ (p : x ≑ y) + β†’ P x β†’ P y +transport {l₁} {lβ‚‚} {A} {x} {y} P p = J (Ξ» x y p β†’ P x β†’ P y) (Ξ» x β†’ id) x y p ``` ### Lemma 2.3.2 (Path lifting property) +TODO + ``` -lift : {A : Type} (P : A β†’ Type) {x y : A} (u : P x) β†’ (p : x ≑ y) - β†’ (x , u) ≑ (y , transport P p u) -lift {A} P {x} {y} u p = - J (Ξ» the what β†’ (x , u) ≑ (the , transport P what u)) p refl +-- lift : {A : Set} (P : A β†’ Set) {x y : A} (u : P x) β†’ (p : x ≑ y) +-- β†’ (x , u) ≑ (y , transport P p u) +-- lift {A} P {x} {y} u p = +-- J (Ξ» the what β†’ (x , u) ≑ (the , transport P what u)) p refl ``` Verifying its property: ``` -lift-prop : {A : Type} (P : A β†’ Type) {x y : A} (u : P x) β†’ (p : x ≑ y) - β†’ proj₁ (Ξ£-≑,≑←≑ (lift P u p)) ≑ p -lift-prop P u p = - J (Ξ» the what β†’ proj₁ (Ξ£-≑,≑←≑ (lift P u what)) ≑ what) p refl +-- lift-prop : {A : Set} (P : A β†’ Set) {x y : A} (u : P x) β†’ (p : x ≑ y) +-- β†’ Ξ£.fst (Ξ£-≑,≑←≑ (lift P u p)) ≑ p +-- lift-prop P u p = +-- J (Ξ» the what β†’ proj₁ (Ξ£-≑,≑←≑ (lift P u what)) ≑ what) p refl ``` ### Lemma 2.3.4 (Dependent map) ``` -apd : {A : Type} {P : A β†’ Type} (f : (x : A) β†’ P x) {x y : A} (p : x ≑ y) +apd : {l₁ lβ‚‚ : Level} {A : Set l₁} {P : A β†’ Set lβ‚‚} {x y : A} + β†’ (f : (x : A) β†’ P x) + β†’ (p : x ≑ y) β†’ transport P p (f x) ≑ f y -apd {A} {P} f {x} p = - let - D : (x y : A) β†’ (p : x ≑ y) β†’ Type - D x y p = transport P p (f x) ≑ f y - - d : (x : A) β†’ D x x refl - d x = refl - in - J (Ξ» y p β†’ transport P p (f x) ≑ f y) p (d x) +apd {l₁} {lβ‚‚} {A} {P} {x} {y} f p = + J (Ξ» x y p β†’ transport P p (f x) ≑ f y) (Ξ» x β†’ refl) x y p ``` ### Lemma 2.3.5 -``` -transportconst : {A : Type} {x y : A} (B : Type) β†’ (p : x ≑ y) β†’ (b : B) - β†’ transport (Ξ» _ β†’ B) p b ≑ b -transportconst {A} {x} B p b = - let - D : (x y : A) β†’ (p : x ≑ y) β†’ Type - D x y p = transport (Ξ» _ β†’ B) p b ≑ b +TODO - d : (x : A) β†’ D x x refl - d x = refl - in - J (Ξ» x p β†’ transport (Ξ» _ β†’ B) p b ≑ b) p (d x) +``` +-- transportconst : {A : Set} {x y : A} (B : Set) β†’ (p : x ≑ y) β†’ (b : B) +-- β†’ transport (Ξ» _ β†’ B) p b ≑ b +-- transportconst {A} {x} B p b = +-- let +-- D : (x y : A) β†’ (p : x ≑ y) β†’ Set +-- D x y p = transport (Ξ» _ β†’ B) p b ≑ b + +-- d : (x : A) β†’ D x x refl +-- d x = refl +-- in +-- J (Ξ» x p β†’ transport (Ξ» _ β†’ B) p b ≑ b) p (d x) ``` ### Lemma 2.3.8 ``` -lemma238 : {A B : Type} (f : A β†’ B) {x y : A} (p : x ≑ y) - β†’ apd f p ≑ transportconst B p (f x) βˆ™ ap f p -lemma238 {A} {B} f {x} p = - J (Ξ» y p β†’ apd f p ≑ transportconst B p (f x) βˆ™ ap f p) p refl +-- lemma238 : {A B : Set} (f : A β†’ B) {x y : A} (p : x ≑ y) +-- β†’ apd f p ≑ transportconst B p (f x) βˆ™ ap f p +-- lemma238 {A} {B} f {x} p = +-- J (Ξ» y p β†’ apd f p ≑ transportconst B p (f x) βˆ™ ap f p) p refl ``` ### Lemma 2.3.9 ``` -lemma239 : {A : Type} {P : A β†’ Type} {x y z : A} - β†’ (p : x ≑ y) β†’ (q : y ≑ z) β†’ (u : P x) - β†’ transport P q (transport P p u) ≑ transport P (p βˆ™ q) u -lemma239 {A} {P} p q u = - let - inner : transport P refl (transport P p u) ≑ transport P p u - inner = refl +-- lemma239 : {A : Set} {P : A β†’ Set} {x y z : A} +-- β†’ (p : x ≑ y) β†’ (q : y ≑ z) β†’ (u : P x) +-- β†’ transport P q (transport P p u) ≑ transport P (p βˆ™ q) u +-- lemma239 {A} {P} p q u = +-- let +-- inner : transport P refl (transport P p u) ≑ transport P p u +-- inner = refl - ok : p βˆ™ refl ≑ p - ok = J (Ξ» _ r β†’ r βˆ™ refl ≑ r) p refl +-- ok : p βˆ™ refl ≑ p +-- ok = J (Ξ» _ r β†’ r βˆ™ refl ≑ r) p refl - bruh : transport P (p βˆ™ refl) u ≑ transport P p u - bruh = ap (Ξ» r β†’ transport P r u) ok - in - J (Ξ» _ what β†’ - transport P what (transport P p u) ≑ transport P (p βˆ™ what) u - ) q (inner βˆ™ sym bruh) +-- bruh : transport P (p βˆ™ refl) u ≑ transport P p u +-- bruh = ap (Ξ» r β†’ transport P r u) ok +-- in +-- J (Ξ» _ what β†’ +-- transport P what (transport P p u) ≑ transport P (p βˆ™ what) u +-- ) q (inner βˆ™ sym bruh) ``` ### Lemma 2.3.10 ``` -lemma2310 : {A B : Type} (f : A β†’ B) β†’ (P : B β†’ Type) - β†’ {x y : A} (p : x ≑ y) β†’ (u : P (f x)) - β†’ transport (P ∘ f) p u ≑ transport P (ap f p) u -lemma2310 f P p u = - let - inner : transport (Ξ» y β†’ P (f y)) refl u ≑ u - inner = refl - in - J (Ξ» _ what β†’ transport (P ∘ f) what u ≑ transport P (ap f what) u) p inner +-- lemma2310 : {A B : Set} (f : A β†’ B) β†’ (P : B β†’ Set) +-- β†’ {x y : A} (p : x ≑ y) β†’ (u : P (f x)) +-- β†’ transport (P ∘ f) p u ≑ transport P (ap f p) u +-- lemma2310 f P p u = +-- let +-- inner : transport (Ξ» y β†’ P (f y)) refl u ≑ u +-- inner = refl +-- in +-- J (Ξ» _ what β†’ transport (P ∘ f) what u ≑ transport P (ap f what) u) p inner ``` ### Lemma 2.3.11 ``` -lemma2311 : {A : Type} {P Q : A β†’ Type} (f : (x : A) β†’ P x β†’ Q x) - β†’ {x y : A} (p : x ≑ y) β†’ (u : P x) - β†’ transport Q p (f x u) ≑ f y (transport P p u) -lemma2311 {A} {P} {Q} f {x} {y} p u = - J (Ξ» the what β†’ transport Q what (f x u) ≑ f the (transport P what u)) p refl +-- lemma2311 : {A : Set} {P Q : A β†’ Set} (f : (x : A) β†’ P x β†’ Q x) +-- β†’ {x y : A} (p : x ≑ y) β†’ (u : P x) +-- β†’ transport Q p (f x u) ≑ f y (transport P p u) +-- lemma2311 {A} {P} {Q} f {x} {y} p u = +-- J (Ξ» the what β†’ transport Q what (f x u) ≑ f the (transport P what u)) p refl ``` ## 2.4 Homotopies and equivalences @@ -138,8 +160,10 @@ lemma2311 {A} {P} {Q} f {x} {y} p u = ### Definition 2.4.1 (Homotopy) ``` -_∼_ : {A : Type} {P : A β†’ Type} (f g : (x : A) β†’ P x) β†’ Type -_∼_ {A} f g = (x : A) β†’ f x ≑ g x +_∼_ : {l₁ lβ‚‚ : Level} {A : Set l₁} {P : A β†’ Set lβ‚‚} + β†’ (f g : (x : A) β†’ P x) + β†’ Set (l₁ βŠ” lβ‚‚) +_∼_ {l₁} {lβ‚‚} {A} {P} f g = (x : A) β†’ f x ≑ g x ``` ### Lemma 2.4.2 @@ -147,13 +171,13 @@ _∼_ {A} f g = (x : A) β†’ f x ≑ g x Homotopy forms an equivalence relation: ``` -∼-refl : {A : Type} {P : A β†’ Type} (f : (x : A) β†’ P x) β†’ f ∼ f +∼-refl : {A : Set} {P : A β†’ Set} (f : (x : A) β†’ P x) β†’ f ∼ f ∼-refl f x = refl -∼-sym : {A : Type} {P : A β†’ Type} (f g : (x : A) β†’ P x) β†’ f ∼ g β†’ g ∼ f +∼-sym : {A : Set} {P : A β†’ Set} (f g : (x : A) β†’ P x) β†’ f ∼ g β†’ g ∼ f ∼-sym f g f∼g x = sym (f∼g x) -∼-trans : {A : Type} {P : A β†’ Type} (f g h : (x : A) β†’ P x) +∼-trans : {A : Set} {P : A β†’ Set} (f g h : (x : A) β†’ P x) β†’ f ∼ g β†’ g ∼ h β†’ f ∼ h ∼-trans f g h f∼g g∼h x = f∼g x βˆ™ g∼h x ``` @@ -161,7 +185,7 @@ Homotopy forms an equivalence relation: ### Lemma 2.4.3 ``` --- lemma243 : {A B : Type} {f g : A β†’ B} (H : f ∼ g) {x y : A} (p : x ≑ y) +-- lemma243 : {A B : Set} {f g : A β†’ B} (H : f ∼ g) {x y : A} (p : x ≑ y) -- β†’ H x βˆ™ ap g p ≑ ap f p βˆ™ H y -- lemma243 {f} {g} H {x} {y} p = -- J (Ξ» the what β†’ (H x βˆ™ ? ≑ ? βˆ™ H the)) p ? @@ -170,17 +194,17 @@ Homotopy forms an equivalence relation: ### Definition 2.4.6 ``` -record qinv {A B : Type} (f : A β†’ B) : Type where +record qinv {A B : Set} (f : A β†’ B) : Set where field g : B β†’ A - Ξ± : (f ∘ g) ∼ id - Ξ² : (g ∘ f) ∼ id + Ξ± : f ∘ g ∼ id + Ξ² : g ∘ f ∼ id ``` ### Example 2.4.7 ``` -id-qinv : {A : Type} β†’ qinv {A} id +id-qinv : {A : Set} β†’ qinv {A} id id-qinv = record { g = id ; Ξ± = Ξ» _ β†’ refl @@ -191,30 +215,24 @@ id-qinv = record ### Definition 2.4.10 ``` -linv : {A B : Type} (f : A β†’ B) β†’ Type -linv {A} {B} f = Ξ£[ g ∈ (B β†’ A) ] (f ∘ g) ∼ id - -rinv : {A B : Type} (f : A β†’ B) β†’ Type -rinv {A} {B} f = Ξ£[ h ∈ (B β†’ A) ] (h ∘ f) ∼ id - -isEquiv : {A B : Type} (f : A β†’ B) β†’ Type -isEquiv f = linv f Γ— rinv f +record isequiv {A B : Set} (f : A β†’ B) : Set where + constructor mkIsEquiv + field + g : B β†’ A + g-id : f ∘ g ∼ id + h : B β†’ A + h-id : h ∘ f ∼ id ``` ### Definition 2.4.11 ``` -_≃_ : (A B : Type) β†’ Type -A ≃ B = Ξ£[ f ∈ (A β†’ B) ] isEquiv f +_≃_ : (A B : Set) β†’ Set +A ≃ B = Ξ£[ f ∈ (A β†’ B) ] isequiv f ``` ## 2.8 The unit type -``` -data πŸ™ : Set where - ⋆ : πŸ™ -``` - ### Theorem 2.8.1 ``` @@ -247,16 +265,19 @@ data πŸ™ : Set where ### Lemma 2.9.2 ``` -happly : {A B : Type} β†’ (f g : A β†’ B) β†’ {x : A} β†’ (p : f ≑ g) β†’ f x ≑ g x -happly f g {x} p = - J (Ξ» the what β†’ f x ≑ the x) p refl +-- happly : {A B : Set} β†’ (f g : A β†’ B) β†’ {x : A} β†’ (p : f ≑ g) β†’ f x ≑ g x +-- happly f g {x} p = +-- J (Ξ» the what β†’ f x ≑ the x) p refl ``` ### Axiom 2.9.3 (Function extensionality) ``` postulate - funext : {A B : Type} β†’ (f g : A β†’ B) β†’ {x : A} β†’ (p : f x ≑ g x) β†’ f ≑ g + funext : {l : Level} {A B : Set l} + β†’ {f g : A β†’ B} + β†’ ((x : A) β†’ f x ≑ g x) + β†’ f ≑ g ``` ## 2.10 Universes and the univalence axiom @@ -264,7 +285,7 @@ postulate ### Lemma 2.10.1 ``` --- idToEquiv : {A B : Type} β†’ (A ≑ B) β†’ A ≃ B +-- idToEquiv : {A B : Set} β†’ (A ≑ B) β†’ A ≃ B -- idToEquiv p = ? , ? ``` @@ -272,5 +293,5 @@ postulate ``` postulate - ua : {A B : Type} (eqv : A ≃ B) β†’ (A ≑ B) + ua : {A B : Set} (eqv : A ≃ B) β†’ (A ≑ B) ``` diff --git a/src/HottBook/Chapter2Exercises.lagda.md b/src/HottBook/Chapter2Exercises.lagda.md index 025ac14..0aa85c6 100644 --- a/src/HottBook/Chapter2Exercises.lagda.md +++ b/src/HottBook/Chapter2Exercises.lagda.md @@ -1,11 +1,10 @@ ``` module HottBook.Chapter2Exercises where -import Relation.Binary.PropositionalEquality as Eq -open Eq -open Eq.≑-Reasoning -Type = Set -transport = subst +open import HottBook.Chapter1 +open import HottBook.Chapter1Util +open import HottBook.Chapter2 +open import HottBook.Util ``` ## Exercise 2.4 @@ -33,65 +32,83 @@ Prove that the functions [2.3.6] and [2.3.7] are inverse equivalences. Show that (2 ≃ 2) ≃ 2. ``` -open import Function.HalfAdjointEquivalence -open import Data.Bool -open _≃_ +exercise2βˆ™13 : (𝟚 ≃ 𝟚) ≃ 𝟚 +exercise2βˆ™13 = aux1 , equiv1 + where + aux1 : 𝟚 ≃ 𝟚 β†’ 𝟚 + aux1 (fst , snd) = fst true -id : {A : Type} β†’ A β†’ A -id x = x + neg : 𝟚 β†’ 𝟚 + neg true = false + neg false = true -Bool-id-equiv : Bool ≃ Bool -Bool-id-equiv = record - { to = id - ; from = id - ; left-inverse-of = Ξ» _ β†’ refl - ; right-inverse-of = Ξ» _ β†’ refl - ; left-right = Ξ» _ β†’ refl - } + neg-homotopy : (neg ∘ neg) ∼ id + neg-homotopy true = refl + neg-homotopy false = refl -Bool-neg : Bool β†’ Bool -Bool-neg true = false -Bool-neg false = true + open Ξ£ + open isequiv -Bool-neg-refl : (x : Bool) β†’ Bool-neg (Bool-neg x) ≑ x -Bool-neg-refl true = refl -Bool-neg-refl false = refl + rev : 𝟚 β†’ (𝟚 ≃ 𝟚) + fst (rev true) = id + g (snd (rev true)) = id + g-id (snd (rev true)) x = refl + h (snd (rev true)) = id + h-id (snd (rev true)) x = refl + fst (rev false) = neg + g (snd (rev false)) = neg + g-id (snd (rev false)) = neg-homotopy + h (snd (rev false)) = neg + h-id (snd (rev false)) = neg-homotopy -Bool-neg-refl-refl : (x : Bool) - β†’ cong Bool-neg (Bool-neg-refl x) ≑ Bool-neg-refl (Bool-neg x) -Bool-neg-refl-refl true = refl -Bool-neg-refl-refl false = refl + equiv1 : isequiv aux1 + g equiv1 = rev + g-id equiv1 (f , f-equiv @ (mkIsEquiv g g-id h h-id)) = + -- proving that given any equivalence e, that: + -- ((aux1 ∘ rev) e ≑ id e) + -- (rev (aux1 e) ≑ e) + -- (rev (e.fst true) ≑ e) + -- since e is a pair, decompose it using Ξ£-≑ and prove separately that: + -- - fst (rev (e.fst true)) ≑ e.fst + -- - left side is a function and right side is a function too + -- - use function extensionality to show they behave the same + -- - somehow use the fact that e.snd.g-id exists + -- - snd (rev (e.fst true)) ≑ e.snd + Ξ£-≑ (funext test1 , {! !}) + where + test1 : (x : 𝟚) β†’ fst (rev (f true)) x ≑ f x + test1 x with x , f true + test1 _ | true , true = {! !} + test1 _ | true , false = {! !} + test1 _ | false , y = {! !} -Bool-neg-equiv : Bool ≃ Bool -Bool-neg-equiv = record - { to = Bool-neg - ; from = Bool-neg - ; left-inverse-of = Bool-neg-refl - ; right-inverse-of = Bool-neg-refl - ; left-right = Bool-neg-refl-refl - } + -- if f mapped everything to the same value, then the inverse couldn't exist + -- how to state this as a proof? -Bool-to : (Bool ≃ Bool) β†’ Bool -Bool-to eqv = eqv .to true + asdf : (x : 𝟚) β†’ neg (f x) ≑ f (neg x) + -- known that (f ∘ g) x ≑ x + -- g (f x) ≑ x + -- g (f true) ≑ true + asdf true = {! !} + asdf false = {! !} -Bool-from : Bool β†’ (Bool ≃ Bool) -Bool-from true = Bool-id-equiv -Bool-from false = Bool-neg-equiv + ft = f true + ff = f false -Bool-left-inverse : (eqv : Bool ≃ Bool) β†’ Bool-from (Bool-to eqv) ≑ eqv -Bool-left-inverse eqv = - J (Ξ» the what β†’ Bool-from (Bool-to the) ≑ eqv) refl ? + div : ft β‰’ ff + div p = + let + id𝟚 : 𝟚 β†’ 𝟚 + id𝟚 = id -Bool-right-inverse : (x : Bool) β†’ Bool-to (Bool-from x) ≑ x -Bool-right-inverse true = refl -Bool-right-inverse false = refl + wtf : ft ≑ ff + wtf = p -Bool≃Bool≃Bool : (Bool ≃ Bool) ≃ Bool -Bool≃Bool≃Bool = record - { to = Bool-to - ; from = Bool-from - ; left-inverse-of = Bool-left-inverse - ; right-inverse-of = Bool-right-inverse - ; left-right = ? - } + wtf2 : g ft ≑ g ff + wtf2 = ap g wtf + + in {! !} + h equiv1 = rev + h-id equiv1 true = refl + h-id equiv1 false = refl ``` diff --git a/src/HottBook/Common.agda b/src/HottBook/Common.agda deleted file mode 100644 index 015c173..0000000 --- a/src/HottBook/Common.agda +++ /dev/null @@ -1,8 +0,0 @@ -module HottBook.Common where - -open import Relation.Binary.PropositionalEquality using (trans) - -Type = Set - -infixr 6 _βˆ™_ -_βˆ™_ = trans \ No newline at end of file