edits to quest 2 and shelf

1FundamentalGroup/Quest2.agda

@@ -2,6 +2,10 @@
 module 1FundamentalGroup.Quest2 where
 open import 1FundamentalGroup.Preambles.P2
 
+
+
+
+
 data _⊔_ (A B : Type) : Type where
 
      inl : A → A ⊔ B

1FundamentalGroup/Quest2Solutions.agda

@@ -2,6 +2,15 @@
 module 1FundamentalGroup.Quest2Solutions where
 open import 1FundamentalGroup.Preambles.P2
 
+isSet→LoopSpace≡⊤ : {A : Type} (x : A) → isSet A → (x ≡ x) ≡ ⊤
+isSet→LoopSpace≡⊤ x h = isoToPath (iso (λ p → tt) inv rightInv (λ p → h x x refl p)) where
+
+  inv : ⊤ → x ≡ x
+  inv tt = refl
+
+  rightInv : section (λ p → tt) inv
+  rightInv tt = refl
+
 
 data _⊔_ (A B : Type) : Type where
 
@@ -90,22 +99,12 @@ isSet⊔NoConfusion hA hB (inr x) (inr y) = hB x y
 ⊔NoConfusionSelf (inl x) = refl
 ⊔NoConfusionSelf (inr x) = refl
 
-Path≅⊔NoConfusion' : (x y : A ⊔ B) → (x ≡ y) ≅ ⊔NoConfusion x y
-Path≅⊔NoConfusion' x y = iso (fun _ _) ({!!}) ({!!}) ({!!}) where
+disjoint : (x : A) (y : B) → inl x ≡ inr y → ⊥
+disjoint x y p = endPt bundle p tt where
 
-  -- if you case on x and y you would have to show that inl and inr are injective
-  -- J avoids this, but leads to needing J and JRefl for showing section and retract
-  fun : (x y : A ⊔ B) → (x ≡ y) → ⊔NoConfusion x y
-  fun x y = J (λ y₂ x₂ → ⊔NoConfusion x y₂) (⊔NoConfusionSelf x)
-
-  inv : (x y : A ⊔ B) → ⊔NoConfusion x y → x ≡ y
-  inv (inl x) (inl y) p = cong inl p
-  inv (inr x) (inr y) p = cong inr p
-
-  rightInv : (x y : A ⊔ B) → section (fun x y) (inv x y)
-  rightInv {A} {B} (inl x) (inl x₁) = J ((λ y' p → fun {A} {B} (inl x) (inl y') (inv (inl x) (inl y') p) ≡ p)) {!!}
-  rightInv {A} {B} (inl x) (inr x₁) = {!!}
-  rightInv {A} {B} (inr x) y = {!!}
+  bundle : A ⊔ B → Type
+  bundle (inl x) = ⊤
+  bundle (inr x) = ⊥
 
 Path≅⊔NoConfusion : (x y : A ⊔ B) → (x ≡ y) ≅ ⊔NoConfusion x y
 Path≅⊔NoConfusion x y = iso (fun _ _) (inv _ _) (rightInv _ _) (leftInv _ _) where

1FundamentalGroup/Shelf/questExtras.agda

@@ -1,8 +1,15 @@
-¬isSetS¹ : isSet S¹ → ⊥
-¬isSetS¹ = {!!}
+module 1FundamentalGroup.Shelf.questExtras where
 
-¬isPropS¹ : isProp S¹ → ⊥
-¬isPropS¹ = {!!}
+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¹ → ⊥
@@ -10,3 +17,110 @@
 
 ¬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 ∎