diff --git a/1FundamentalGroup/Quest2.agda b/1FundamentalGroup/Quest2.agda index d33d069..fda160a 100644 --- a/1FundamentalGroup/Quest2.agda +++ b/1FundamentalGroup/Quest2.agda @@ -21,8 +21,8 @@ The definition of sucℤPath goes here. helix : S¹ → Type helix = {!!} -spinCountBase : base ≡ base → ℤ -spinCountBase = ? +windingNumberBase : base ≡ base → ℤ +windingNumberBase = {!!} -spinCount : (x : S¹) → base ≡ x → helix x -spinCount = ? +windingNumber : (x : S¹) → base ≡ x → helix x +windingNumber = {!!} diff --git a/1FundamentalGroup/Quest2Solutions.agda b/1FundamentalGroup/Quest2Solutions.agda index 7c2dc54..0ae8831 100644 --- a/1FundamentalGroup/Quest2Solutions.agda +++ b/1FundamentalGroup/Quest2Solutions.agda @@ -34,8 +34,8 @@ helix : S¹ → Type helix base = ℤ helix (loop i) = sucℤPath i -spinCountBase : base ≡ base → ℤ -spinCountBase p = endPt helix p (pos zero) +windingNumberBase : base ≡ base → ℤ +windingNumberBase p = endPt helix p (pos zero) -spinCount : (x : S¹) → base ≡ x → helix x -spinCount x p = endPt helix p (pos zero) +windingNumber : (x : S¹) → base ≡ x → helix x +windingNumber x p = endPt helix p (pos zero) diff --git a/_build/2.6.2/agda/1FundamentalGroup/Preambles/P1.agdai b/_build/2.6.2/agda/1FundamentalGroup/Preambles/P1.agdai index 5af2140..ddc0f69 100644 Binary files a/_build/2.6.2/agda/1FundamentalGroup/Preambles/P1.agdai and b/_build/2.6.2/agda/1FundamentalGroup/Preambles/P1.agdai differ diff --git a/_build/2.6.2/agda/1FundamentalGroup/Preambles/P2.agdai b/_build/2.6.2/agda/1FundamentalGroup/Preambles/P2.agdai index da35261..c54b7bf 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/Quest1Solutions.agdai b/_build/2.6.2/agda/1FundamentalGroup/Quest1Solutions.agdai index 0605090..fe514f3 100644 Binary files a/_build/2.6.2/agda/1FundamentalGroup/Quest1Solutions.agdai and b/_build/2.6.2/agda/1FundamentalGroup/Quest1Solutions.agdai differ diff --git a/_build/2.6.2/agda/1FundamentalGroup/Quest2Solutions.agdai b/_build/2.6.2/agda/1FundamentalGroup/Quest2Solutions.agdai index 17bcb36..cf233b9 100644 Binary files a/_build/2.6.2/agda/1FundamentalGroup/Quest2Solutions.agdai and b/_build/2.6.2/agda/1FundamentalGroup/Quest2Solutions.agdai differ