Add some notes
This commit is contained in:
parent
8466f79ecc
commit
565a7b19d9
|
@ -1,8 +1,19 @@
|
||||||
-- {{{
|
-- {{{
|
||||||
|
|
||||||
open import Agda.Builtin.Equality
|
open import Agda.Builtin.Equality
|
||||||
|
open import Agda.Builtin.Sigma
|
||||||
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) renaming (Set to Type)
|
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) renaming (Set to Type)
|
||||||
open import Data.Nat
|
open import Data.Nat
|
||||||
|
open import Data.Product
|
||||||
|
open import Data.Product.Base
|
||||||
|
open import Data.Product.Properties
|
||||||
|
open import Data.Bool
|
||||||
|
|
||||||
|
open import Data.Product using (_,_)
|
||||||
|
open import Function.Base using (_∘_)
|
||||||
|
open import Relation.Binary.Core
|
||||||
|
open import Relation.Binary.Definitions
|
||||||
|
open import Relation.Nullary.Negation.Core using (¬_)
|
||||||
|
|
||||||
import Relation.Binary.PropositionalEquality as Eq
|
import Relation.Binary.PropositionalEquality as Eq
|
||||||
open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst)
|
open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst)
|
||||||
|
@ -71,6 +82,23 @@ apd {A} {B} f {x} {y} p =
|
||||||
in
|
in
|
||||||
path-ind D d x y p
|
path-ind D d x y p
|
||||||
|
|
||||||
|
-- Fibers
|
||||||
|
fiber : {A B : Type} → (f : A → B) → (y : B) → Type
|
||||||
|
fiber {A} {B} f y = Σ[ x ∈ A ] f x ≡ y
|
||||||
|
|
||||||
|
-- Contractibility
|
||||||
|
isContr : Type → Type
|
||||||
|
isContr A = Σ[ x ∈ A ] (∀ y → x ≡ y)
|
||||||
|
|
||||||
|
-- Equivalence
|
||||||
|
record isEquiv {A B : Type} (f : A → B) : Type where
|
||||||
|
field
|
||||||
|
equiv-proof : (y : B) → isContr (fiber f y)
|
||||||
|
open isEquiv
|
||||||
|
|
||||||
|
_≃_ : (A B : Type) → Type
|
||||||
|
A ≃ B = Σ[ f ∈ (A → B) ] (isEquiv f)
|
||||||
|
|
||||||
-- }}}
|
-- }}}
|
||||||
|
|
||||||
-------------------------------------------------------------------------------
|
-------------------------------------------------------------------------------
|
||||||
|
@ -101,20 +129,13 @@ l212-obv-proof-2 {A} x y z p q =
|
||||||
in
|
in
|
||||||
r x p
|
r x p
|
||||||
|
|
||||||
l212-obv-proof-3 : {A : Type} → lemma-212
|
l212-pairwise-1-2 : {A : Type} → (x y z : A) → (x ≡ y) → (y ≡ z)
|
||||||
l212-obv-proof-3 {A} x y z p q =
|
→ l212-obv-proof-1 ≡ l212-obv-proof-2
|
||||||
|
l212-pairwise-1-2 {A} x y z p q =
|
||||||
let
|
let
|
||||||
f : (y z : A) → (q : y ≡ z) → (x : A) → x ≡ y → x ≡ z
|
left-proof = l212-obv-proof-1 x y z p q
|
||||||
f = ?
|
right-proof = l212-obv-proof-2 x y z p q
|
||||||
r = f y z q
|
in ?
|
||||||
|
|
||||||
g : (x y : A) → (p : x ≡ y) → (x ≡ z)
|
|
||||||
g = path-ind
|
|
||||||
(λ a b a≡b → a ≡ z)
|
|
||||||
(λ a → r a ?)
|
|
||||||
s = g x y p
|
|
||||||
in
|
|
||||||
?
|
|
||||||
|
|
||||||
-- Exercise 2.3: Give a fourth, different proof of Lemma 2.1.2, and prove it
|
-- Exercise 2.3: Give a fourth, different proof of Lemma 2.1.2, and prove it
|
||||||
-- equal to the others
|
-- equal to the others
|
||||||
|
@ -132,9 +153,44 @@ l212-obv-proof-4 {A} x y z p q =
|
||||||
-- Exercise 2.4: Define, by induction on n, a general notion of n-dimensional
|
-- Exercise 2.4: Define, by induction on n, a general notion of n-dimensional
|
||||||
-- path in a type A, simultaneously with the type of boundaries of such paths
|
-- path in a type A, simultaneously with the type of boundaries of such paths
|
||||||
|
|
||||||
data nPath {A : Type} : ℕ → Type where
|
-- p : (2 ≡ 1 + 1)
|
||||||
zeroPath : (x y : A) → (p : x ≡ y) → nPath zero
|
-- p = refl
|
||||||
sucPath : {n : ℕ} → (nPath n)
|
--
|
||||||
|
-- q : (2 ≡ 1 + 1)
|
||||||
|
-- q = ?
|
||||||
|
--
|
||||||
|
-- p2 : p ≡ q
|
||||||
|
-- q2 : p ≡ q
|
||||||
|
--
|
||||||
|
-- p3 : p2 ≡ q2
|
||||||
|
--
|
||||||
|
-- nSuc- npath 5
|
||||||
|
|
||||||
|
-- data nPath {A : Type} : ℕ → Type where
|
||||||
|
-- zeroPath : (x y : A) → (p : x ≡ y) → nPath zero
|
||||||
|
-- sucPath : {n : ℕ}
|
||||||
|
-- → (left : nPath n)
|
||||||
|
-- → (right : nPath n)
|
||||||
|
-- → (p : left ≡ right)
|
||||||
|
-- → nPath (suc n)
|
||||||
|
|
||||||
|
-- data nPath : (A : Type) → (x y : A) → Type where
|
||||||
|
-- path-zero : (A : Type) → (x y : A) → (p : x ≡ y) → nPath A x y
|
||||||
|
-- path-suc : (A : Type) → (x y : A)
|
||||||
|
-- → (left : nPath A x y)
|
||||||
|
-- → (right : nPath A x y)
|
||||||
|
-- → (p : left ≡ right)
|
||||||
|
-- → nPath (nPath A x y) left right
|
||||||
|
|
||||||
|
data nPath : Type where
|
||||||
|
|
||||||
|
-- p : nPath ℕ (1 + 1) 2
|
||||||
|
-- p = path-zero ℕ (1 + 1) 2 refl
|
||||||
|
--
|
||||||
|
-- q : nPath ℕ (1 + 1) 2
|
||||||
|
-- q = path-zero ℕ (1 + 1) 2 refl
|
||||||
|
--
|
||||||
|
-- p2 : nPath (nPath ℕ (1 + 1) 2) p q
|
||||||
|
|
||||||
-- Exercise 2.5: Prove that the functions (2.3.6) and (2.3.7) are
|
-- Exercise 2.5: Prove that the functions (2.3.6) and (2.3.7) are
|
||||||
-- inverse-equivalences
|
-- inverse-equivalences
|
||||||
|
@ -153,7 +209,88 @@ f237 {p = p} {f = f} _ = ap f p
|
||||||
-- Exercise 2.6: Prove that if p : x = y, then the function (p ∙ –) : (y = z) →
|
-- Exercise 2.6: Prove that if p : x = y, then the function (p ∙ –) : (y = z) →
|
||||||
-- (x = z) is an equivalence.
|
-- (x = z) is an equivalence.
|
||||||
|
|
||||||
e26 : {A : Type} {x y : A} → (p : x ≡ y) → ?
|
|
||||||
|
|
||||||
-- Exercise 2.9. Prove that coproducts have the expected universal property,
|
-- Exercise 2.9. Prove that coproducts have the expected universal property,
|
||||||
-- (A + B → X) ≃ (A → X) × (B → X).
|
-- (A + B → X) ≃ (A → X) × (B → X).
|
||||||
|
|
||||||
|
-- Exercise 2.13
|
||||||
|
-- Show that (2 ≃ 2) ≃ 2
|
||||||
|
|
||||||
|
-- The fiber of id for the Bool y (aka all x's such that id x ≡ y, which is just
|
||||||
|
-- y)
|
||||||
|
id-fiber-base : (y : Bool) → Σ[ x ∈ Bool ] id x ≡ y
|
||||||
|
proj₁ (id-fiber-base y) = y
|
||||||
|
proj₂ (id-fiber-base y) = refl
|
||||||
|
|
||||||
|
id-fiber-is-contr : (y : Bool) → (y₁ : Σ[ x ∈ Bool ] id x ≡ y) → id-fiber-base y ≡ y₁
|
||||||
|
id-fiber-is-contr y y₁ =
|
||||||
|
let
|
||||||
|
y₁-Bool-equiv = snd y₁
|
||||||
|
|
||||||
|
pair₁ : y ≡ fst y₁
|
||||||
|
pair₁ = sym y₁-Bool-equiv
|
||||||
|
|
||||||
|
snd-fiber : id (fst (id-fiber-base y)) ≡ y
|
||||||
|
snd-fiber = snd (id-fiber-base y)
|
||||||
|
|
||||||
|
pair₂ : subst (λ x → id x ≡ y) pair₁ (snd (id-fiber-base y)) ≡ snd y₁
|
||||||
|
pair₂ =
|
||||||
|
begin
|
||||||
|
subst (λ x → id x ≡ y) pair₁ snd-fiber
|
||||||
|
≡⟨ ? ⟩
|
||||||
|
-- subst : Substitutive {A = A} _≡_ ℓ
|
||||||
|
-- subst P refl p = p
|
||||||
|
-- snd-fiber
|
||||||
|
?
|
||||||
|
≡⟨ ? ⟩
|
||||||
|
snd y₁
|
||||||
|
∎
|
||||||
|
|
||||||
|
pair = pair₁ , pair₂
|
||||||
|
in Σ-≡,≡→≡ pair
|
||||||
|
|
||||||
|
x : Substitutive ? ?
|
||||||
|
x = ?
|
||||||
|
|
||||||
|
-- Σ-≡,≡←≡ : p₁ ≡ p₂ → Σ (a₁ ≡ a₂) (λ p → subst B p b₁ ≡ b₂)
|
||||||
|
-- Σ-≡,≡←≡ refl = refl , refl
|
||||||
|
|
||||||
|
-- A proof that for every y, the fiber of id for that y (which is just going to
|
||||||
|
-- be y itself) is contractible, which means that for every pair of (a, path),
|
||||||
|
-- there needs to be a path between that pair and the pair i gave above in id-fiber-base
|
||||||
|
id-is-contr : (y : Bool) → isContr (fiber id y)
|
||||||
|
proj₁ (id-is-contr y) = id-fiber-base y
|
||||||
|
proj₂ (id-is-contr y) y₁ = id-fiber-is-contr y y₁
|
||||||
|
|
||||||
|
id-is-eqv : isEquiv id
|
||||||
|
id-is-eqv .equiv-proof y = ?
|
||||||
|
|
||||||
|
id-eqv : Bool ≃ Bool
|
||||||
|
proj₁ id-eqv = id
|
||||||
|
proj₂ id-eqv = id-is-eqv
|
||||||
|
|
||||||
|
-- proj₁ (proj₁ (proj₂ id-eqv .equiv-proof y)) = y
|
||||||
|
-- proj₂ (proj₁ (proj₂ id-eqv .equiv-proof y)) = refl
|
||||||
|
-- proj₂ (proj₂ id-eqv .equiv-proof y) y₁ = {! !}
|
||||||
|
|
||||||
|
e213 : (Bool ≃ Bool) ≃ Bool
|
||||||
|
|
||||||
|
e213-helper-1 : (y : Bool) → Σ (Bool ≃ Bool) (λ x → proj₁ e213 x ≡ y)
|
||||||
|
proj₁ (e213-helper-1 y) = {! !}
|
||||||
|
proj₂ (e213-helper-1 y) = {! !}
|
||||||
|
|
||||||
|
proj₁ e213 bool-equiv = (proj₁ bool-equiv) true
|
||||||
|
proj₁ (proj₂ e213 .equiv-proof y) = e213-helper-1 y
|
||||||
|
proj₂ (proj₂ e213 .equiv-proof y) y₁ = {! !}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
130
src/2023-05-06-equiv.lagda.md
Normal file
130
src/2023-05-06-equiv.lagda.md
Normal file
|
@ -0,0 +1,130 @@
|
||||||
|
+++
|
||||||
|
title = "Equivalences"
|
||||||
|
slug = "equivalences"
|
||||||
|
date = 2023-05-06
|
||||||
|
tags = ["type-theory", "agda", "hott"]
|
||||||
|
math = true
|
||||||
|
draft = true
|
||||||
|
+++
|
||||||
|
|
||||||
|
<details>
|
||||||
|
<summary>Imports</summary>
|
||||||
|
|
||||||
|
```
|
||||||
|
{-# OPTIONS --cubical #-}
|
||||||
|
|
||||||
|
open import Agda.Primitive.Cubical
|
||||||
|
open import Cubical.Foundations.Equiv
|
||||||
|
open import Cubical.Foundations.Prelude
|
||||||
|
open import Data.Bool
|
||||||
|
```
|
||||||
|
|
||||||
|
</details>
|
||||||
|
|
||||||
|
```
|
||||||
|
Bool-id : Bool → Bool
|
||||||
|
Bool-id true = true
|
||||||
|
Bool-id false = false
|
||||||
|
|
||||||
|
unap : {A B : Type} {x y : A} (f : A → B) → f x ≡ f y → x ≡ y
|
||||||
|
unap p i = ?
|
||||||
|
|
||||||
|
-- Need to convert point-wise equality into universally quantified equality?
|
||||||
|
Bool-id-refl : (x : Bool) → (Bool-id x ≡ x)
|
||||||
|
Bool-id-refl true = refl
|
||||||
|
Bool-id-refl false = refl
|
||||||
|
```
|
||||||
|
|
||||||
|
The equivalence proof below involves the contractibility-of-fibers definition of
|
||||||
|
an equivalence. There are others, but the "default" one used by the Cubical
|
||||||
|
standard library uses this.
|
||||||
|
|
||||||
|
```
|
||||||
|
Bool-id-is-equiv : isEquiv Bool-id
|
||||||
|
```
|
||||||
|
|
||||||
|
In the contractibility-of-fibers proof, we must first establish our fibers. If
|
||||||
|
we had $(f : A \rightarrow B)$, then this is saying given any $(y : B)$, we must
|
||||||
|
provide:
|
||||||
|
|
||||||
|
- an $(x : A)$ that would have gotten mapped to $y$ (preimage), and
|
||||||
|
- a proof that $f\ x \equiv y$
|
||||||
|
|
||||||
|
These are the two elements of the pair given below. Since our function is `id`,
|
||||||
|
we can just give $y$ again, and use the `refl` function above for the equality
|
||||||
|
proof
|
||||||
|
|
||||||
|
```
|
||||||
|
Bool-id-is-equiv .equiv-proof y .fst = y , Bool-id-refl y
|
||||||
|
```
|
||||||
|
|
||||||
|
The next step is to prove that it's contractible. Using the same derivation for
|
||||||
|
$y$ as above, this involves taking in another fiber $y_1$, and proving that it's
|
||||||
|
equivalent the fiber we've just defined above.
|
||||||
|
|
||||||
|
To prove fiber equality, we can just do point-wise equality over both the
|
||||||
|
preimage of $y$, and then the second-level equality of the proof of $f\ x \equiv
|
||||||
|
y$.
|
||||||
|
|
||||||
|
In the first case here, we need to provide something that equals our $x$ above
|
||||||
|
when $i = i0$, and something that equals the fiber $y_1$'s preimage $x_1$ when
|
||||||
|
$i = i1$, aka $y \equiv proj_1\ y_1$.
|
||||||
|
|
||||||
|
```
|
||||||
|
Bool-id-is-equiv .equiv-proof y .snd y₁ i .fst =
|
||||||
|
let
|
||||||
|
eqv = snd y₁
|
||||||
|
-- eqv : Bool-id (fst y₁) ≡ y
|
||||||
|
|
||||||
|
eqv2 = eqv ∙ sym (Bool-id-refl y)
|
||||||
|
-- eqv2 : Bool-id (fst y₁) ≡ Bool-id y
|
||||||
|
|
||||||
|
-- Ok, unap doesn't actually exist unless f is known to have an inverse.
|
||||||
|
-- Fortunately, because we're proving an equivalence, we know that f has an
|
||||||
|
-- inverse, in particular going from y to x, which in thise case is also y.
|
||||||
|
eqv3 = unap Bool-id eqv2
|
||||||
|
|
||||||
|
Bool-id-inv : Bool → Bool
|
||||||
|
Bool-id-inv b = (((Bool-id-is-equiv .equiv-proof) b) .fst) .fst
|
||||||
|
|
||||||
|
eqv3′ = cong Bool-id-inv eqv2
|
||||||
|
give-me-info = ?
|
||||||
|
-- eqv3 : fst y₁ ≡ y
|
||||||
|
|
||||||
|
-- https://git.mzhang.io/school/cubical/issues/1
|
||||||
|
eqv4′ = ?
|
||||||
|
eqv4 = sym eqv3
|
||||||
|
-- eqv4 : y ≡ fst y₁
|
||||||
|
in
|
||||||
|
eqv4 i
|
||||||
|
```
|
||||||
|
|
||||||
|
Now we can prove that the path is the same
|
||||||
|
|
||||||
|
\begin{CD}
|
||||||
|
A @> > > B \\\
|
||||||
|
@VVV @VVV \\\
|
||||||
|
C @> > > D
|
||||||
|
\end{CD}
|
||||||
|
|
||||||
|
- $A \rightarrow B$ is the path of the original fiber that we've specified, which is $f\ x \equiv y$
|
||||||
|
- $C \rightarrow D$ is the path of the other fiber that we're proving, which is $proj_2\ y_1$
|
||||||
|
|
||||||
|
So what we want now is `a-b ≡ c-d`
|
||||||
|
|
||||||
|
```
|
||||||
|
Bool-id-is-equiv .equiv-proof y .snd y₁ i .snd j =
|
||||||
|
let
|
||||||
|
a-b = Bool-id-refl y
|
||||||
|
c-d = y₁ .snd
|
||||||
|
in
|
||||||
|
|
||||||
|
-- https://git.mzhang.io/school/cubical/issues/2
|
||||||
|
?
|
||||||
|
```
|
||||||
|
|
||||||
|
## Other Equivalences
|
||||||
|
|
||||||
|
There are 2 other ways we can define equivalences:
|
||||||
|
|
||||||
|
TODO: Talk about them being equivalent to each other
|
|
@ -1,13 +1,15 @@
|
||||||
{-# OPTIONS --cubical #-}
|
{-# OPTIONS --cubical #-}
|
||||||
|
|
||||||
open import Cubical.Foundations.Prelude
|
open import Cubical.Foundations.Prelude
|
||||||
using (_≡_; refl; _∙_; _≡⟨_⟩_; _∎; cong; sym; fst; snd; _,_; ~_)
|
using (_≡_; refl; _∙_; _∎; cong; sym; fst; snd; _,_; ~_)
|
||||||
open import Cubical.Data.Empty as ⊥
|
open import Cubical.Data.Empty as ⊥
|
||||||
open import Cubical.Foundations.Equiv using (isEquiv; equivProof; equiv-proof)
|
open import Cubical.Foundations.Equiv using (isEquiv; equivProof; equiv-proof)
|
||||||
open import Relation.Nullary using (¬_)
|
open import Relation.Nullary using (¬_)
|
||||||
open import Relation.Binary.Core using (Rel)
|
open import Relation.Binary.Core using (Rel)
|
||||||
open import Data.Nat
|
open import Data.Nat
|
||||||
|
|
||||||
|
open import Data.Bool
|
||||||
|
|
||||||
sanity : 1 + 1 ≡ 2
|
sanity : 1 + 1 ≡ 2
|
||||||
sanity = refl
|
sanity = refl
|
||||||
|
|
||||||
|
@ -38,3 +40,20 @@ sanity = refl
|
||||||
-- _[_;_]′
|
-- _[_;_]′
|
||||||
-- a [ 34 ; b ]
|
-- a [ 34 ; b ]
|
||||||
--
|
--
|
||||||
|
|
||||||
|
|
||||||
|
x : Bool
|
||||||
|
x = true
|
||||||
|
|
||||||
|
-- _&&_ : Bool → Bool → Bool
|
||||||
|
|
||||||
|
-- (x && true) : Bool
|
||||||
|
|
||||||
|
|
||||||
|
p : 2 + 3 ≡ 3 + 2
|
||||||
|
p = refl
|
||||||
|
|
||||||
|
-- _+_ : Nat → Nat → Nat
|
||||||
|
-- zero + m = m
|
||||||
|
-- suc n + m = suc (n + m)
|
||||||
|
p2 : (x y : ℕ) → x + y ≡ y + x
|
||||||
|
|
Loading…
Reference in a new issue