updates

.gitignore

@@ -1,3 +1,7 @@
 *.agdai
 .DS_Store
-node_modules
+node_modules
+
+logseq
+!logseq/custom.edn
+!logseq/custom.css

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)

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) = {!   !}
 ```
 
 

src/Hurewicz.agda

@@ -1,2 +0,0 @@
-module Hurewicz where
-

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?