From 1a06c10bb5ae754df7138605bf34bff4269449a0 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Sun, 15 Sep 2024 17:39:30 -0500 Subject: [PATCH] updates --- .gitignore | 6 +- src/CubicalHott/Chapter2.agda | 32 +++++++++- .../Agda/Exercises/02-Exercises.lagda.md | 54 +++++++++-------- src/Hurewicz.agda | 2 - src/Log.lagda.md | 60 +++++++++++++++++++ 5 files changed, 123 insertions(+), 31 deletions(-) delete mode 100644 src/Hurewicz.agda create mode 100644 src/Log.lagda.md diff --git a/.gitignore b/.gitignore index f7454a2..c7ce020 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,7 @@ *.agdai .DS_Store -node_modules \ No newline at end of file +node_modules + +logseq +!logseq/custom.edn +!logseq/custom.css \ No newline at end of file diff --git a/src/CubicalHott/Chapter2.agda b/src/CubicalHott/Chapter2.agda index 31fe5ef..b9f0e97 100644 --- a/src/CubicalHott/Chapter2.agda +++ b/src/CubicalHott/Chapter2.agda @@ -28,9 +28,35 @@ module lemma214 where q : y ≡ z r : z ≡ w - lemma-i : p ≡ p ∙ refl - lemma-i = hfill {! !} {! !} {! !} - + -- https://agda.readthedocs.io/en/v2.7.0/language/cubical.html#homogeneous-composition + lemma-i1 : p ≡ p ∙ refl + lemma-i1 {l} {A} {x} {y} {p} j i = hfill {φ = ~ i ∨ i ∨ ~ j} (λ k → λ where + (i = i0) → x + (i = i1) → y + (j = i0) → p i + ) + -- (p ≡ p ∙ refl) [ _φ_99 ↦ ?0 i0 ] + -- this is an element of p ≡ p ∙ refl s.t this element definitionally equals ?0 i0 when φ = φ₀ + -- to construct this, use inS, since ?0 i0 is automatically an element of this type + (inS (p i)) + -- I, the axis that's being hfilled + j + + lemma-i2 : p ≡ refl ∙ p + -- Breaking down refl ∙ p + -- refl ∙ p ≡ refl ∙∙ refl ∙∙ p + -- ≡ hcomp (doubleComp-faces refl p i) (refl i) + -- ≡ hcomp (λ j → λ { (i = i0) → refl (~ j) ; (i = i1) → p j }) x + -- ≡ hcomp (λ j → λ { (i = i0) → x ; (i = i1) → p j }) x + lemma-i2 {l} {A} {x} {y} {p} j i = hfill (λ _ → λ where + (i = i0) → x + (i = i1) → p i + ) + (inS (p i)) + {! i !} + + lemma-ii1 : (sym p) ∙ p ≡ refl + module lemma2310 where lemma : {A B : Type l} → (P : B → Type l2) diff --git a/src/HoTTEST/Agda/Exercises/02-Exercises.lagda.md b/src/HoTTEST/Agda/Exercises/02-Exercises.lagda.md index fd52330..4db345e 100644 --- a/src/HoTTEST/Agda/Exercises/02-Exercises.lagda.md +++ b/src/HoTTEST/Agda/Exercises/02-Exercises.lagda.md @@ -49,38 +49,44 @@ But what do they say under the propositions-as-types interpretation? Consider the following goals: ```agda [i] : {A B C : Type} → (A × B) ∔ C → (A ∔ C) × (B ∔ C) -[i] = {!!} +[i] (inl (x , y)) = inl x , inl y +[i] (inr x) = inr x , inr x [ii] : {A B C : Type} → (A ∔ B) × C → (A × C) ∔ (B × C) -[ii] = {!!} +[ii] (inl x , y) = inl (x , y) +[ii] (inr x , y) = inr (x , y) [iii] : {A B : Type} → ¬ (A ∔ B) → ¬ A × ¬ B -[iii] = {!!} +[iii] x = (λ p → x (inl p)) , λ p → x (inr p) -[iv] : {A B : Type} → ¬ (A × B) → ¬ A ∔ ¬ B -[iv] = {!!} +postulate + [iv] : {A B : Type} → ¬ (A × B) → ¬ A ∔ ¬ B + -- Not possible [v] : {A B : Type} → (A → B) → ¬ B → ¬ A -[v] = {!!} +[v] f nb a = nb (f a) -[vi] : {A B : Type} → (¬ A → ¬ B) → B → A -[vi] = {!!} +postulate + [vi] : {A B : Type} → (¬ A → ¬ B) → B → A + -- Not possible -[vii] : {A B : Type} → ((A → B) → A) → A -[vii] = {!!} +postulate + [vii] : {A B : Type} → ((A → B) → A) → A + -- Not possible [viii] : {A : Type} {B : A → Type} → ¬ (Σ a ꞉ A , B a) → (a : A) → ¬ B a -[viii] = {!!} +[viii] ns a ba = ns (a , ba) -[ix] : {A : Type} {B : A → Type} - → ¬ ((a : A) → B a) → (Σ a ꞉ A , ¬ B a) -[ix] = {!!} +postulate + [ix] : {A : Type} {B : A → Type} + → ¬ ((a : A) → B a) → (Σ a ꞉ A , ¬ B a) + -- Not possible [x] : {A B : Type} {C : A → B → Type} → ((a : A) → (Σ b ꞉ B , C a b)) → Σ f ꞉ (A → B) , ((a : A) → C a (f a)) -[x] = {!!} +[x] x = (λ a → pr₁ (x a)) , λ a → pr₂ (x a) ``` For each goal determine whether it is provable or not. If it is, fill it. If not, explain why it shouldn't be possible. @@ -100,7 +106,7 @@ In the lecture we have discussed that we can't prove `∀ {A : Type} → ¬¬ A What you can prove however, is ```agda tne : ∀ {A : Type} → ¬¬¬ A → ¬ A -tne = {!!} +tne nnna a = nnna λ p → p a ``` @@ -111,14 +117,10 @@ Prove ¬¬-functor f ¬¬A ¬B = ¬¬A (λ A → ¬B (f A)) ¬¬-kleisli : {A B : Type} → (A → ¬¬ B) → ¬¬ A → ¬¬ B -¬¬-kleisli = {!!} +¬¬-kleisli f ¬¬A ¬B = ¬¬A λ a → f a ¬B ``` Hint: For the second goal use `tne` from the previous exercise - - - - ## Part II: `_≡_` for `Bool` **In this exercise we want to investigate what equality of booleans looks like. @@ -129,11 +131,13 @@ In particular we want to show that for `true false : Bool` we have `true ≢ fal Under the propositions-as-types paradigm, an inhabited type corresponds to a true proposition while an uninhabited type corresponds to a false proposition. With this in mind construct a family + ```agda bool-as-type : Bool → Type bool-as-type true = 𝟙 -bool-as-type false = {! 𝟘 !} +bool-as-type false = 𝟘 ``` + such that `bool-as-type true` corresponds to "true" and `bool-as-type false` corresponds to "false". (Hint: we have seen canonical types corresponding true and false in the lectures) @@ -144,7 +148,7 @@ we have seen canonical types corresponding true and false in the lectures) Prove ```agda bool-≡-char₁ : ∀ (b b' : Bool) → b ≡ b' → (bool-as-type b ⇔ bool-as-type b') -bool-≡-char₁ b b' p = (λ x → {! !}) , λ x → {! !} +bool-≡-char₁ b b' p = (λ x → transport bool-as-type p x) , λ x → transport bool-as-type (sym p) x ``` @@ -153,7 +157,7 @@ bool-≡-char₁ b b' p = (λ x → {! !}) , λ x → {! !} Using ex. 2, conclude that ```agda true≢false : ¬ (true ≡ false) -true≢false () +true≢false p = pr₁ (bool-≡-char₁ true false p) ⋆ ``` You can actually prove this much easier! How? @@ -163,7 +167,7 @@ You can actually prove this much easier! How? Finish our characterisation of `_≡_` by proving ```agda bool-≡-char₂ : ∀ (b b' : Bool) → (bool-as-type b ⇔ bool-as-type b') → b ≡ b' -bool-≡-char₂ = {!!} +bool-≡-char₂ b b' (l , r) = {! !} ``` diff --git a/src/Hurewicz.agda b/src/Hurewicz.agda deleted file mode 100644 index 06773e1..0000000 --- a/src/Hurewicz.agda +++ /dev/null @@ -1,2 +0,0 @@ -module Hurewicz where - diff --git a/src/Log.lagda.md b/src/Log.lagda.md new file mode 100644 index 0000000..ca40feb --- /dev/null +++ b/src/Log.lagda.md @@ -0,0 +1,60 @@ +``` +{-# OPTIONS --cubical #-} + +module Log where + +open import Cubical.Foundations.Prelude +``` + +## 2024-09-12 + +Trying to get hcomp to work + +``` +module log-20240912 where + private + variable + l : Level + A : Type l + x y z w : A + p : x ≡ y + q : y ≡ z + r : z ≡ w + s : w ≡ x + + -- Order of the square is + -- 4 + -- +----->+ + -- ^ ^ + -- 1 | | 2 + -- | | + -- +----->+ + -- 3 + -- In this below case, i is the vertical dimension and j is the horizontal dimension + test-square : Square refl refl p p + test-square {l} {A} {x} {y} {p} i j = p i + + -- Creating the same square with hfill + test-square2 : p ∙ refl ≡ p + test-square2 {l} {A} {x} {y} {p} i j = hfill (λ k → λ where + (j = i0) → x + (j = i1) → y + ) + -- A [ ~ j ∨ j ↦ (λ { (j = i0) → x ; (j = i1) → y }) ] + -- looking for some expression s.t when φ = i1, will equal the thing in the expression + (inS (p j)) + (~ i) + + -- Trying to port over the 1lab filler + -- This fills a square + ∙∙-filler : Square s q p (sym s ∙∙ p ∙∙ q) + ∙∙-filler {l} {A} {x} {y} {z} {w} {p} {q} {s} i j = hfill (λ k → λ where + (j = i0) → {! s (~ i) !} + (j = i1) → {! !} + ) + {! !} {! i !} +``` + +Question: +- How many sides do you need for the hcomp to be correct? +- What direction, semantically, is the last argument to hfill? \ No newline at end of file