36 lines
834 B
Agda
36 lines
834 B
Agda
-- ignore
|
|
module 1FundamentalGroup.Quest0Solutions where
|
|
open import 1FundamentalGroup.Preambles.P0
|
|
|
|
Refl : base ≡ base
|
|
Refl = λ i → base
|
|
|
|
Flip : Bool → Bool
|
|
Flip false = true
|
|
Flip true = false
|
|
|
|
-- notice we used `refl` instead of `λ i → false`,
|
|
-- more on `refl` in Quest1
|
|
flipIso : Bool ≅ Bool
|
|
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 = isoToPath flipIso
|
|
|
|
doubleCover : S¹ → Type
|
|
doubleCover base = Bool
|
|
doubleCover (loop i) = flipPath i
|
|
|
|
endPtOfTrue : (p : base ≡ base) → doubleCover base
|
|
endPtOfTrue p = endPt doubleCover p true
|
|
|
|
Refl≢loop : Refl ≡ loop → ⊥
|
|
Refl≢loop p = true≢false (cong endPtOfTrue p)
|