From 0fd49a19e9f9641f98458bb3af99c3ae59e9e753 Mon Sep 17 00:00:00 2001 From: pingu Date: Sun, 8 Feb 2026 12:32:06 +0100 Subject: [PATCH] Added templates and some code done --- 0Trinitarianism/Preambles/P0.agda | 3 + 0Trinitarianism/Preambles/P1.agda | 6 ++ 0Trinitarianism/Preambles/P2.agda | 6 ++ 0Trinitarianism/Preambles/P3.agda | 6 ++ 0Trinitarianism/Preambles/P4.agda | 5 ++ 0Trinitarianism/Preambles/P5.agda | 33 +++++++++++ 0Trinitarianism/Quest0.agda | 20 +++++++ 0Trinitarianism/Quest1.agda | 21 +++++++ 0Trinitarianism/Quest2.agda | 31 +++++++++++ 0Trinitarianism/Quest3.agda | 39 +++++++++++++ 0Trinitarianism/Quest4.agda | 38 +++++++++++++ 0Trinitarianism/Quest5.agda | 3 + 1FundamentalGroup/Preambles/P0.agda | 12 ++++ 1FundamentalGroup/Preambles/P1.agda | 12 ++++ 1FundamentalGroup/Preambles/P2.agda | 19 +++++++ 1FundamentalGroup/Preambles/P3.agda | 33 +++++++++++ 1FundamentalGroup/Quest0.agda | 64 ++++++++++++++++++++++ 1FundamentalGroup/Quest1.agda | 35 ++++++++++++ 1FundamentalGroup/Quest1SideQuests/Sn.agda | 23 ++++++++ 1FundamentalGroup/Quest2.agda | 27 +++++++++ 1FundamentalGroup/Quest3.agda | 3 + Heated-Gaming.agda-lib | 9 +++ 22 files changed, 448 insertions(+) create mode 100644 0Trinitarianism/Preambles/P0.agda create mode 100644 0Trinitarianism/Preambles/P1.agda create mode 100644 0Trinitarianism/Preambles/P2.agda create mode 100644 0Trinitarianism/Preambles/P3.agda create mode 100644 0Trinitarianism/Preambles/P4.agda create mode 100644 0Trinitarianism/Preambles/P5.agda create mode 100644 0Trinitarianism/Quest0.agda create mode 100644 0Trinitarianism/Quest1.agda create mode 100644 0Trinitarianism/Quest2.agda create mode 100644 0Trinitarianism/Quest3.agda create mode 100644 0Trinitarianism/Quest4.agda create mode 100644 0Trinitarianism/Quest5.agda create mode 100644 1FundamentalGroup/Preambles/P0.agda create mode 100644 1FundamentalGroup/Preambles/P1.agda create mode 100644 1FundamentalGroup/Preambles/P2.agda create mode 100644 1FundamentalGroup/Preambles/P3.agda create mode 100644 1FundamentalGroup/Quest0.agda create mode 100644 1FundamentalGroup/Quest1.agda create mode 100644 1FundamentalGroup/Quest1SideQuests/Sn.agda create mode 100644 1FundamentalGroup/Quest2.agda create mode 100644 1FundamentalGroup/Quest3.agda create mode 100644 Heated-Gaming.agda-lib diff --git a/0Trinitarianism/Preambles/P0.agda b/0Trinitarianism/Preambles/P0.agda new file mode 100644 index 0000000..b5c024d --- /dev/null +++ b/0Trinitarianism/Preambles/P0.agda @@ -0,0 +1,3 @@ +module 0Trinitarianism.Preambles.P0 where + +open import Cubical.Foundations.Prelude hiding (_∨_) public diff --git a/0Trinitarianism/Preambles/P1.agda b/0Trinitarianism/Preambles/P1.agda new file mode 100644 index 0000000..d45b0cf --- /dev/null +++ b/0Trinitarianism/Preambles/P1.agda @@ -0,0 +1,6 @@ +module 0Trinitarianism.Preambles.P1 where + +open import Cubical.Foundations.Prelude public +open import Cubical.Data.Unit public renaming (Unit to ⊤) +open import Cubical.Data.Empty public using (⊥) +open import Cubical.Data.Nat public hiding (isEven) diff --git a/0Trinitarianism/Preambles/P2.agda b/0Trinitarianism/Preambles/P2.agda new file mode 100644 index 0000000..8512c91 --- /dev/null +++ b/0Trinitarianism/Preambles/P2.agda @@ -0,0 +1,6 @@ +module 0Trinitarianism.Preambles.P2 where + +open import Cubical.Foundations.Prelude public +open import Cubical.Data.Unit public renaming (Unit to ⊤) +open import Cubical.Data.Empty public using (⊥) +open import Cubical.Data.Nat public hiding (isEven) diff --git a/0Trinitarianism/Preambles/P3.agda b/0Trinitarianism/Preambles/P3.agda new file mode 100644 index 0000000..89fd299 --- /dev/null +++ b/0Trinitarianism/Preambles/P3.agda @@ -0,0 +1,6 @@ +module 0Trinitarianism.Preambles.P3 where + +open import Cubical.Foundations.Prelude public +open import Cubical.Data.Nat public hiding (_+_ ; isEven) +open import 0Trinitarianism.Quest1 public +open import Cubical.Data.Empty public using (⊥) diff --git a/0Trinitarianism/Preambles/P4.agda b/0Trinitarianism/Preambles/P4.agda new file mode 100644 index 0000000..52a0250 --- /dev/null +++ b/0Trinitarianism/Preambles/P4.agda @@ -0,0 +1,5 @@ +module 0Trinitarianism.Preambles.P4 where + +open import Cubical.Foundations.Prelude using + ( Level ; Type ; _≡_ ; J ; JRefl ; refl ; i1 ; i0 ; I ; cong) public +open import Cubical.Foundations.Isomorphism renaming (Iso to _≅_) public diff --git a/0Trinitarianism/Preambles/P5.agda b/0Trinitarianism/Preambles/P5.agda new file mode 100644 index 0000000..6aa8889 --- /dev/null +++ b/0Trinitarianism/Preambles/P5.agda @@ -0,0 +1,33 @@ +module 0Trinitarianism.Preambles.P5 where + +open import Cubical.Foundations.Prelude renaming + (funExt to libFunExt ; + sym to libSym ; + _∎ to lib_∎ ; + _∙_ to lib_∙_ ; + fst to libFst ; + snd to libSnd + ) hiding ( step-≡ ) public +open import Cubical.HITs.S1 using ( S¹ ; base ; loop ) public +open import Cubical.Foundations.Isomorphism renaming (Iso to _≅_) public +open import Cubical.Foundations.Path public +open import 0Trinitarianism.Quest4Solutions public +open import 1FundamentalGroup.Quest0Solutions public +open import Cubical.Data.Bool public + +pathToFun≡transport : {u : Level} {A B : Type u} (p : A ≡ B) (x : A) + → pathToFun p x ≡ transport p x +pathToFun≡transport {u} {A} = J (λ B p → (x : A) → pathToFun p x ≡ transport p x) + λ x → + pathToFun refl x + ≡⟨ pathToFunReflx x ⟩ + x + ≡⟨ sym (transportRefl x) ⟩ + transport refl x ∎ + +PathPIsoPathD : {u : Level} {A B : Type u} (p : A ≡ B) (x : A) (y : B) → + (PathP (λ i → p i) x y) ≅ (pathToFun p x ≡ y) +PathPIsoPathD {u} {A} {B} p x = + subst (λ b → (y : B) → (PathP (λ i → p i) x y) ≅ (b ≡ y)) + (sym (pathToFun≡transport p x)) + (PathPIsoPath _ x) diff --git a/0Trinitarianism/Quest0.agda b/0Trinitarianism/Quest0.agda new file mode 100644 index 0000000..f704e57 --- /dev/null +++ b/0Trinitarianism/Quest0.agda @@ -0,0 +1,20 @@ +module 0Trinitarianism.Quest0 where +open import 0Trinitarianism.Preambles.P0 + +data ⊤ : Type where + tt : ⊤ + +TrueToTrue : ⊤ → ⊤ +TrueToTrue = λ x → x + +TrueToTrue' : ⊤ → ⊤ +TrueToTrue' tt = tt + +data ⊥ : Type where + +explosion : ⊥ → ⊤ +explosion () + +data ℕ : Type where + zero : ℕ + suc : ℕ → ℕ diff --git a/0Trinitarianism/Quest1.agda b/0Trinitarianism/Quest1.agda new file mode 100644 index 0000000..23708fd --- /dev/null +++ b/0Trinitarianism/Quest1.agda @@ -0,0 +1,21 @@ +module 0Trinitarianism.Quest1 where + +open import 0Trinitarianism.Preambles.P1 + +isEven : ℕ → Type +isEven zero = ⊤ +isEven (suc zero) = ⊥ +isEven (suc (suc n)) = isEven n + +{- +This is a comment block. +Remove this comment block and formulate +'there exists an even natural' here. +-} + +_×_ : Type → Type → Type +A × C = Σ A (λ a → C) + +div2 : Σ ℕ isEven → ℕ +div2 (zero , snd₁) = zero +div2 (suc (suc fst₁) , snd₁) = suc (div2 (fst₁ , snd₁)) diff --git a/0Trinitarianism/Quest2.agda b/0Trinitarianism/Quest2.agda new file mode 100644 index 0000000..fab09bb --- /dev/null +++ b/0Trinitarianism/Quest2.agda @@ -0,0 +1,31 @@ +module 0Trinitarianism.Quest2 where + +open import 0Trinitarianism.Preambles.P2 + +isEven : ℕ → Type +isEven zero = ⊤ +isEven (suc zero) = ⊥ +isEven (suc (suc n)) = isEven n + +{- +This is a comment block. +Remove this comment block and formulate +'there exists an even natural' here. +-} + +_×_ : Type → Type → Type +A × C = Σ A (λ a → C) + +div2 : Σ ℕ isEven → ℕ +div2 (zero , snd₁) = zero +div2 (suc (suc fst₁) , snd₁) = suc (div2 ( fst₁ , snd₁)) + +private + postulate + A B C : Type + +uncurry : (A → B → C) → (A × B → C) +uncurry f x = f (fst x) (snd x) + +curry : (A × B → C) → (A → B → C) +curry f a b = f (a , b) diff --git a/0Trinitarianism/Quest3.agda b/0Trinitarianism/Quest3.agda new file mode 100644 index 0000000..db286cb --- /dev/null +++ b/0Trinitarianism/Quest3.agda @@ -0,0 +1,39 @@ +module 0Trinitarianism.Quest3 where + +open import 0Trinitarianism.Preambles.P3 + +_+_ : ℕ → ℕ → ℕ +n + zero = n +n + suc m = suc (n + m) + +_+'_ : ℕ → ℕ → ℕ +zero +' m = m +suc n +' m = suc (n +' m) + +{- +Write here your proof that the sum of +even naturals is even. +-} + +SumOfEven : (x y : Σ ℕ isEven) → isEven (x .fst + y .fst) +SumOfEven x@(fst₁ , snd₁) (zero , snd₂) = snd₁ +SumOfEven x@(fst₁ , snd₁) (suc (suc fst₂) , snd₂) = SumOfEven x ( fst₂ , snd₂) + +data _⊕_ (A B : Type) : Type where + inl : A → A ⊕ B + inr : B → A ⊕ B + +_⇔_ : Type → Type → Type +A ⇔ B = (A → B) × (B → A) + +ex : {A : Type} → (A ⇔ ⊥) ⇔ (A → ⊥) +ex .fst = λ z → z .fst +ex .snd = λ x → x , λ () + +¬ : Type → Type +¬ A = A → ⊥ + +proof : (x : ℕ) → (isEven x) ⊕ (¬ (isEven x)) +proof zero = inl tt +proof (suc zero) = inr (λ ()) +proof (suc (suc x)) = proof x diff --git a/0Trinitarianism/Quest4.agda b/0Trinitarianism/Quest4.agda new file mode 100644 index 0000000..1b90617 --- /dev/null +++ b/0Trinitarianism/Quest4.agda @@ -0,0 +1,38 @@ +module 0Trinitarianism.Quest4 where + +open import 0Trinitarianism.Preambles.P4 + +data Id {A : Type} : (x y : A) → Type where + rfl : {x : A} → Id x x + +private + variable + A : Type + x y z w : A + +sym : Id x y → Id y x +sym rfl = rfl + +trans : Id x y → Id y z → Id x z +trans rfl rfl = rfl + +_*_ : Id x y → Id y z → Id x z +_*_ = trans + +rfl* : (p : Id x y) → Id (rfl * p) p +rfl* rfl = rfl + +*rfl : (p : Id x y) → Id (p * rfl) p +*rfl rfl = rfl + +*sym : (p : Id x y) → Id (sym p * p) rfl +*sym rfl = rfl + +sym* : (p : Id x y) → Id (p * sym p) rfl +sym* rfl = rfl + +assoc : (p : Id x y) (q : Id y z) (r : Id z w) → Id ((p * q) * r) (p * (q * r)) +assoc rfl rfl rfl = rfl + +outOfId : (M : (y : A) → Id x y → Type) → M x rfl → {y : A} → (p : Id x y) → M y p +outOfId M x rfl = x diff --git a/0Trinitarianism/Quest5.agda b/0Trinitarianism/Quest5.agda new file mode 100644 index 0000000..89b7aaf --- /dev/null +++ b/0Trinitarianism/Quest5.agda @@ -0,0 +1,3 @@ +module 0Trinitarianism.Quest5 where + +open import 0Trinitarianism.Preambles.P5 diff --git a/1FundamentalGroup/Preambles/P0.agda b/1FundamentalGroup/Preambles/P0.agda new file mode 100644 index 0000000..f79c339 --- /dev/null +++ b/1FundamentalGroup/Preambles/P0.agda @@ -0,0 +1,12 @@ +module 1FundamentalGroup.Preambles.P0 where + +open import Cubical.Data.Empty using (⊥) public +open import Cubical.Data.Unit renaming ( Unit to ⊤ ) public +open import Cubical.Data.Bool renaming ( elim to Bool-elim ) public +open import Cubical.Foundations.Prelude + renaming ( subst to endPt + ; transport to pathToFun + ) public +open import Cubical.Foundations.Isomorphism renaming ( Iso to _≅_ ) public +open import Cubical.Foundations.Path public +open import Cubical.HITs.S1 renaming ( elim to S¹-elim ) public diff --git a/1FundamentalGroup/Preambles/P1.agda b/1FundamentalGroup/Preambles/P1.agda new file mode 100644 index 0000000..0c9c2a7 --- /dev/null +++ b/1FundamentalGroup/Preambles/P1.agda @@ -0,0 +1,12 @@ +module 1FundamentalGroup.Preambles.P1 where + +open import Cubical.HITs.S1 using (S¹ ; base ; loop) public +open import Cubical.Data.Nat using (ℕ ; suc ; zero) public +open import Cubical.Data.Int using (ℤ ; pos ; negsuc ; -_) public +open import Cubical.Data.Empty public +open import Cubical.Foundations.Prelude + renaming ( subst to endPt + ; transport to pathToFun + ) public +open import Cubical.Foundations.Isomorphism renaming (Iso to _≅_) public +open import 1FundamentalGroup.Quest0Solutions using ( Refl ; Refl≢loop ) public diff --git a/1FundamentalGroup/Preambles/P2.agda b/1FundamentalGroup/Preambles/P2.agda new file mode 100644 index 0000000..78e8513 --- /dev/null +++ b/1FundamentalGroup/Preambles/P2.agda @@ -0,0 +1,19 @@ +module 1FundamentalGroup.Preambles.P2 where + +open import Cubical.Data.Nat public +open import Cubical.Data.Int using (ℤ ; pos ; negsuc ; -_) public +open import Cubical.Foundations.Isomorphism renaming (Iso to _≅_) public +open import Cubical.Data.Empty using (⊥) public +open import Cubical.Data.Unit renaming (Unit to ⊤) public +open import Cubical.Foundations.Prelude + renaming ( subst to endPt + ; transport to pathToFun + ) public +open import Cubical.HITs.S1 using (S¹ ; base ; loop) public +open import 1FundamentalGroup.Quest1Solutions public + +refl∙refl : {A : Type} {a : A} → refl ∙ refl ≡ refl {x = a} +refl∙refl {a = a} = sym (λ i j → compPath-filler (refl {x = a}) refl i j) + +symRefl : {A : Type} {a : A} → sym refl ≡ refl {x = a} +symRefl = refl diff --git a/1FundamentalGroup/Preambles/P3.agda b/1FundamentalGroup/Preambles/P3.agda new file mode 100644 index 0000000..02a167e --- /dev/null +++ b/1FundamentalGroup/Preambles/P3.agda @@ -0,0 +1,33 @@ +module 1FundamentalGroup.Preambles.P3 where + +open import Cubical.Foundations.Prelude public + renaming (transport to pathToFun ; + transportRefl to pathToFunRefl ; + subst to endPt) public +open import Cubical.Foundations.Isomorphism renaming (Iso to _≅_) public +open import Cubical.Foundations.GroupoidLaws + renaming (lCancel to sym∙ ; rCancel to ∙sym ; lUnit to Refl∙ ; rUnit to ∙Refl) public +open import Cubical.Foundations.Path public +open import Cubical.Data.Int using (ℤ ; isSetℤ) public +open import Cubical.Data.Nat public +open import Cubical.HITs.S1 using ( S¹ ; base ; loop ) public +open import 1FundamentalGroup.Quest1Solutions public + +open ℤ public + +PathD : {A0 A1 : Type} (A : A0 ≡ A1) (x : A0) (y : A1) → Type +PathD A x y = pathToFun A x ≡ y + +endPtRefl : {A : Type} {x : A} (B : A → Type) → endPt B (refl {x = x}) ≡ λ b → b +endPtRefl {x = x} B = funExt (λ b → substRefl {B = B} b) + +outOfS¹P : (B : S¹ → Type) (b : B base) → PathP (λ i → B (loop i)) b b → (x : S¹) → B x +outOfS¹P B b p base = b +outOfS¹P B b p (loop i) = p i + +outOfS¹D : (B : S¹ → Type) (b : B base) → PathD (λ i → B (loop i)) b b → (x : S¹) → B x +outOfS¹D B b p x = outOfS¹P B b (_≅_.inv (PathPIsoPath (λ i → B (loop i)) b b) p) x + +outOfS¹DBase : (B : S¹ → Type) (b : B base) + (p : PathD (λ i → B (loop i)) b b) → outOfS¹D B b p base ≡ b +outOfS¹DBase B b p = refl diff --git a/1FundamentalGroup/Quest0.agda b/1FundamentalGroup/Quest0.agda new file mode 100644 index 0000000..869e257 --- /dev/null +++ b/1FundamentalGroup/Quest0.agda @@ -0,0 +1,64 @@ +-- ignore +module 1FundamentalGroup.Quest0 where +open import 1FundamentalGroup.Preambles.P0 + +Refl : base ≡ base +Refl = {!!} + +Flip : Bool → Bool +Flip x = {!!} + +flipIso : Bool ≅ Bool +flipIso = {!!} + +flipPath : Bool ≡ Bool +flipPath = {!!} + +doubleCover : S¹ → Type +doubleCover x = {!!} + +endPtOfTrue : base ≡ base → doubleCover base +endPtOfTrue p = {!!} + +Refl≢loop : Refl ≡ loop → ⊥ +Refl≢loop p = {!!} + +------------------- Side Quest - Empty ------------------------- + +{- +-- This is a comment box, +-- remove the {- and -} to do the side quests + +toEmpty : (A : Type) → Type +toEmpty A = {!!} + +pathEmpty : (A : Type) → Type₁ +pathEmpty A = {!!} + +isoEmpty : (A : Type) → Type +isoEmpty A = {!!} + +outOf⊥ : (A : Type) → ⊥ → A +outOf⊥ A () + +toEmpty→isoEmpty : (A : Type) → toEmpty A → isoEmpty A +toEmpty→isoEmpty A = {!!} + +isoEmpty→pathEmpty : (A : Type) → isoEmpty A → pathEmpty A +isoEmpty→pathEmpty A = {!!} + +pathEmpty→toEmpty : (A : Type) → pathEmpty A → toEmpty A +pathEmpty→toEmpty A = {!!} +-} + +------------------- Side Quests - true≢false -------------------- + +{- +-- This is a comment box, +-- remove the {- and -} to do the side quests + +true≢false' : true ≡ false → ⊥ +true≢false' = {!!} + +-} + diff --git a/1FundamentalGroup/Quest1.agda b/1FundamentalGroup/Quest1.agda new file mode 100644 index 0000000..bb63b46 --- /dev/null +++ b/1FundamentalGroup/Quest1.agda @@ -0,0 +1,35 @@ +-- ignore +module 1FundamentalGroup.Quest1 where +open import 1FundamentalGroup.Preambles.P1 + + +loopSpace : (A : Type) (a : A) → Type +loopSpace A a = a ≡ a + +loop_times : ℤ → loopSpace S¹ base +loop n times = {!!} + +{- +The definition of sucℤ goes here. +-} + +{- +The definition of predℤ goes here. +-} + +{- +The definition of sucℤIso goes here. +-} + +{- +The definition of sucℤPath goes here. +-} + +helix : S¹ → Type +helix = {!!} + +windingNumberBase : base ≡ base → ℤ +windingNumberBase = {!!} + +windingNumber : (x : S¹) → base ≡ x → helix x +windingNumber = {!!} diff --git a/1FundamentalGroup/Quest1SideQuests/Sn.agda b/1FundamentalGroup/Quest1SideQuests/Sn.agda new file mode 100644 index 0000000..13a5b14 --- /dev/null +++ b/1FundamentalGroup/Quest1SideQuests/Sn.agda @@ -0,0 +1,23 @@ +module 1FundamentalGroup.Quest1SideQuests.Sn where + +open import Cubical.Data.Nat +open import Cubical.Data.Empty +open import Cubical.Data.Unit renaming (Unit to ⊤) +open import Cubical.Data.Bool +open import Cubical.Foundations.Prelude + + +data susp (X : Type) : Type where + north : {!!} + south : {!!} + merid : {!!} + +Sphere : ℕ → Type +Sphere = {!!} + +Disk : (n : ℕ) → Type +Disk zero = {!!} +Disk (suc n) = {!!} + +SphereToDisk : {n : ℕ} → Sphere n → Disk n +SphereToDisk {n} s = {!!} diff --git a/1FundamentalGroup/Quest2.agda b/1FundamentalGroup/Quest2.agda new file mode 100644 index 0000000..8bea655 --- /dev/null +++ b/1FundamentalGroup/Quest2.agda @@ -0,0 +1,27 @@ +-- ignore +module 1FundamentalGroup.Quest2 where +open import 1FundamentalGroup.Preambles.P2 + +isSet→LoopSpace≡⊤ : {A : Type} (x : A) → isSet A → (x ≡ x) ≡ ⊤ +isSet→LoopSpace≡⊤ = {!!} + +data _⊔_ (A B : Type) : Type where + + inl : A → A ⊔ B + inr : B → A ⊔ B + +{- + +Your definition of ℤ≡ℕ⊔ℕ goes here. + +Your definition of ⊔NoConfusion goes here. + +Your definition of Path≡⊔NoConfusion goes here. + +Your definition of isSet⊔NoConfusion goes here. + +Your definition of isSet⊔ goes here. + +Your definition of isSetℤ goes here. + +-} diff --git a/1FundamentalGroup/Quest3.agda b/1FundamentalGroup/Quest3.agda new file mode 100644 index 0000000..85bef2d --- /dev/null +++ b/1FundamentalGroup/Quest3.agda @@ -0,0 +1,3 @@ +module 1FundamentalGroup.Quest3 where + +open import 1FundamentalGroup.Preambles.P3 diff --git a/Heated-Gaming.agda-lib b/Heated-Gaming.agda-lib new file mode 100644 index 0000000..742852f --- /dev/null +++ b/Heated-Gaming.agda-lib @@ -0,0 +1,9 @@ +name: Heated-Gaming +include: . +depend: cubical +flags: + --cubical + --guardedness + --no-import-sorts + -W noUnsupportedIndexedMatch + --allow-unsolved-metas