diff --git a/.vscode/settings.json b/.vscode/settings.json index b5429d2..6cab46b 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -4,8 +4,6 @@ "gitdoc.autoCommitDelay": 300000, "gitdoc.commitMessageFormat": "'auto gitdoc commit'", "agdaMode.connection.commandLineOptions": "--without-K", - "search.exclude": { - "src/CubicalHott/**": true - }, + "search.exclude": {}, "editor.fontFamily": "'PragmataPro Mono Liga', 'Droid Sans Mono', 'monospace', monospace" } diff --git a/src/CubicalHott/Chapter1.lagda.md b/src/CubicalHott/Chapter1.lagda.md deleted file mode 100644 index b091a79..0000000 --- a/src/CubicalHott/Chapter1.lagda.md +++ /dev/null @@ -1,122 +0,0 @@ -``` -{-# OPTIONS --no-load-primitives --cubical #-} -module CubicalHott.Chapter1 where - -open import CubicalHott.Primitives public -``` - -## 1.4 Dependent function types (Ξ -types) - -``` -id : βˆ€ {l} {A : Type l} β†’ A β†’ A -id x = x -``` - -## 1.5 Product types - -``` -data πŸ™ : Type where - tt : πŸ™ -``` - -## 1.7 Coproduct types - -``` -record Ξ£ {β„“ β„“'} (A : Type β„“) (B : A β†’ Type β„“') : Type (β„“ βŠ” β„“') where - constructor _,_ - field - fst : A - snd : B fst - -open Ξ£ public - -{-# BUILTIN SIGMA Ξ£ #-} -infixr 4 _,_ - -syntax Ξ£ A (Ξ» x β†’ B) = Ξ£[ x ∈ A ] B - -_Γ—_ : {l : Level} (A B : Type l) β†’ Type l -_Γ—_ A B = Ξ£ A (Ξ» _ β†’ B) -``` - -Unit type: - -``` -record ⊀ : Type where - instance constructor tt -{-# BUILTIN UNIT ⊀ #-} -``` - -``` -data βŠ₯ : Type where -``` - -## 1.8 The type of booleans - -``` -data 𝟚 : Type where - true : 𝟚 - false : 𝟚 -``` - -``` -neg : 𝟚 β†’ 𝟚 -neg true = false -neg false = true -``` - -## 1.11 Propositions as types - -``` -infix 3 Β¬_ -Β¬_ : βˆ€ {l} (A : Type l) β†’ Type l -Β¬_ A = A β†’ βŠ₯ -``` - -## 1.12 Identity types - -``` -private - to-path : βˆ€ {l} {A : Type l} β†’ (f : I β†’ A) β†’ Path A (f i0) (f i1) - to-path f i = f i - -refl : {l : Level} {A : Type l} {x : A} β†’ x ≑ x -refl {x = x} = to-path (Ξ» i β†’ x) -``` - -### 1.12.3 Disequality - -``` -_β‰’_ : {A : Type} (x y : A) β†’ Type -_β‰’_ x y = (p : x ≑ y) β†’ βŠ₯ -``` - -# Exercises - -## Exercise 1.1 - -Given functions f : A β†’ B and g : B β†’ C, define their composite g β—¦ f : A β†’ C. -Show that we have h β—¦ (g β—¦ f) ≑ (h β—¦ g) β—¦ f. - -``` -composite : {A B C : Type} - β†’ (f : A β†’ B) - β†’ (g : B β†’ C) - β†’ A β†’ C -composite f g x = g (f x) - --- https://agda.github.io/agda-stdlib/master/Function.Base.html -infixr 9 _∘_ -_∘_ : {l1 l2 l3 : Level} {A : Type l1} {B : Type l2} {C : Type l3} - β†’ (g : B β†’ C) - β†’ (f : A β†’ B) - β†’ A β†’ C -_∘_ g f x = g (f x) - -composite-assoc : {A B C D : Type} - β†’ (f : A β†’ B) - β†’ (g : B β†’ C) - β†’ (h : C β†’ D) - β†’ h ∘ (g ∘ f) ≑ (h ∘ g) ∘ f -composite-assoc f g h = refl -``` \ No newline at end of file diff --git a/src/CubicalHott/Chapter2.lagda.md b/src/CubicalHott/Chapter2.lagda.md deleted file mode 100644 index 078759f..0000000 --- a/src/CubicalHott/Chapter2.lagda.md +++ /dev/null @@ -1,299 +0,0 @@ -``` -{-# OPTIONS --no-load-primitives --cubical #-} -module CubicalHott.Chapter2 where - -open import CubicalHott.Chapter1 -open import CubicalHott.Chapter2Lemma221 public -``` - -``` -``` - - -### Lemma 2.1.1 - -``` -sym : {l : Level} {A : Type l} {x y : A} β†’ (x ≑ y) β†’ y ≑ x -sym {l} {A} {x} {y} p i = p (~ i) -``` - -### Lemma 2.1.2 - -TODO: Read more about composition [here](https://1lab.dev/1Lab.Path.html#composition) - -``` -private - -- https://1lab.dev/1Lab.Reflection.Regularity.html#1191 - double-comp - : βˆ€ {β„“} {A : Type β„“} {w z : A} (x y : A) - β†’ w ≑ x β†’ x ≑ y β†’ y ≑ z - β†’ w ≑ z - double-comp x y p q r i = primHComp - (Ξ» { j (i = i0) β†’ p (~ j) ; j (i = i1) β†’ r j }) (q i) - -trans : βˆ€ {l} {A : Type l} {x y z : A} β†’ (x ≑ y) β†’ (y ≑ z) β†’ (x ≑ z) -trans {l} {A} {x} {y} {z} p q = double-comp x y refl p q - -infixr 30 _βˆ™_ -_βˆ™_ = trans -``` - -### Equational Reasoning - -``` -module ≑-Reasoning where - infix 1 begin_ - begin_ : {l : Level} {A : Type l} {x y : A} β†’ (x ≑ y) β†’ (x ≑ y) - begin x = x - - _β‰‘βŸ¨βŸ©_ : {l : Level} {A : Type l} (x {y} : A) β†’ x ≑ y β†’ x ≑ y - _ β‰‘βŸ¨βŸ© x≑y = x≑y - - infixr 2 _β‰‘βŸ¨βŸ©_ step-≑ - step-≑ : {l : Level} {A : Type l} (x {y z} : A) β†’ y ≑ z β†’ x ≑ y β†’ x ≑ z - step-≑ _ y≑z x≑y = trans x≑y y≑z - syntax step-≑ x y≑z x≑y = x β‰‘βŸ¨ x≑y ⟩ y≑z - - infix 3 _∎ - _∎ : {l : Level} {A : Type l} (x : A) β†’ (x ≑ x) - _ ∎ = refl -``` - -### Lemma 2.1.4 - -``` -module lemma2βˆ™1βˆ™4 {l : Level} {A : Type l} where - iii : {x y : A} (p : x ≑ y) β†’ sym (sym p) ≑ p - iii {x} {y} p i j = p j -``` - -### Lemma 2.2.1 - -{{#include CubicalHott.Chapter2Lemma221.md:ap}} - -### Lemma 2.3.1 (Transport) - -``` --- 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 refl = id - -transport : βˆ€ {l1 l2} {A : Type l1} {x y : A} - β†’ (P : A β†’ Type l2) β†’ (p : x ≑ y) β†’ P x β†’ P y -transport P p = transp (Ξ» i β†’ P (p i)) i0 -``` - -### Definition 2.4.1 (Homotopy) - -``` -infixl 18 _∼_ -_∼_ : {l₁ lβ‚‚ : Level} {A : Type l₁} {P : A β†’ Type lβ‚‚} - β†’ (f g : (x : A) β†’ P x) - β†’ Type (l₁ βŠ” lβ‚‚) -_∼_ {l₁} {lβ‚‚} {A} {P} f g = (x : A) β†’ f x ≑ g x -``` - -### Definition 2.4.6 - -``` -record qinv {l1 l2 : Level} {A : Type l1} {B : Type l2} (f : A β†’ B) : Type (l1 βŠ” l2) where - constructor mkQinv - field - g : B β†’ A - Ξ± : (f ∘ g) ∼ id - Ξ² : (g ∘ f) ∼ id -``` - -### Definition 2.4.10 - -``` -record isequiv {l1 l2 : Level} {A : Type l1} {B : Type l2} (f : A β†’ B) : Type (l1 βŠ” l2) where - eta-equality - constructor mkIsEquiv - field - g : B β†’ A - g-id : (f ∘ g) ∼ id - h : B β†’ A - h-id : (h ∘ f) ∼ id -``` - -``` -qinv-to-isequiv : {l1 l2 : Level} {A : Type l1} {B : Type l2} - β†’ {f : A β†’ B} - β†’ qinv f - β†’ isequiv f -qinv-to-isequiv (mkQinv g Ξ± Ξ²) = mkIsEquiv g Ξ± g Ξ² -``` - -Still kinda shaky on this one, TODO study it later: - -``` -isequiv-to-qinv : {l : Level} {A B : Type l} - β†’ {f : A β†’ B} - β†’ isequiv f - β†’ qinv f -isequiv-to-qinv {l} {A} {B} {f} (mkIsEquiv g g-id h h-id) = - let - Ξ³ : g ∼ h - Ξ³ x = (sym (h-id (g x))) βˆ™ ap h (g-id x) - - Ξ² : (g ∘ f) ∼ id - Ξ² x = Ξ³ (f x) βˆ™ h-id x - in - mkQinv g g-id Ξ² -``` - -### Definition 2.4.11 - -``` -_≃_ : {l1 l2 : Level} β†’ (A : Type l1) (B : Type l2) β†’ Type (l1 βŠ” l2) -A ≃ B = Ξ£ (A β†’ B) isequiv -``` - -### Lemma 2.4.12 - -``` -module lemma2βˆ™4βˆ™12 where - id-equiv : {l : Level} β†’ (A : Type l) β†’ A ≃ A - id-equiv A = id , qinv-to-isequiv (mkQinv id (Ξ» _ β†’ refl) (Ξ» _ β†’ refl)) - - sym-equiv : {A B : Type} β†’ (f : A ≃ B) β†’ B ≃ A - sym-equiv {A} {B} (f , eqv) = - let (mkQinv g Ξ± Ξ²) = isequiv-to-qinv eqv - in g , qinv-to-isequiv (mkQinv f Ξ² Ξ±) - - -- trans-equiv : {A B C : Type} β†’ (f : A ≃ B) β†’ (g : B ≃ C) β†’ A ≃ C - -- trans-equiv {A} {B} {C} (f , f-eqv) (g , g-eqv) = - -- let - -- (mkQinv f-inv f-inv-left f-inv-right) = isequiv-to-qinv f-eqv - -- (mkQinv g-inv g-inv-left g-inv-right) = isequiv-to-qinv g-eqv - - -- open ≑-Reasoning - - -- forward : ((g ∘ f) ∘ (f-inv ∘ g-inv)) ∼ id - -- forward c = - -- begin - -- ((g ∘ f) ∘ (f-inv ∘ g-inv)) c β‰‘βŸ¨ ap (Ξ» f β†’ f c) (composite-assoc (f-inv ∘ g-inv) f g) ⟩ - -- (g ∘ (f ∘ f-inv) ∘ g-inv) c β‰‘βŸ¨ ap g (f-inv-left (g-inv c)) ⟩ - -- (g ∘ id ∘ g-inv) c β‰‘βŸ¨βŸ© - -- (g ∘ g-inv) c β‰‘βŸ¨ g-inv-left c ⟩ - -- id c ∎ - - -- backward : ((f-inv ∘ g-inv) ∘ (g ∘ f)) ∼ id - -- backward a = - -- begin - -- ((f-inv ∘ g-inv) ∘ (g ∘ f)) a β‰‘βŸ¨ ap (Ξ» f β†’ f a) (composite-assoc (g ∘ f) g-inv f-inv) ⟩ - -- (f-inv ∘ (g-inv ∘ (g ∘ f))) a β‰‘βŸ¨ ap f-inv (g-inv-right (f a)) ⟩ - -- (f-inv ∘ (id ∘ f)) a β‰‘βŸ¨βŸ© - -- (f-inv ∘ f) a β‰‘βŸ¨ f-inv-right a ⟩ - -- id a ∎ - - -- in {! !} - -- in g ∘ f , qinv-to-isequiv (mkQinv (f-inv ∘ g-inv) forward backward) -``` - -### Lemma 2.9.2 - -``` -happly : {A B : Type} - β†’ {f g : A β†’ B} - β†’ (p : f ≑ g) - β†’ (x : A) - β†’ f x ≑ g x -happly {A} {B} {f} {g} p x = ap (Ξ» h β†’ h x) p - -happlyd : {A : Type} {B : A β†’ Type} - β†’ {f g : (a : A) β†’ B a} - β†’ (p : f ≑ g) - β†’ (x : A) - β†’ f x ≑ g x -happlyd {A} {B} {f} {g} p x = ap (Ξ» h β†’ h x) p -``` - -### Theorem 2.9.3 (Function extensionality) - -``` -funext : {l : Level} {A B : Type l} - β†’ {f g : A β†’ B} - β†’ ((x : A) β†’ f x ≑ g x) - β†’ f ≑ g -funext h i x = h x i -``` - -## 2.10 Universes and the univalence axiom - -### Lemma 2.10.1 - -``` --- idtoeqv : {l : Level} {A B : Type l} --- β†’ (A ≑ B) --- β†’ (A ≃ B) --- idtoeqv {l} {A} {B} p = transport {! !} {! !} {! p !} , qinv-to-isequiv (mkQinv {! !} {! !} {! !}) -``` - -### Axiom 2.10.3 (Univalence) - -``` -module axiom2βˆ™10βˆ™3 where - -- Glue : βˆ€ {l l2} (A : Type l) - -- β†’ {Ο† : I} - -- β†’ (Te : Partial Ο† (Ξ£ (Type l2) (Ξ» T β†’ T ≃ A))) - -- β†’ Type l2 - - postulate - -- TODO: Provide the definition for this after reading CCHM - ua : {l : Level} {A B : Type l} β†’ (A ≃ B) β†’ (A ≑ B) - - -- forward : {l : Level} {A B : Type l} β†’ (eqv : A ≃ B) β†’ (idtoeqv ∘ ua) eqv ≑ eqv - -- -- forward eqv = {! !} - - -- backward : {l : Level} {A B : Type l} β†’ (p : A ≑ B) β†’ (ua ∘ idtoeqv) p ≑ p - -- -- backward p = {! !} - - -- ua-eqv : {l : Level} {A : Type l} {B : Type l} β†’ (A ≃ B) ≃ (A ≑ B) - -- ua-eqv = ua , qinv-to-isequiv (mkQinv idtoeqv backward forward) - -open axiom2βˆ™10βˆ™3 -``` - -### Theorem 2.11.2 - -``` --- module lemma2βˆ™11βˆ™2 where --- open ≑-Reasoning - --- i : {l : Level} {A : Type l} {a x1 x2 : A} --- β†’ (p : x1 ≑ x2) --- β†’ (q : a ≑ x1) --- β†’ transport (Ξ» y β†’ a ≑ y) p q ≑ q βˆ™ p --- i {l} {A} {a} {x1} {x2} p q j = {! !} - --- ii : {l : Level} {A : Type l} {a x1 x2 : A} --- β†’ (p : x1 ≑ x2) --- β†’ (q : x1 ≑ a) --- β†’ transport (Ξ» y β†’ y ≑ a) p q ≑ sym p βˆ™ q --- ii {l} {A} {a} {x1} {x2} p q = {! !} - --- iii : {l : Level} {A : Type l} {a x1 x2 : A} --- β†’ (p : x1 ≑ x2) --- β†’ (q : x1 ≑ x1) --- β†’ transport (Ξ» y β†’ y ≑ y) p q ≑ sym p βˆ™ q βˆ™ p --- iii {l} {A} {a} {x1} {x2} p q = {! !} -``` - -### Remark 2.12.6 - -``` -module remark2βˆ™12βˆ™6 where - trueβ‰’false : true β‰’ false - trueβ‰’false p = genBot tt - where - Bmap : 𝟚 β†’ Type - Bmap true = πŸ™ - Bmap false = βŠ₯ - - genBot : πŸ™ β†’ βŠ₯ - genBot = transport Bmap p -``` \ No newline at end of file diff --git a/src/CubicalHott/Chapter2Lemma221.lagda.md b/src/CubicalHott/Chapter2Lemma221.lagda.md deleted file mode 100644 index 279e053..0000000 --- a/src/CubicalHott/Chapter2Lemma221.lagda.md +++ /dev/null @@ -1,20 +0,0 @@ -``` -{-# OPTIONS --no-load-primitives --cubical #-} -module CubicalHott.Chapter2Lemma221 where - -open import CubicalHott.Chapter1 -``` - -## Lemma 2.2.1 - -[//]: <> (ANCHOR: ap) - -``` -ap : {l1 l2 : Level} {A : Type l1} {B : Type l2} {x y : A} - β†’ (f : A β†’ B) - β†’ (p : x ≑ y) - β†’ f x ≑ f y -ap {l1} {l2} {A} {B} {x} {y} f p i = f (p i) -``` - -[//]: <> (ANCHOR_END: ap) \ No newline at end of file diff --git a/src/CubicalHott/Chapter2Util.agda b/src/CubicalHott/Chapter2Util.agda deleted file mode 100644 index fd61345..0000000 --- a/src/CubicalHott/Chapter2Util.agda +++ /dev/null @@ -1,22 +0,0 @@ -{-# OPTIONS --no-load-primitives --cubical #-} - -module CubicalHott.Chapter2Util where - -open import CubicalHott.Primitives -open import CubicalHott.CoreUtil -open import CubicalHott.Chapter1 -open import CubicalHott.Chapter2 - -Bool : βˆ€ {l} β†’ Type l -Bool = Lift 𝟚 - -Bool-neg : βˆ€ {l} β†’ Bool {l} β†’ Bool {l} -Bool-neg (lift true) = lift false -Bool-neg (lift false) = lift true - -Bool-neg-homotopy : βˆ€ {l} β†’ (Bool-neg {l} ∘ Bool-neg {l}) ∼ id -Bool-neg-homotopy (lift true) = refl -Bool-neg-homotopy (lift false) = refl - -Bool-neg-equiv : βˆ€ {l} β†’ Bool {l} ≃ Bool {l} -Bool-neg-equiv = Bool-neg , qinv-to-isequiv (mkQinv Bool-neg Bool-neg-homotopy Bool-neg-homotopy) \ No newline at end of file diff --git a/src/CubicalHott/Chapter3.lagda.md b/src/CubicalHott/Chapter3.lagda.md deleted file mode 100644 index da0d289..0000000 --- a/src/CubicalHott/Chapter3.lagda.md +++ /dev/null @@ -1,106 +0,0 @@ -``` -{-# OPTIONS --no-load-primitives --cubical #-} -module CubicalHott.Chapter3 where - -open import CubicalHott.Chapter1 -open import CubicalHott.Chapter2 -open import CubicalHott.Chapter2Util -open import CubicalHott.CoreUtil -``` - -### Definition 3.1.1 - -``` -isSet : {l : Level} (A : Type l) β†’ Type l -isSet A = (x y : A) β†’ (p q : x ≑ y) β†’ p ≑ q -``` - -### Example 3.1.9 - -``` -example3βˆ™1βˆ™9 : βˆ€ {l : Level} β†’ Β¬ (isSet (Type l)) -example3βˆ™1βˆ™9 p = remark2βˆ™12βˆ™6.trueβ‰’false lol - where - open axiom2βˆ™10βˆ™3 - - f-path : Bool ≑ Bool - f-path = ua Bool-neg-equiv - - bogus : id ≑ Bool-neg - bogus = - let - helper : f-path ≑ refl - helper = p Bool Bool f-path refl - - wtf : idtoeqv f-path ≑ idtoeqv refl - wtf = ap idtoeqv helper - - wtf2 : Ξ£.fst (idtoeqv (ua Bool-neg-equiv)) ≑ id - wtf2 = ap Ξ£.fst wtf - - wtf3 : Ξ£.fst (idtoeqv (ua Bool-neg-equiv)) ≑ Bool-neg - wtf3 = ap Ξ£.fst (propositional-computation Bool-neg-equiv) - - wtf4 : Bool-neg ≑ id - wtf4 = sym wtf3 βˆ™ wtf2 - in {! !} - - lol : true ≑ false - lol = ap (Ξ» f β†’ Lift.lower (f (lift true))) bogus -``` - -### Definition 3.3.1 - -``` -isProp : (P : Type) β†’ Type -isProp P = (x y : P) β†’ x ≑ y -``` - -## 3.7 Propositional truncation - -``` -module section3βˆ™7 where - data βˆ₯_βˆ₯ (A : Type) : Type where - ∣_∣ : (a : A) β†’ βˆ₯ A βˆ₯ - witness : (x y : βˆ₯ A βˆ₯) β†’ x ≑ y - - rec-βˆ₯_βˆ₯ : (A : Type) β†’ {B : Type} β†’ isProp B β†’ (f : A β†’ B) - β†’ Ξ£ (βˆ₯ A βˆ₯ β†’ B) (Ξ» g β†’ (a : A) β†’ g (∣ a ∣) ≑ f a) - rec-βˆ₯ A βˆ₯ {B} BisProp f = g , Ξ» _ β†’ refl - where - g : βˆ₯ A βˆ₯ β†’ B - g ∣ a ∣ = f a - g (witness x y i) = BisProp (g x) (g y) i -open section3βˆ™7 -``` - -## 3.8 The axiom of choice - -### Equation 3.8.1 (axiom of choice AC) - -``` -postulate - AC : {X : Type} {A : X β†’ Type} {P : (x : X) β†’ A x β†’ Type} - β†’ ((x : X) β†’ βˆ₯ Ξ£ (A x) (Ξ» a β†’ P x a) βˆ₯) - β†’ βˆ₯ Ξ£ ((x : X) β†’ A x) (Ξ» g β†’ (x : X) β†’ P x (g x)) βˆ₯ -``` - -### Lemma 3.8.5 - -``` -``` - -## 3.9 The principle of unique choice - -### Lemma 3.9.1 - -``` -lemma3βˆ™9βˆ™1 : {P : Type} β†’ isProp P β†’ P ≃ βˆ₯ P βˆ₯ -lemma3βˆ™9βˆ™1 {P} Pprop = ∣_∣ , qinv-to-isequiv (mkQinv inv {! !} {! !}) - where - inv : βˆ₯ P βˆ₯ β†’ P - inv ∣ a ∣ = a - inv (witness p q i) = - let what = ap βˆ₯_βˆ₯ {! !} - in {! !} -``` \ No newline at end of file diff --git a/src/CubicalHott/Chapter6.lagda.md b/src/CubicalHott/Chapter6.lagda.md deleted file mode 100644 index ea3f2fd..0000000 --- a/src/CubicalHott/Chapter6.lagda.md +++ /dev/null @@ -1,95 +0,0 @@ -``` -{-# OPTIONS --no-load-primitives --cubical #-} -module CubicalHott.Chapter6 where - -open import CubicalHott.Chapter1 -open import CubicalHott.Chapter2 - -private - variable - l : Level -``` - -## 6.3 The interval - -``` -data Iv : Type where - 0I : Iv - 1I : Iv - seg : 0I ≑ 1I -``` - -### Lemma 6.3.1 - -``` -isContr : (A : Type l) β†’ Type l -isContr A = Ξ£ A (Ξ» a β†’ (x : A) β†’ a ≑ x) - -lemma6βˆ™3βˆ™1 : isContr Iv -lemma6βˆ™3βˆ™1 = 1I , f - where - f : (x : Iv) β†’ 1I ≑ x - f 0I = sym seg - f 1I = refl - f (seg i) j = {! !} -``` - -### Lemma 6.3.2 - -``` -``` - -## 6.4 Circles and spheres - -``` -data SΒΉ : Type where - base : SΒΉ - loop : base ≑ base -``` - -### Lemma 6.4.1 - -``` -lemma6βˆ™4βˆ™1 : loop β‰’ refl --- lemma6βˆ™4βˆ™1 p = --- {! !} --- where --- open ≑-Reasoning - --- f : {A : Type} (x : A) β†’ (p : x ≑ x) β†’ SΒΉ β†’ A --- f x p base = x --- f x p (loop i) = p i - --- bad : {A : Type} (x : A) β†’ (p : x ≑ x) β†’ p ≑ refl --- bad x p = begin --- p β‰‘βŸ¨ {! !} ⟩ --- p β‰‘βŸ¨ {! !} ⟩ --- refl ∎ -``` - -### Lemma 6.4.2 - -``` -lemma6βˆ™4βˆ™2 : Ξ£ ((x : SΒΉ) β†’ x ≑ x) (Ξ» y β†’ y β‰’ (Ξ» x β†’ refl)) --- lemma6βˆ™4βˆ™2 = f , g --- where --- f : (x : SΒΉ) β†’ x ≑ x --- f base = loop --- f (loop i) i₁ = loop {! !} - --- g : f β‰’ (Ξ» x β†’ refl) --- g p = let --- z = happlyd p --- z2 = z base --- z3 = lemma6βˆ™4βˆ™1 z2 --- in z3 -``` - -``` -circle-is-contractible : isContr SΒΉ -circle-is-contractible = base , f - where - f : (x : SΒΉ) β†’ base ≑ x - f base = refl - f (loop i) j = {! !} -``` \ No newline at end of file diff --git a/src/CubicalHott/CoreUtil.agda b/src/CubicalHott/CoreUtil.agda deleted file mode 100644 index df03a43..0000000 --- a/src/CubicalHott/CoreUtil.agda +++ /dev/null @@ -1,9 +0,0 @@ -{-# OPTIONS --no-load-primitives --cubical #-} - -module CubicalHott.CoreUtil where - -open import CubicalHott.Primitives - -record Lift {a β„“} (A : Type a) : Type (a βŠ” β„“) where - constructor lift - field lower : A diff --git a/src/CubicalHott/Primitives.agda b/src/CubicalHott/Primitives.agda deleted file mode 100644 index 8898faa..0000000 --- a/src/CubicalHott/Primitives.agda +++ /dev/null @@ -1,6 +0,0 @@ -{-# OPTIONS --no-load-primitives --cubical #-} -module CubicalHott.Primitives where - -open import CubicalHott.Primitives.Interval public -open import CubicalHott.Primitives.Kan public -open import CubicalHott.Primitives.Type public \ No newline at end of file diff --git a/src/CubicalHott/Primitives/Interval.lagda.md b/src/CubicalHott/Primitives/Interval.lagda.md deleted file mode 100644 index bc29ffa..0000000 --- a/src/CubicalHott/Primitives/Interval.lagda.md +++ /dev/null @@ -1,83 +0,0 @@ -``` -{-# OPTIONS --no-load-primitives --cubical #-} -module CubicalHott.Primitives.Interval where - -open import CubicalHott.Primitives.Type -``` - -The interval type, and its associated operations, are also very magical. - -``` -{-# BUILTIN CUBEINTERVALUNIV IUniv #-} -- IUniv : SSet₁ -{-# BUILTIN INTERVAL I #-} -- I : IUniv -``` - -Note that the interval (as of Agda 2.6.3) is in its own sort, IUniv. The reason for this is that the interval can serve as the domain of fibrant types: - -``` -_ : Type β†’ Type -_ = Ξ» A β†’ (I β†’ A) -``` - -The interval has two endpoints, the builtins IZERO and IONE: - -``` -{-# BUILTIN IZERO i0 #-} -{-# BUILTIN IONE i1 #-} -``` - -It also supports a De Morgan algebra structure. Unlike the other built-in symbols, the operations on the interval are defined as primitive, so we must use renaming to give them usable names. - -``` -private module X where - infix 30 primINeg - infixr 20 primIMin primIMax - primitive - primIMin : I β†’ I β†’ I - primIMax : I β†’ I β†’ I - primINeg : I β†’ I -open X public - renaming ( primIMin to _∧_ - ; primIMax to _∨_ - ; primINeg to ~_ - ) -``` - -The IsOne predicate - -To specify the shape of composition problems, Cubical Agda gives us the predicate IsOne, which can be thought of as an embedding Iβ†ͺΞ© of the interval object into the subobject classifier. Of course, we have that IsOne i0 is uninhabited (since 0 is not 1), but note that assuming a term in IsOne i0 collapses the judgemental equality. - -``` -{-# BUILTIN ISONE IsOne #-} -- IsOne : I β†’ SetΟ‰ - -postulate - 1=1 : IsOne i1 - leftIs1 : βˆ€ i j β†’ IsOne i β†’ IsOne (i ∨ j) - rightIs1 : βˆ€ i j β†’ IsOne j β†’ IsOne (i ∨ j) - -{-# BUILTIN ITISONE 1=1 #-} -{-# BUILTIN ISONE1 leftIs1 #-} -{-# BUILTIN ISONE2 rightIs1 #-} -``` - -The IsOne proposition is used as the domain of the type Partial, where Partial Ο† A is a refinement of the type .(IsOne Ο†) β†’ A1, where inhabitants p, q : Partial Ο† A are equal iff they agree on a decomposition of Ο† into DNF. - -``` -{-# BUILTIN PARTIAL Partial #-} -{-# BUILTIN PARTIALP PartialP #-} - -postulate - isOneEmpty : βˆ€ {β„“} {A : Partial i0 (Type β„“)} β†’ PartialP i0 A - -primitive - primPOr : βˆ€ {β„“} (i j : I) {A : Partial (i ∨ j) (Type β„“)} - β†’ (u : PartialP i (Ξ» z β†’ A (leftIs1 i j z))) - β†’ (v : PartialP j (Ξ» z β†’ A (rightIs1 i j z))) - β†’ PartialP (i ∨ j) A - -{-# BUILTIN ISONEEMPTY isOneEmpty #-} - -syntax primPOr Ο† ψ u v = [ Ο† ↦ u , ψ ↦ v ] -``` - -Note that the type of primPOr is incomplete: it looks like the eliminator for a coproduct, but i ∨ j behaves more like a pushout. We can represent the accurate type with extension types. \ No newline at end of file diff --git a/src/CubicalHott/Primitives/Kan.lagda.md b/src/CubicalHott/Primitives/Kan.lagda.md deleted file mode 100644 index dcaf63b..0000000 --- a/src/CubicalHott/Primitives/Kan.lagda.md +++ /dev/null @@ -1,48 +0,0 @@ -``` -{-# OPTIONS --no-load-primitives --cubical #-} -module CubicalHott.Primitives.Kan where - -open import CubicalHott.Primitives.Type -open import CubicalHott.Primitives.Interval - -private module X where primitive - primTransp : βˆ€ {β„“} (A : (i : I) β†’ Type (β„“ i)) (Ο† : I) (a : A i0) β†’ A i1 - primHComp : βˆ€ {β„“} {A : Type β„“} {Ο† : I} (u : βˆ€ i β†’ Partial Ο† A) (a : A) β†’ A - primComp : βˆ€ {β„“} (A : (i : I) β†’ Type (β„“ i)) {Ο† : I} (u : βˆ€ i β†’ Partial Ο† (A i)) (a : A i0) β†’ A i1 - -open X public renaming (primTransp to transp) - -hcomp - : βˆ€ {β„“} {A : Type β„“} (Ο† : I) - β†’ (u : (i : I) β†’ Partial (Ο† ∨ ~ i) A) - β†’ A -hcomp Ο† u = X.primHComp (Ξ» j .o β†’ u j (leftIs1 Ο† (~ j) o)) (u i0 1=1) - -βˆ‚ : I β†’ I -βˆ‚ i = i ∨ ~ i - -comp - : βˆ€ {β„“ : I β†’ Level} (A : (i : I) β†’ Type (β„“ i)) (Ο† : I) - β†’ (u : (i : I) β†’ Partial (Ο† ∨ ~ i) (A i)) - β†’ A i1 -comp A Ο† u = X.primComp A (Ξ» j .o β†’ u j (leftIs1 Ο† (~ j) o)) (u i0 1=1) -``` - -We also define the type of dependent paths, and of non-dependent paths. - -``` -postulate - PathP : βˆ€ {β„“} (A : I β†’ Type β„“) β†’ A i0 β†’ A i1 β†’ Type β„“ - -{-# BUILTIN PATHP PathP #-} - -infix 4 _≑_ - -Path : βˆ€ {β„“} (A : Type β„“) β†’ A β†’ A β†’ Type β„“ -Path A = PathP (Ξ» i β†’ A) - -_≑_ : βˆ€ {β„“} {A : Type β„“} β†’ A β†’ A β†’ Type β„“ -_≑_ {A = A} = Path A - -{-# BUILTIN PATH _≑_ #-} -``` diff --git a/src/CubicalHott/Primitives/Type.lagda.md b/src/CubicalHott/Primitives/Type.lagda.md deleted file mode 100644 index b56e305..0000000 --- a/src/CubicalHott/Primitives/Type.lagda.md +++ /dev/null @@ -1,36 +0,0 @@ -``` -{-# OPTIONS --no-load-primitives --cubical #-} -module CubicalHott.Primitives.Type where -``` - -Primitives: Sorts - -This module defines bindings for the primitive sorts in Agda. These are very magic symbols since they bootstrap everything about the type system. For more details about the use of universes, see 1Lab.Type. - -``` -{-# BUILTIN TYPE Type #-} -{-# BUILTIN SETOMEGA TypeΟ‰ #-} - -{-# BUILTIN PROP Prop #-} -{-# BUILTIN PROPOMEGA PropΟ‰ #-} - -{-# BUILTIN STRICTSET SSet #-} -{-# BUILTIN STRICTSETOMEGA SSetΟ‰ #-} -``` - -Additionally, we have the Level type, of universe levels. The universe levels are an algebra containing 0, closed under successor and maximum. The difference between this and e.g. the natural numbers is that Level isn’t initial, i.e. you can’t pattern-match on it. - -``` -postulate - Level : Type - lzero : Level - lsuc : Level β†’ Level - _βŠ”_ : Level β†’ Level β†’ Level -infixl 6 _βŠ”_ - -{-# BUILTIN LEVELUNIV LevelUniv #-} -{-# BUILTIN LEVEL Level #-} -{-# BUILTIN LEVELZERO lzero #-} -{-# BUILTIN LEVELSUC lsuc #-} -{-# BUILTIN LEVELMAX _βŠ”_ #-} -```