quest 2 ready

1FundamentalGroup/Quest2.agda

@@ -2,37 +2,18 @@
 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
-{-
-ℤ≡ℕ⊔ℕ : ℤ ≡ ℕ ⊔ ℕ
-ℤ≡ℕ⊔ℕ = {!!}
-
-∙refl : {A : Type} {x y : A} (p : x ≡ y) → p ∙ refl ≡ p
-∙refl = {!!}
-
-refl∙ : {A : Type} {x y : A} (p : x ≡ y) → refl ∙ p ≡ p
-refl∙ = {!!}
-
-∙sym : {A : Type} {x y : A} (p : x ≡ y) → p ∙ sym p ≡ refl
-∙sym = {!!}
-
-sym∙ : {A : Type} {x y : A} (p : x ≡ y) → (sym p) ∙ p ≡ refl
-sym∙ = {!!}
-
-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} = {!!}
--}
 
 {-
 
+Your definition of ℤ≡ℕ⊔ℕ goes here.
+
 Your definition of ⊔NoConfusion goes here.
 
 Your definition of Path≡⊔NoConfusion goes here.