diff --git a/1FundamentalGroup/Preambles/P2.agda b/1FundamentalGroup/Preambles/P2.agda index 30fa264..d26c358 100644 --- a/1FundamentalGroup/Preambles/P2.agda +++ b/1FundamentalGroup/Preambles/P2.agda @@ -5,4 +5,4 @@ open import Cubical.Data.Int using (ℤ ; pos ; negsuc ; -_) public open import Cubical.Foundations.Isomorphism public open import Cubical.Foundations.Prelude renaming (subst to endPt) public open import Cubical.HITs.S1 using (S¹ ; base ; loop) public -open import 1FundamentalGroup.Quest1 public +open import 1FundamentalGroup.Quest1Solutions public diff --git a/1FundamentalGroup/Quest0Solutions.agda b/1FundamentalGroup/Quest0Solutions.agda index 2a85daf..26b6170 100644 --- a/1FundamentalGroup/Quest0Solutions.agda +++ b/1FundamentalGroup/Quest0Solutions.agda @@ -1,12 +1,6 @@ +-- ignore module 1FundamentalGroup.Quest0Solutions where - -open import Cubical.Data.Empty -open import Cubical.Data.Unit renaming ( Unit to ⊤ ) -open import Cubical.Data.Bool -open import Cubical.Foundations.Prelude renaming ( subst to endPt ) -open import Cubical.Foundations.Isomorphism renaming ( Iso to _≅_ ) -open import Cubical.Foundations.Path -open import Cubical.HITs.S1 +open import 1FundamentalGroup.Preambles.P0 Refl : base ≡ base Refl = λ i → base diff --git a/1FundamentalGroup/Quest2.agda b/1FundamentalGroup/Quest2.agda index b6adab1..d33d069 100644 --- a/1FundamentalGroup/Quest2.agda +++ b/1FundamentalGroup/Quest2.agda @@ -2,40 +2,27 @@ module 1FundamentalGroup.Quest2 where open import 1FundamentalGroup.Preambles.P2 -sucℤ : ℤ → ℤ -sucℤ (pos n) = pos (suc n) -sucℤ (negsuc zero) = pos zero -sucℤ (negsuc (suc n)) = negsuc n +{- +The definition of sucℤ goes here. +-} -predℤ : ℤ → ℤ -predℤ (pos zero) = negsuc zero -predℤ (pos (suc n)) = pos n -predℤ (negsuc n) = negsuc (suc n) +{- +The definition of predℤ goes here. +-} -sucℤIso : Iso ℤ ℤ -sucℤIso = iso sucℤ predℤ s r where +{- +The definition of sucℤIso goes here. +-} - 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 - -sucℤPath : ℤ ≡ ℤ -sucℤPath = isoToPath sucℤIso +{- +The definition of sucℤPath goes here. +-} helix : S¹ → Type -helix base = ℤ -helix (loop i) = sucℤPath i +helix = {!!} spinCountBase : base ≡ base → ℤ -spinCountBase p = endPt helix p (pos zero) +spinCountBase = ? spinCount : (x : S¹) → base ≡ x → helix x -spinCount x p = endPt helix p (pos zero) +spinCount = ? diff --git a/1FundamentalGroup/Quest2Solutions.agda b/1FundamentalGroup/Quest2Solutions.agda new file mode 100644 index 0000000..7c2dc54 --- /dev/null +++ b/1FundamentalGroup/Quest2Solutions.agda @@ -0,0 +1,41 @@ +-- ignore +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 + +predℤ : ℤ → ℤ +predℤ (pos zero) = negsuc zero +predℤ (pos (suc n)) = pos n +predℤ (negsuc n) = negsuc (suc n) + +sucℤIso : Iso ℤ ℤ +sucℤIso = 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 + + r : retract sucℤ predℤ + r (pos zero) = refl + r (pos (suc n)) = refl + r (negsuc zero) = refl + r (negsuc (suc n)) = refl + +sucℤPath : ℤ ≡ ℤ +sucℤPath = isoToPath sucℤIso + +helix : S¹ → Type +helix base = ℤ +helix (loop i) = sucℤPath i + +spinCountBase : base ≡ base → ℤ +spinCountBase p = endPt helix p (pos zero) + +spinCount : (x : S¹) → base ≡ x → helix x +spinCount x p = endPt helix p (pos zero) diff --git a/_build/2.6.2/agda/1FundamentalGroup/Preambles/P2.agdai b/_build/2.6.2/agda/1FundamentalGroup/Preambles/P2.agdai index 51c632e..da35261 100644 Binary files a/_build/2.6.2/agda/1FundamentalGroup/Preambles/P2.agdai and b/_build/2.6.2/agda/1FundamentalGroup/Preambles/P2.agdai differ diff --git a/_build/2.6.2/agda/1FundamentalGroup/Quest0Solutions.agdai b/_build/2.6.2/agda/1FundamentalGroup/Quest0Solutions.agdai index 88594b3..19ec25a 100644 Binary files a/_build/2.6.2/agda/1FundamentalGroup/Quest0Solutions.agdai and b/_build/2.6.2/agda/1FundamentalGroup/Quest0Solutions.agdai differ diff --git a/_build/2.6.2/agda/1FundamentalGroup/Quest2.agdai b/_build/2.6.2/agda/1FundamentalGroup/Quest2.agdai index 7aefc71..7284c34 100644 Binary files a/_build/2.6.2/agda/1FundamentalGroup/Quest2.agdai and b/_build/2.6.2/agda/1FundamentalGroup/Quest2.agdai differ diff --git a/_build/2.6.2/agda/1FundamentalGroup/Quest2Solutions.agdai b/_build/2.6.2/agda/1FundamentalGroup/Quest2Solutions.agdai new file mode 100644 index 0000000..17bcb36 Binary files /dev/null and b/_build/2.6.2/agda/1FundamentalGroup/Quest2Solutions.agdai differ