remove cubical hott folder
This commit is contained in:
parent
491b1b87b0
commit
e0f6ba0477
12 changed files with 1 additions and 849 deletions
4
.vscode/settings.json
vendored
4
.vscode/settings.json
vendored
|
|
@ -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"
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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
|
||||
```
|
||||
|
|
@ -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
|
||||
```
|
||||
|
|
@ -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)
|
||||
|
|
@ -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)
|
||||
|
|
@ -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 {! !}
|
||||
```
|
||||
|
|
@ -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 = {! !}
|
||||
```
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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.
|
||||
|
|
@ -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 _≡_ #-}
|
||||
```
|
||||
|
|
@ -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 _⊔_ #-}
|
||||
```
|
||||
Loading…
Reference in a new issue