Complete 1FundamentalGroup/Quest1.agda

Fix tiny typo in Quest3.agda

0Trinitarianism/Quest3.agda

@@ -6,6 +6,6 @@ _+_ : ℕ → ℕ → ℕ
 n + m = {!!}
 
 {-
-Write here you proof that the sum of
+Write here your proof that the sum of
 even naturals is even.
 -}

0Trinitarianism/bin/AsProps/Quest0.agda

@@ -1,216 +0,0 @@
-module Trinitarianism.AsProps.Quest0 where
-open import Trinitarianism.AsProps.Quest0Preamble
-
-{-
-  Here are some things that we could like to have in a logical framework
-  * Propositions (with the data of proofs)
-  * Objects to reason about with propositions
-
-  To make propositions we want
-  * False ⊥
-  * True ⊤
-  * Or ∨
-  * And ∧
-  * Implication →
-
-  but propositions are useless if they're not talking about anything,
-  so we also want
-  * Predicates
-  * Exists ∃
-  * For all ∀
-  * Equality ≡ (of objects)
--}
-
--- Here is how we define 'true'
-data ⊤ : Prop where
-  trivial : ⊤
-
-{- It reads '⊤ is a proposition and there is a proof of it, called "trivial"'. -}
-
--- Here is how we define 'false'
-data ⊥ : Prop where
-
-{- This says that ⊥ is the proposition where there are no proofs of it. -}
-
-{-
-Given two propositions P and Q, we can form a new proposition 'P implies Q'
-written P → Q
-To introduce a proof of P → Q we assume a proof x of P and give a proof y of Q
-
-Here is an example demonstrating → in action
--}
-
-TrueToTrue : ⊤ → ⊤
-TrueToTrue = ?
-
-{-
-  * press C-c C-l (this means Ctrl-c Ctrl-l) to load the document,
-    and now you can fill the holes
-  * navigate to the hole { } using C-c C-f (forward) or C-c C-b (backward)
-  * press C-c C-r and agda will try to help you (r for refine)
-  * you should see λ x → { }
-  * navigate to the new hole
-  * C-c C-, to check what agda wants in the hole (C-c C-comma)
-  * the Goal area should look like
-
-  Goal: ⊤
-  ————————————————————————————————————————————————————————————
-  x : ⊤
-
-  * this means you have a proof of ⊤ 'x : ⊤' and you need to give a proof of ⊤
-  * you can now give it a proof of ⊤ and press C-c C-SPC to fill the hole
-
-  There is more than one proof (see solutions) - are they the same?
--}
-
-{-
-Let's assume we have the following the naturals ℕ
-and try to define the 'predicate on ℕ' given by 'x is 0'
--}
-isZero : ℕ → Prop
-isZero zero = ?
-isZero (suc n) = ?
-
-{-
-Here's how:
-  * when x is zero, we give the proposition ⊤
-  (try typing it in by writing \top then pressing C-c C-SPC)
-  * when x is suc n (i.e. 'n + 1', suc for successor) we give ⊥ (\bot)
-This is technically using induction - see AsTypes.
-
-In general a 'predicate on ℕ' is just a 'function' P : ℕ → Prop
--}
-
-{-
-You can check if zero is indeed zero by clicking C-c C-n,
-which brings up a thing on the bottom saying 'Expression',
-and you can type the following
-isZero zero
-isZero (suc zero)
-isZero (suc (suc zero))
-...
--}
-
-{-
-We can prove that 'there exists a natural number that isZero'
-in set theory we might write
-  ∃ x ∈ ℕ, x = 0
-which in agda noation is
-  Σ ℕ isZero
-
-In general if we have predicate P : ℕ → Prop we would write
-  Σ ℕ P
-for
-  ∃ x ∈ ℕ, P x
-
-To formulate the result Σ ℕ isZero we need to define
-a proof of it
--}
-ExistsZero : Σ ℕ isZero
-ExistsZero = ?
-
-{-
-To fill the hole, we need to give a natural and a proof that it is zero.
-Agda will give the syntax you need:
-  * navigate to the correct hole then refine using C-c C-r
-  * there are now two holes - but which is which?
-  * navigate to the first holes and type C-c C-,
-    - for the first hole it will ask you to give it a natural 'Goal: ℕ'
-    - for the second hole it will ask you for a proof that
-    whatever you put in the first hole is zero 'Goal: isZero ?0' for example
-  * try to fill both holes, using C-c C-SPC as before
-  * for the second hole you can try also C-c C-r,
-    Agda knows there is an obvious proof!
--}
-
-{-
-Let's show 'if all natural numbers are zero then we have a contradiction',
-where 'a contradiction' is a proof of ⊥.
-In maths we would write
-  (∀ x ∈ ℕ, x = 0) → ⊥
-and the agda notation for this is
-  ((x : ℕ) → isZero x) → ⊥
-
-In general if we have a predicate P : ℕ → Prop then we write
-  (x : ℕ) → P x
-to mean
-  ∀ x ∈ ℕ, P x
--}
-
-AllZero→⊥ : ((x : ℕ) → isZero x) → ⊥
-AllZero→⊥ = ?
-
-{-
-Here is how we prove it in maths
-  * assume hypothesis h, a proof of (x : ℕ) → isZero x
-  * apply the hypothesis h to 1, deducing isZero 1, i.e. we get a proof of isZero 1
-  * notice isZero 1 IS ⊥
-
-Here is how you can prove it here
-  * navigate to the hole and check the goal
-  * to assume the hypothesis (x : ℕ) → isZero x,
-    type an h in front like so
-    AllZero→⊥ h = { }
-  * now do
-    * C-c C-l to load the file
-    * navigate to the new hole and check the new goal
-  * type h in the hole, type C-c C-r
-  * this should give h { }
-  * navigate to the new hole and check the Goal
-  * Explanation
-    * (h x) is a proof of isZero x for each x
-    * it's now asking for a natural x such that isZero x is ⊥
-  * Try filling the hole with 0 and 1 and see what Agda says
--}
-
-{-
-Let's try to show the mathematical statement
-'any natural n is 0 or not'
-but we need a definition of 'or'
--}
-data OR (P Q : Prop) : Prop where
-  left : P → OR P Q
-  right : Q → OR P Q
-{-
-This reads
-  * Given propositions P and Q we have another proposition P or Q
-  * There are two ways of proving P or Q
-    * given a proof of P, left sends this to a proof of P or Q
-    * given a proof of Q, right sends this to a proof of P or Q
-
-Agda supports nice notation using underscores.
--}
-
-data _∨_ (P Q : Prop) : Prop where
-  left : P → P ∨ Q
-  right : Q → P ∨ Q
-
-{-
-[Important note]
-Agda is sensitive to spaces so these are bad
-
-data _ ∨ _ (P Q : Prop) : Prop where
-  left : P → P ∨ Q
-  right : Q → P ∨ Q
-
-data _∨_ (P Q : Prop) : Prop where
-  left : P → P∨Q
-  right : Q → P∨Q
-
-it is also sensitive to indentation so these are also bad
-
-data _∨_ (P Q : Prop) : Prop where
-left : P → P ∨ Q
-right : Q → P ∨ Q
-
--}
-
-{-
-Now we can prove it!
-This technically uses induction - see AsTypes.
-Fill the missing part of the theorem statement.
-You need to first uncomment this by getting rid of the -- in front (C-x C-;)
--}
--- DecidableIsZero : (n : ℕ) → {!!}
--- DecidableIsZero zero = {!!}
--- DecidableIsZero (suc n) = {!!}

