Complete 1Fundamentalgroup/Quest0.agda

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 = ⊤
 
--}