65 lines
1.2 KiB
Agda
65 lines
1.2 KiB
Agda
-- ignore
|
|
module 1FundamentalGroup.Quest0 where
|
|
open import 1FundamentalGroup.Preambles.P0
|
|
|
|
Refl : base ≡ base
|
|
Refl = {!!}
|
|
|
|
Flip : Bool → Bool
|
|
Flip x = {!!}
|
|
|
|
flipIso : Bool ≅ Bool
|
|
flipIso = {!!}
|
|
|
|
flipPath : Bool ≡ Bool
|
|
flipPath = {!!}
|
|
|
|
doubleCover : S¹ → Type
|
|
doubleCover x = {!!}
|
|
|
|
endPtOfTrue : (p : base ≡ base) → doubleCover base
|
|
endPtOfTrue p = {!!}
|
|
|
|
Refl≢loop : Refl ≡ loop → ⊥
|
|
Refl≢loop p = {!!}
|
|
|
|
------------------- Side Quest - Empty -------------------------
|
|
|
|
{-
|
|
-- This is a comment box,
|
|
-- remove the {- and -} to do the side quests
|
|
|
|
toEmpty : (A : Type) → Type
|
|
toEmpty A = {!!}
|
|
|
|
pathEmpty : (A : Type) → Type₁
|
|
pathEmpty A = {!!}
|
|
|
|
isoEmpty : (A : Type) → Type
|
|
isoEmpty A = {!!}
|
|
|
|
outOf⊥ : (A : Type) → ⊥ → A
|
|
outOf⊥ A ()
|
|
|
|
toEmpty→isoEmpty : (A : Type) → toEmpty A → isoEmpty A
|
|
toEmpty→isoEmpty A = {!!}
|
|
|
|
isoEmpty→pathEmpty : (A : Type) → isoEmpty A → pathEmpty A
|
|
isoEmpty→pathEmpty A = {!!}
|
|
|
|
pathEmpty→toEmpty : (A : Type) → pathEmpty A → toEmpty A
|
|
pathEmpty→toEmpty A = {!!}
|
|
-}
|
|
|
|
------------------- Side Quests - true≢false --------------------
|
|
|
|
{-
|
|
-- This is a comment box,
|
|
-- remove the {- and -} to do the side quests
|
|
|
|
true≢false' : true ≡ false → ⊥
|
|
true≢false' = {!!}
|
|
|
|
-}
|
|
|