auto gitdoc commit
This commit is contained in:
parent
f68001e728
commit
c642f47288
4 changed files with 196 additions and 167 deletions
|
|
@ -17,7 +17,6 @@ open import Agda.Primitive
|
|||
```
|
||||
data 𝟙 : Set where
|
||||
tt : 𝟙
|
||||
|
||||
```
|
||||
|
||||
## 1.6 Dependent pair types (Σ-types)
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
```
|
||||
|
|
|
|||
|
|
@ -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
|
||||
```
|
||||
|
|
|
|||
|
|
@ -1,8 +0,0 @@
|
|||
module HottBook.Common where
|
||||
|
||||
open import Relation.Binary.PropositionalEquality using (trans)
|
||||
|
||||
Type = Set
|
||||
|
||||
infixr 6 _∙_
|
||||
_∙_ = trans
|
||||
Loading…
Reference in a new issue