0Trinitarianism/bin/AsProps/Quest0Preamble.agda

@@ -1,12 +0,0 @@
-
-module Trinitarianism.AsProps.Quest0Preamble where
-
-open import Cubical.Core.Everything hiding (_∨_) public
-open import Cubical.Data.Nat public
-
-private
-  postulate
-    u : Level
-
-Prop = Type u
-

0Trinitarianism/bin/AsProps/Quest0Solutions.agda

@@ -1,43 +0,0 @@
-module Trinitarianism.Quest0Solutions where
-open import Trinitarianism.Quest0Preamble
-
-private
-  postulate
-    u : Level
-
-data ⊤ : Type u where
-  trivial : ⊤
-
-data ⊥ : Type u where
-
-TrueToTrue : ⊤ → ⊤
-TrueToTrue = λ x → x
-
-TrueToTrue' : ⊤ → ⊤
-TrueToTrue' x = x
-
-TrueToTrue'' : ⊤ → ⊤
-TrueToTrue'' trivial = trivial
-
-TrueToTrue''' : ⊤ → ⊤
-TrueToTrue''' x = trivial
-
-isZero : ℕ → Type u
-isZero zero = ⊤
-isZero (suc n) = ⊥
-
-ExistsZero : Σ ℕ isZero
-ExistsZero = zero , trivial
-
-AllZero→⊥ : ((x : ℕ) → isZero x) → ⊥
-AllZero→⊥ h = h 1
-
-data _∨_ (P Q : Type u) : Type u where
-  left : P → P ∨ Q
-  right : Q → P ∨ Q
-
-DecidableIsZero : (n : ℕ) → (isZero n) ∨ (isZero n → ⊥)
-DecidableIsZero zero = left trivial
-DecidableIsZero (suc n) = right (λ x → x)
-
-

