waht

.vscode/settings.json

@@ -0,0 +1,3 @@
+{
+  "editor.unicodeHighlight.ambiguousCharacters": false
+}

src/2023-11-27-asdf.agda

@@ -0,0 +1,13 @@
+module 2023-11-27-asdf where
+
+open import Relation.Binary.Core
+open import Relation.Binary.Definitions
+open import Relation.Binary.PropositionalEquality as Eq
+
+postulate
+    S1 : Set
+    base : S1
+    loop : base ≡ base
+
+asdf : (c : S1)
+    → ((x : A) → x ≡ c)

src/2023-12-21-some-group-theory-shit.agda

@@ -0,0 +1,15 @@
+{-# OPTIONS --cubical #-}
+-- http://jesse.jaksin14.angelfire.com/Proofs/Group_Theory.pdf
+
+open import Agda.Primitive hiding (Prop)
+
+open import Cubical.Core.Everything
+
+is-Semigroup : (l : Level) → (S : Type l) → Type l
+is-Semigroup l S = Σ[ mul ∈ (S → S → S) ] ((x y z : S) → mul (mul x y) z ≡ mul x (mul y z))
+
+Semigroup : (l : Level) → Type (lsuc l)
+Semigroup l = Σ[ G ∈ Type l ] (is-Semigroup l G)
+
+is-Group : (l : Level) → (S : Semigroup l) → Type l
+is-Group l S = {!   !}

src/CubicalHott/Chapter1Exercises.agda

@@ -0,0 +1,31 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Chapter1Exercises where
+
+open import Cubical.Core.Everything
+open import Cubical.Core.Primitives public
+open import Data.Empty
+
+refl : {ℓ : Level} {A : Set ℓ} {x : A} → Path A x x
+refl {x = x} = λ i → x
+
+-- Exercise 1.1. Given functions f : A → B and g : B → C, define their composite g ◦ f : A → C. Show that we have h ◦ (g ◦ f ) ≡ (h ◦ g) ◦ f .
+infix 10 _∘_
+_∘_ : {A B C : Set} → (g : B → C) → (f : A → B) → A → C
+(g ∘ f) a = g (f a)
+
+exercise-1-1 : {A B C D : Set}
+  → (f : A → B)
+  → (g : B → C)
+  → (h : C → D)
+  → h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f
+exercise-1-1 f g h = refl {x = h ∘ (g ∘ f)}
+
+-- TODO: Explain how this works
+
+-- Exercise 1.11. Show that for any type A, we have ¬¬¬A → ¬A.
+¬_ : (A : Set) → Set
+¬ A = ⊥
+
+exercise-1-11 : {A : Set} → ¬ (¬ (¬ A)) → ¬ A
+exercise-1-11 ()

src/CubicalHott/Chapter2.lagda.md

@@ -0,0 +1,69 @@
+```
+{-# OPTIONS --cubical #-}
+module CubicalHott.Chapter2 where
+open import Cubical.Core.Everything
+```
+
+# 2.1 Types are higher groupoids
+
+```
+lemma-2-1-2 : {A : Set}
+  → {x y z : A}
+  → x ≡ y
+  → y ≡ z
+  → x ≡ z
+lemma-2-1-2 {A} {x} p q i = hcomp (λ j → λ { (i = i0) → x ; (i = i1) → q j }) (p i)
+
+_∙_ = lemma-2-1-2
+```
+
+# 2.2 Functions are functors
+
+```
+lemma-2-2-1 : {A B : Set} {x y : A}
+  → (f : A → B)
+  → x ≡ y
+  → f x ≡ f y
+lemma-2-2-1 f p i = f (p i)
+
+ap = lemma-2-2-1
+```
+
+# 2.4 Homotopies and equivalences
+
+```
+definition-2-4-1 : {A : Set} {P : A → Set}
+  → (f g : (x : A) → P x)
+  → Set
+definition-2-4-1 {A} f g = (x : A) → f x ≡ g x
+
+_∼_ = definition-2-4-1
+
+lemma-2-4-2-1 : {A : Set} {P : A → Set}
+  → (f : (x : A) → P x)
+  → f ∼ f
+lemma-2-4-2-1 f x i = f x
+
+lemma-2-4-2-2 : {A : Set} {P : A → Set}
+  → (f g : (x : A) → P x)
+  → (f∼g : f ∼ g)
+  → g ∼ f
+lemma-2-4-2-2 f g f∼g x i = f∼g x (~ i)
+
+lemma-2-4-2-3 : {A : Set} {P : A → Set}
+  → (f g h : (x : A) → P x)
+  → (f∼g : f ∼ g)
+  → (g∼h : g ∼ h)
+  → f ∼ h
+lemma-2-4-2-3 {A} f g h f∼g g∼h x = (f∼g x) ∙ (g∼h x)
+-- TODO: Wtf how does this work?
+
+lemma-2-4-3 : {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)
+lemma-2-4-3 f g H {x} {y} p i =
+  {!   !}
+```

src/CubicalHott/Chapter2Exercises.agda

@@ -0,0 +1,8 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Chapter2Exercises where
+
+-- 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 for such paths.
+
+-- Exercise 2.13. Show that (2 ≃ 2) ≃ 2.