From 565a7b19d9ab226d6b1d2c833b236303104f071c Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Mon, 8 May 2023 18:56:59 -0500 Subject: [PATCH] Add some notes --- src/2023-04-03-more-ch2.agda | 173 ++++++++++++++++++++++++++++++---- src/2023-05-06-equiv.lagda.md | 130 +++++++++++++++++++++++++ src/Simple.agda | 21 ++++- 3 files changed, 305 insertions(+), 19 deletions(-) create mode 100644 src/2023-05-06-equiv.lagda.md diff --git a/src/2023-04-03-more-ch2.agda b/src/2023-04-03-more-ch2.agda index cd1c462..d9b9ec8 100644 --- a/src/2023-04-03-more-ch2.agda +++ b/src/2023-04-03-more-ch2.agda @@ -1,8 +1,19 @@ -- {{{ open import Agda.Builtin.Equality +open import Agda.Builtin.Sigma open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) renaming (Set to Type) 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 open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst) @@ -71,6 +82,23 @@ apd {A} {B} f {x} {y} p = in 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 r x p -l212-obv-proof-3 : {A : Type} → lemma-212 -l212-obv-proof-3 {A} x y z p q = +l212-pairwise-1-2 : {A : Type} → (x y z : A) → (x ≡ y) → (y ≡ z) + → l212-obv-proof-1 ≡ l212-obv-proof-2 +l212-pairwise-1-2 {A} x y z p q = let - f : (y z : A) → (q : y ≡ z) → (x : A) → x ≡ y → x ≡ z - f = ? - r = f y z q - - 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 - ? + left-proof = l212-obv-proof-1 x y z p q + right-proof = l212-obv-proof-2 x y z p q + in ? -- Exercise 2.3: Give a fourth, different proof of Lemma 2.1.2, and prove it -- 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 -- path in a type A, simultaneously with the type of boundaries of such paths -data nPath {A : Type} : ℕ → Type where - zeroPath : (x y : A) → (p : x ≡ y) → nPath zero - sucPath : {n : ℕ} → (nPath n) +-- p : (2 ≡ 1 + 1) +-- p = refl +-- +-- 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 -- 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) → -- (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, -- (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₁ = {! !} + + + + + + + + + + + + + diff --git a/src/2023-05-06-equiv.lagda.md b/src/2023-05-06-equiv.lagda.md new file mode 100644 index 0000000..8fcd82d --- /dev/null +++ b/src/2023-05-06-equiv.lagda.md @@ -0,0 +1,130 @@ ++++ +title = "Equivalences" +slug = "equivalences" +date = 2023-05-06 +tags = ["type-theory", "agda", "hott"] +math = true +draft = true ++++ + +
+ Imports + +``` +{-# OPTIONS --cubical #-} + +open import Agda.Primitive.Cubical +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Prelude +open import Data.Bool +``` + +
+ +``` +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 diff --git a/src/Simple.agda b/src/Simple.agda index c9249a7..0fcedae 100644 --- a/src/Simple.agda +++ b/src/Simple.agda @@ -1,13 +1,15 @@ {-# OPTIONS --cubical #-} 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.Foundations.Equiv using (isEquiv; equivProof; equiv-proof) open import Relation.Nullary using (¬_) open import Relation.Binary.Core using (Rel) open import Data.Nat +open import Data.Bool + sanity : 1 + 1 ≡ 2 sanity = refl @@ -38,3 +40,20 @@ sanity = refl -- _[_;_]′ -- 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