0Trinitarianism/bin/AsProps/Quest0Solutions.lagda.md

@@ -1,39 +0,0 @@
-```agda
-module Trinitarianism.AsProps.Quest0Solutions where
-open import Trinitarianism.AsProps.Quest0Preamble
-
-data ⊤ : Prop where
-  trivial : ⊤
-
-data ⊥ : Prop where
-
-TrueToTrue : ⊤ → ⊤
-TrueToTrue = λ x → x
-
-TrueToTrue' : ⊤ → ⊤
-TrueToTrue' x = x
-
-TrueToTrue'' : ⊤ → ⊤
-TrueToTrue'' trivial = trivial
-
-TrueToTrue''' : ⊤ → ⊤
-TrueToTrue''' x = trivial
-
-isZero : ℕ → Prop
-isZero zero = ⊤
-isZero (suc n) = ⊥
-
-ExistsZero : Σ ℕ isZero
-ExistsZero = zero , trivial
-
-AllZero→⊥ : ((x : ℕ) → isZero x) → ⊥
-AllZero→⊥ h = h 1
-
-data _∨_ (P Q : Prop) : Prop where
-  left : P → P ∨ Q
-  right : Q → P ∨ Q
-
-DecidableIsZero : (n : ℕ) → (isZero n) ∨ (isZero n → ⊥)
-DecidableIsZero zero = left trivial
-DecidableIsZero (suc n) = right (λ x → x)
-```

0Trinitarianism/bin/AsProps/Quest1.agda

@@ -1,13 +0,0 @@
-{-
-Two things being equal is also a proposition
-
--}
-
-
-
-
--- FalseToTrue : ⊥ → ⊤
--- FalseToTrue = λ x → trivial
-
--- FalseToTrue' : ⊥ → ⊤
--- FalseToTrue' ()

0Trinitarianism/bin/AsTypes/Quest0.agda

