Added templates and some code done
This commit is contained in:
@@ -0,0 +1,3 @@
|
||||
module 0Trinitarianism.Preambles.P0 where
|
||||
|
||||
open import Cubical.Foundations.Prelude hiding (_∨_) public
|
||||
@@ -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)
|
||||
@@ -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)
|
||||
@@ -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 (⊥)
|
||||
@@ -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
|
||||
@@ -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)
|
||||
@@ -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 : ℕ → ℕ
|
||||
@@ -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₁))
|
||||
@@ -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)
|
||||
@@ -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
|
||||
@@ -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
|
||||
@@ -0,0 +1,3 @@
|
||||
module 0Trinitarianism.Quest5 where
|
||||
|
||||
open import 0Trinitarianism.Preambles.P5
|
||||
@@ -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
|
||||
@@ -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
|
||||
@@ -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
|
||||
@@ -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
|
||||
@@ -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' = {!!}
|
||||
|
||||
-}
|
||||
|
||||
@@ -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 = {!!}
|
||||
@@ -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 = {!!}
|
||||
@@ -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.
|
||||
|
||||
-}
|
||||
@@ -0,0 +1,3 @@
|
||||
module 1FundamentalGroup.Quest3 where
|
||||
|
||||
open import 1FundamentalGroup.Preambles.P3
|
||||
@@ -0,0 +1,9 @@
|
||||
name: Heated-Gaming
|
||||
include: .
|
||||
depend: cubical
|
||||
flags:
|
||||
--cubical
|
||||
--guardedness
|
||||
--no-import-sorts
|
||||
-W noUnsupportedIndexedMatch
|
||||
--allow-unsolved-metas
|
||||
Reference in New Issue
Block a user