changed transport to pathToFun

This commit is contained in:
Jlh18 2021-10-02 16:41:34 +01:00
parent 9268cc2b51
commit ccb193a881
11 changed files with 43 additions and 34 deletions

View File

@ -3,7 +3,10 @@ module 1FundamentalGroup.Preambles.P0 where
open import Cubical.Data.Empty using () public
open import Cubical.Data.Unit renaming ( Unit to ) public
open import Cubical.Data.Bool public
open import Cubical.Foundations.Prelude renaming ( subst to endPt ) public
open import Cubical.Foundations.Prelude
renaming ( subst to endPt
; transport to pathToFun
) public
open import Cubical.Foundations.Isomorphism renaming ( Iso to _≅_ ) public
open import Cubical.Foundations.Path public
open import Cubical.HITs.S1 public

View File

@ -4,6 +4,9 @@ open import Cubical.HITs.S1 using (S¹ ; base ; loop) public
open import Cubical.Data.Nat using ( ; suc ; zero) public
open import Cubical.Data.Int using ( ; pos ; negsuc ; -_) public
open import Cubical.Data.Empty public
open import Cubical.Foundations.Prelude renaming (subst to endPt) public
open import Cubical.Foundations.Prelude
renaming ( subst to endPt
; transport to pathToFun
) public
open import Cubical.Foundations.Isomorphism renaming (Iso to _≅_) public
open import 1FundamentalGroup.Quest0Solutions using ( Refl ; Refl≢loop ) public

View File

@ -3,6 +3,9 @@ module 1FundamentalGroup.Preambles.P2 where
open import Cubical.Data.Nat public
open import Cubical.Data.Int using ( ; pos ; negsuc ; -_) public
open import Cubical.Foundations.Isomorphism renaming (Iso to _≅_) public
open import Cubical.Foundations.Prelude renaming (subst to endPt) public
open import Cubical.Foundations.Prelude
renaming ( subst to endPt
; transport to pathToFun
) public
open import Cubical.HITs.S1 using ( ; base ; loop) public
open import 1FundamentalGroup.Quest1Solutions public

View File

@ -61,12 +61,12 @@ isoEmpty→pathEmpty : (A : Type) → isoEmpty A → pathEmpty A
isoEmpty→pathEmpty A = isoToPath
pathEmpty→toEmpty : (A : Type) pathEmpty A toEmpty A
pathEmpty→toEmpty A p x = transport p x
pathEmpty→toEmpty A p x = pathToFun p x
------------------- Side Quests - true≢false --------------------
true≢false' : true false
true≢false' h = transport ⊤≡⊥ tt where
true≢false' h = pathToFun ⊤≡⊥ tt where
propify : Bool Type
propify false =

View File

@ -2,40 +2,40 @@
module 1FundamentalGroup.Quest2Solutions where
open import 1FundamentalGroup.Preambles.P2
suc :
suc (pos n) = pos (suc n)
suc (negsuc zero) = pos zero
suc (negsuc (suc n)) = negsuc n
-- suc :
-- suc (pos n) = pos (suc n)
-- suc (negsuc zero) = pos zero
-- suc (negsuc (suc n)) = negsuc n
pred :
pred (pos zero) = negsuc zero
pred (pos (suc n)) = pos n
pred (negsuc n) = negsuc (suc n)
-- pred :
-- pred (pos zero) = negsuc zero
-- pred (pos (suc n)) = pos n
-- pred (negsuc n) = negsuc (suc n)
sucIso :
sucIso = iso suc pred s r where
-- sucIso :
-- sucIso = iso suc pred s r where
s : section suc pred
s (pos zero) = refl
s (pos (suc n)) = refl
s (negsuc zero) = refl
s (negsuc (suc n)) = refl
-- s : section suc pred
-- s (pos zero) = refl
-- s (pos (suc n)) = refl
-- s (negsuc zero) = refl
-- s (negsuc (suc n)) = refl
r : retract suc pred
r (pos zero) = refl
r (pos (suc n)) = refl
r (negsuc zero) = refl
r (negsuc (suc n)) = refl
-- r : retract suc pred
-- r (pos zero) = refl
-- r (pos (suc n)) = refl
-- r (negsuc zero) = refl
-- r (negsuc (suc n)) = refl
sucPath :
sucPath = isoToPath sucIso
-- sucPath :
-- sucPath = isoToPath sucIso
helix : Type
helix base =
helix (loop i) = sucPath i
-- helix : S¹ → Type
-- helix base =
-- helix (loop i) = sucPath i
windingNumberBase : base base
windingNumberBase p = endPt helix p (pos zero)
-- windingNumberBase : base ≡ base →
-- windingNumberBase p = endPt helix p (pos zero)
windingNumber : (x : ) base x helix x
windingNumber x p = endPt helix p (pos zero)
-- windingNumber : (x : S¹) → base ≡ x → helix x
-- windingNumber x p = endPt helix p (pos zero)