@@ -1,227 +0,0 @@
-module Trinitarianism.AsTypes.Quest0 where
-
-open import Cubical.Core.Everything hiding (_∨_)
--- ------------------------------
-
-{-
-  In this branch,
-  we develop the point of view of types as constructions / programs.
-
-  Here is our first construction.
--}
-data Unit : Type where
-  trivial : Unit
-{-
-  This reads 'Unit is a type of construction and
-  there is a recipe for it, called "trivial"'.
-
-  Here is another construction.
--}
-
-data Empty : Type where
-
-{-
-  This says that Empty is a construction and
-  there are no recipes for it.
--}
-
-{-
-  Given two constructions A and B,
-  'converting recipes of A into recipes of B' is itself a type of construction,
-  written A → B.
-  To give a recipe of A → B,
-  we assume a recipe x of A and give a recipe y of B.
-
-  Here is an example demonstrating → in action
--}
-
-UnitToUnit : Unit → Unit
-UnitToUnit = {!!}
-
-{-
-  * press C-c C-l (this means Ctrl-c Ctrl-l) to load the document,
-    and now you can fill the holes
-  * navigate to the hole { } using C-c C-f (forward) or C-c C-b (backward)
-  * press C-c C-r and agda will try to help you (r for refine)
-  * you should see λ x → { }
-  * navigate to the new hole
-  * C-c C-, to check what agda wants in the hole (C-c C-comma)
-  * the Goal area should look like
-
-  Goal: Unit
-  ————————————————————————————————————————————————————————————
-  x : Unit
-
-  * this means you have a proof of Unit 'x : Unit' and you need to give a proof of Unit
-  * you can now give it a proof of Unit and press C-c C-SPC to fill the hole
-
-  There is more than one proof (see solutions) - are they the same?
--}
-
-{-
-  We can also encode "natural numbers" as a type of construction.
--}
-data ℕ : Type where
-  zero : ℕ
-  suc : ℕ → ℕ
-{-
-  This reads '
-    - ℕ is a type of construction
-    - "zero" is a recipe for ℕ
-    - "suc" takes an existing recipe for ℕ and gives
-      another recipe for ℕ.
-  '
--}
-{-
-  Let's write a program that
-  "given a recipe n of ℕ, tells us whether it is zero".
-
-  TODO finish this.
--}
-isZero : ℕ → Type
-isZero zero = {!!}
-isZero (suc n) = {!!}
-
-{-
-Here's how:
-  * when x is zero, we give the proposition Unit
-  (try typing it in by writing \top then pressing C-c C-SPC)
-  * when x is suc n (i.e. 'n + 1', suc for successor) we give Empty (\bot)
-This is technically using induction - see AsTypes.
-
-In general a 'predicate on ℕ' is just a 'function' P : ℕ → Type
--}
-
-{-
-You can check if zero is indeed zero by clicking C-c C-n,
-which brings up a thing on the bottom saying 'Expression',
-and you can type the following
-isZero zero
-isZero (suc zero)
-isZero (suc (suc zero))
-...
--}
-
-{-
-We can prove that 'there exists a natural number that isZero'
-in set theory we might write
-  ∃ x ∈ ℕ, x = 0
-which in agda noation is
-  Σ ℕ isZero
-
-In general if we have predicate P : ℕ → Type we would write
-  Σ ℕ P
-for
-  ∃ x ∈ ℕ, P x
-
-To formulate the result Σ ℕ isZero we need to define
-a proof of it
--}
-ExistsZero : Σ ℕ isZero
-ExistsZero = {!!}
-
-{-
-To fill the hole, we need to give a natural and a proof that it is zero.
-Agda will give the syntax you need:
-  * navigate to the correct hole then refine using C-c C-r
-  * there are now two holes - but which is which?
-  * navigate to the first holes and type C-c C-,
-    - for the first hole it will ask you to give it a natural 'Goal: ℕ'
-    - for the second hole it will ask you for a proof that
-    whatever you put in the first hole is zero 'Goal: isZero ?0' for example
-  * try to fill both holes, using C-c C-SPC as before
-  * for the second hole you can try also C-c C-r,
-    Agda knows there is an obvious proof!
--}
-
-{-
-Let's show 'if all natural numbers are zero then we have a contradiction',
-where 'a contradiction' is a proof of Empty.
-In maths we would write
-  (∀ x ∈ ℕ, x = 0) → Empty
-and the agda notation for this is
-  ((x : ℕ) → isZero x) → Empty
-
-In general if we have a predicate P : ℕ → Type then we write
-  (x : ℕ) → P x
-to mean
-  ∀ x ∈ ℕ, P x
--}
-
-AllZero→Empty : ((x : ℕ) → isZero x) → Empty
-AllZero→Empty = {!!}
-
-{-
-Here is how we prove it in maths
-  * assume hypothesis h, a proof of (x : ℕ) → isZero x
-  * apply the hypothesis h to 1, deducing isZero 1, i.e. we get a proof of isZero 1
-  * notice isZero 1 IS Empty
-
-Here is how you can prove it here
-  * navigate to the hole and check the goal
-  * to assume the hypothesis (x : ℕ) → isZero x,
-    type an h in front like so
-    AllZero→Empty h = { }
-  * now do
-    * C-c C-l to load the file
-    * navigate to the new hole and check the new goal
-  * type h in the hole, type C-c C-r
-  * this should give h { }
-  * navigate to the new hole and check the Goal
-  * Explanation
-    * (h x) is a proof of isZero x for each x
-    * it's now asking for a natural x such that isZero x is Empty
-  * Try filling the hole with 0 and 1 and see what Agda says
--}
-
-{-
-Let's try to show the mathematical statement
-'any natural n is 0 or not'
-but we need a definition of 'or'
--}
-data OR (P Q : Type) : Type where
-  left : P → OR P Q
-  right : Q → OR P Q
-{-
-This reads
-  * Given propositions P and Q we have another proposition P or Q
-  * There are two ways of proving P or Q
-    * given a proof of P, left sends this to a proof of P or Q
-    * given a proof of Q, right sends this to a proof of P or Q
-
-Agda supports nice notation using underscores.
--}
-
-data _∨_ (P Q : Type) : Type where
-  left : P → P ∨ Q
-  right : Q → P ∨ Q
-
-{-
-[Important note]
-Agda is sensitive to spaces so these are bad
-
-data _ ∨ _ (P Q : Type) : Type where
-  left : P → P ∨ Q
-  right : Q → P ∨ Q
-
-data _∨_ (P Q : Type) : Type where
-  left : P → P∨Q
-  right : Q → P∨Q
-
-it is also sensitive to indentation so these are also bad
-
-data _∨_ (P Q : Type) : Type where
-left : P → P ∨ Q
-right : Q → P ∨ Q
-
--}
-
-{-
-Now we can prove it!
-This technically uses induction - see AsTypes.
-Fill the missing part of the theorem statement.
-You need to first uncomment this by getting rid of the -- in front (C-x C-;)
--}
--- DecidableIsZero : (n : ℕ) → {!!}
--- DecidableIsZero zero = {!!}
--- DecidableIsZero (suc n) = {!!}

1FundamentalGroup/Preambles/P0.agda

@@ -2,7 +2,7 @@ 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 public
+open import Cubical.Data.Bool hiding (elim) public
 open import Cubical.Foundations.Prelude
      renaming ( subst to endPt
               ; transport to pathToFun

1FundamentalGroup/Quest0.agda

@@ -3,62 +3,77 @@ module 1FundamentalGroup.Quest0 where
 open import 1FundamentalGroup.Preambles.P0
 
 Refl : base ≡ base
-Refl = {!!}
+Refl = λ i → base
 
 Flip : Bool → Bool
-Flip x = {!!}
+Flip false = true
+Flip true = false
 
 flipIso : Bool ≅ Bool
-flipIso = {!!}
+flipIso = iso Flip Flip rightInv leftInv where
+  rightInv : section Flip Flip
+  rightInv false = refl
+  rightInv true = refl
+
+  leftInv : retract Flip Flip
+  leftInv false = refl
+  leftInv true = refl
 
 flipPath : Bool ≡ Bool
-flipPath = {!!}
+flipPath = isoToPath flipIso
 
 doubleCover : S¹ → Type
-doubleCover x = {!!}
+doubleCover base = Bool
+doubleCover (loop i) = flipPath i
 
 endPtOfTrue : base ≡ base → doubleCover base
-endPtOfTrue p = {!!}
+endPtOfTrue p = endPt doubleCover p true
 
 Refl≢loop : Refl ≡ loop → ⊥
-Refl≢loop p = {!!}
+Refl≢loop p = true≢false (cong endPtOfTrue p)
 
 ------------------- Side Quest - Empty -------------------------
 
-{-
 -- This is a comment box,
 -- remove the {- and -} to do the side quests
 
 toEmpty : (A : Type) → Type
-toEmpty A = {!!}
+toEmpty A = A → ⊥
 
 pathEmpty : (A : Type) → Type₁
-pathEmpty A = {!!}
+pathEmpty A = A ≡ ⊥
 
 isoEmpty : (A : Type) → Type
-isoEmpty A = {!!}
+isoEmpty A = A ≅ ⊥
 
 outOf⊥ : (A : Type) → ⊥ → A
 outOf⊥ A ()
 
 toEmpty→isoEmpty : (A : Type) → toEmpty A → isoEmpty A
-toEmpty→isoEmpty A = {!!}
+toEmpty→isoEmpty A f = iso f (outOf⊥ A) leftInv rightInv where
+
+  leftInv : section f (outOf⊥ A)
+  leftInv ()
+
+  rightInv : retract f (outOf⊥ A)
+  rightInv x = outOf⊥ (outOf⊥ A (f x) ≡ x) (f x)
 
 isoEmpty→pathEmpty : (A : Type) → isoEmpty A → pathEmpty A
-isoEmpty→pathEmpty A = {!!}
+isoEmpty→pathEmpty A = isoToPath
 
 pathEmpty→toEmpty : (A : Type) → pathEmpty A → toEmpty A
-pathEmpty→toEmpty A = {!!}
--}
+pathEmpty→toEmpty A p x = pathToFun p x
 
 ------------------- Side Quests - true≢false --------------------
 
-{-
 -- This is a comment box,
 -- remove the {- and -} to do the side quests
 
 true≢false' : true ≡ false → ⊥
-true≢false' = {!!}
+true≢false' true≡false = pathToFun (cong subsingleton true≡false) tt where
+
+  subsingleton : Bool → Type
+  subsingleton false = ⊥
+  subsingleton true = ⊤
 
--}
 

1FundamentalGroup/Quest1.agda

@@ -7,29 +7,44 @@ loopSpace : (A : Type) (a : A) → Type
 loopSpace A a = a ≡ a
 
 loop_times : ℤ → loopSpace S¹ base
-loop n times = {!!}
+loop pos zero times = refl
+loop pos (suc n) times = loop ∙ loop (pos n) times
+loop negsuc zero times = sym loop
+loop negsuc (suc n) times = sym loop ∙ loop (negsuc n) times
 
-{-
-The definition of sucℤ goes here.
--}
 
-{-
-The definition of predℤ goes here.
--}
+sucℤ : ℤ → ℤ
+sucℤ (pos n) = pos (suc n)
+sucℤ (negsuc zero) = pos zero
+sucℤ (negsuc (suc n)) = negsuc n
 
-{-
-The definition of sucℤIso goes here.
--}
+predℤ : ℤ → ℤ
+predℤ (pos zero) = negsuc zero
+predℤ (pos (suc n)) = pos n
+predℤ (negsuc n) = negsuc (suc n)
 
-{-
-The definition of sucℤPath goes here.
--}
+sucℤIso : ℤ ≅ ℤ
+sucℤIso = iso sucℤ predℤ leftInv rightInv where
+
+  leftInv : section sucℤ predℤ
+  leftInv (pos zero) = refl
+  leftInv (pos (suc n)) = refl
+  leftInv (negsuc n) = refl
+
+  rightInv : retract sucℤ predℤ
+  rightInv (pos n) = refl
+  rightInv (negsuc zero) = refl
+  rightInv (negsuc (suc n)) = refl
+
+sucℤPath : ℤ ≡ ℤ
+sucℤPath = isoToPath sucℤIso
 
 helix : S¹ → Type
-helix = {!!}
+helix base = ℤ
+helix (loop i) = sucℤPath i
 
 windingNumberBase : base ≡ base → ℤ
-windingNumberBase = {!!}
+windingNumberBase p = endPt helix p (pos zero)
 
 windingNumber : (x : S¹) → base ≡ x → helix x
-windingNumber = {!!}
+windingNumber x p = endPt helix p (pos zero)

1FundamentalGroup/Shelf/questExtras.agda

@@ -1,126 +0,0 @@
-module 1FundamentalGroup.Shelf.questExtras where
-
-open import Cubical.Foundations.Prelude
-open import Cubical.HITs.S1
-open import Cubical.Data.Empty
-open import 1FundamentalGroup.Quest0Solutions
-
--- ¬isSetS¹ : isSet S¹ → ⊥
--- ¬isSetS¹ = {!!}
-
--- ¬isPropS¹ : isProp S¹ → ⊥
--- ¬isPropS¹ = {!!}
-
--------------solutions------
-¬isSetS¹ : isSet S¹ → ⊥
-¬isSetS¹ h = Refl≢loop (h base base Refl loop)
-
-¬isPropS¹ : isProp S¹ → ⊥
-¬isPropS¹ h = ¬isSetS¹ (isProp→isSet h)
-
-
-------------J exercises----------------
-
-private
-  variable
-    A B : Type
-
-Cong : {x y : A} (f : A → B) → x ≡ y → f x ≡ f y
-Cong {A} {B} {x} f = J (λ y p → f x ≡ f y) refl
-
-Sym : {x y : A} → x ≡ y → y ≡ x
-Sym {A} {x} = J (λ y1 p → y1 ≡ x) refl
-
-SymRefl : {x : A} → Sym {A} {x} {x} (refl) ≡ refl
-SymRefl {A} {x} = JRefl (λ y1 p → y1 ≡ x) refl
-
-Trans : {x y z : A} → x ≡ y → y ≡ z → x ≡ z
-Trans {x = x} {z = z} = J (λ y1 p → y1 ≡ z → x ≡ z) λ q → q
-
-_⋆_ = Trans -- input \*
-
-TransRefl : {x y : A} → Trans {A} {x} {x} {y} refl ≡ λ q → q
-TransRefl {x = x} {y = y} = JRefl ((λ y1 p → y1 ≡ y → x ≡ y)) λ q → q
-
-refl⋆refl : {x : A} → refl {_} {A} {x} ⋆ refl ≡ refl
-refl⋆refl = Cong (λ f → f refl) TransRefl
-
-⋆refl : {x y : A} (p : x ≡ y) → Trans p refl ≡ p
-⋆refl {A} {x} {y} = J (λ y p → Trans p refl ≡ p) refl⋆refl
-
-refl⋆ : {A : Type} {x y : A} (p : x ≡ y) → refl ⋆ p ≡ p
-refl⋆ = J (λ y p → refl ⋆ p ≡ p) refl⋆refl
-
-
-⋆Sym : {A : Type} {x y : A} (p : x ≡ y) → p ⋆ Sym p ≡ refl
-⋆Sym = J (λ y p → p ⋆ Sym p ≡ refl)
-       (
-         refl ⋆ Sym refl
-       ≡⟨ cong (λ p → refl ⋆ p) SymRefl ⟩
-         refl ⋆ refl
-       ≡⟨ refl⋆refl ⟩
-         refl ∎
-       )
-
-
-Sym⋆ : {A : Type} {x y : A} (p : x ≡ y) → (Sym p) ⋆ p ≡ refl
-Sym⋆ = J (λ y p → (Sym p) ⋆ p ≡ refl)
-       (
-         (Sym refl) ⋆ refl
-       ≡⟨ cong (λ p → p ⋆ refl) SymRefl ⟩
-         refl ⋆ refl
-       ≡⟨ refl⋆refl ⟩
-         refl ∎
-       )
-
-Assoc : {A : Type} {w x : A} (p : w ≡ x) {y z : A} (q : x ≡ y) (r : y ≡ z)
-        → (p ⋆ q) ⋆ r ≡ p ⋆ (q ⋆ r)
-Assoc {A} = J
-        -- casing on p
-        (λ x p → {y z : A} (q : x ≡ y) (r : y ≡ z) → (p ⋆ q) ⋆ r ≡ p ⋆ (q ⋆ r))
-        -- reduce to showing when p = refl
-        λ q r →  ((refl ⋆ q) ⋆ r)
-                 ≡⟨ cong (λ p' → p' ⋆ r) (refl⋆ q) ⟩
-                  (q ⋆ r)
-                 ≡⟨ Sym (refl⋆ (q ⋆ r)) ⟩
-                  (refl ⋆ (q ⋆ r)) ∎
-
-
--------------original-------------------
-
-
--- ∙refl : {A : Type} {x y : A} (p : x ≡ y) → p ∙ refl ≡ p
--- ∙refl = J (λ y p → p ∙ refl ≡ p) refl∙refl
-
--- refl∙ : {A : Type} {x y : A} (p : x ≡ y) → refl ∙ p ≡ p
--- refl∙ = J (λ y p → refl ∙ p ≡ p) refl∙refl
-
--- ∙sym : {A : Type} {x y : A} (p : x ≡ y) → p ∙ sym p ≡ refl
--- ∙sym = J (λ y p → p ∙ sym p ≡ refl)
---        (
---          refl ∙ sym refl
---        ≡⟨ cong (λ p → refl ∙ p) symRefl ⟩
---          refl ∙ refl
---        ≡⟨ refl∙refl ⟩
---          refl ∎)
-
--- sym∙ : {A : Type} {x y : A} (p : x ≡ y) → (sym p) ∙ p ≡ refl
--- sym∙ = J (λ y p → (sym p) ∙ p ≡ refl)
---        (
---          (sym refl) ∙ refl
---        ≡⟨ cong (λ p → p ∙ refl) symRefl ⟩
---          refl ∙ refl
---        ≡⟨ refl∙refl ⟩
---          refl ∎)
-
--- assoc : {A : Type} {w x : A} (p : w ≡ x) {y z : A} (q : x ≡ y) (r : y ≡ z)
---         → (p ∙ q) ∙ r ≡ p ∙ (q ∙ r)
--- assoc {A} = J
---         -- casing on p
---         (λ x p → {y z : A} (q : x ≡ y) (r : y ≡ z) → (p ∙ q) ∙ r ≡ p ∙ (q ∙ r))
---         -- reduce to showing when p = refl
---         λ q r →  (refl ∙ q) ∙ r
---                  ≡⟨ cong (λ p' → p' ∙ r) (refl∙ q) ⟩
---                   q ∙ r
---                  ≡⟨ sym (refl∙ (q ∙ r)) ⟩
---                   refl ∙ q ∙ r ∎