module Homotopy.Space.Circle where
Spaces: The circleđ
The first example of nontrivial space one typically encounters when studying synthetic homotopy theory is the circle: it is, in a sense, the perfect space to start with, having exactly one nontrivial path space, which is a free group, and the simplest nontrivial free group at that: the integers.
data SÂč : Type where base : SÂč loop : base ⥠base SÂčâ : Typeâ lzero SÂčâ = SÂč , base
Diagrammatically, we can picture the circle as being the generated by the following diagram:
In type theory with K, the circle is exactly the same type as â€
. However, with univalence
, it can be shown
that the circle has at least two different paths:
möbius : SÂč â Type möbius base = Bool möbius (loop i) = ua notâ i
When pattern matching on the circle, we are asked to provide a
basepoint b
and a path l : b ⥠b
, as can be
seen in the definition above. To make it clearer, we can also define a
recursion principle:
SÂč-rec : â {â} {A : Type â} (b : A) (l : b ⥠b) â SÂč â A SÂč-rec b l base = b SÂč-rec b l (loop i) = l i
SÂč-elim : â {â} {A : SÂč â Type â} (b : A base) (l : PathP (λ i â A (loop i)) b b) â â s â A s SÂč-elim b l base = b SÂč-elim b l (loop i) = l i
We call the map möbius
a double
cover of the circle, since the fibre at each point is a discrete
space with two elements. It has an action by the fundamental group of
the circle, which has the effect of negating the âparityâ of the path.
In fact, we can use möbius
to show that loop
is not refl
:
parity : base ⥠base â Bool parity l = subst möbius l true _ : parity refl ⥠true _ = refl _ : parity loop ⥠false _ = refl reflâ loop : ÂŹ refl ⥠loop reflâ loop path = trueâ false (ap parity path)
The circle is also useful as a source of counterexamples: we can
prove that there is an inhabitant of (x : SÂč) â x ⥠x
which is not constantly refl
.
always-loop : (x : SÂč) â x ⥠x always-loop = SÂč-elim loop (double-connection loop loop)
Fundamental groupđ
We will now calculate that the first loop space of the circle at the
basepoint is a type of integers, i.e. it satisfies the universal property of
the integers. First, we generalise the construction of möbius
to turn an
equivalence on an arbitrary type into a type family over SÂč
. Transport over this
family will give the universal map
associated with an equivalence
and basepoint
equivâfamily : X â X â SÂč â Type _ equivâfamily {X = X} eqv base = X equivâfamily eqv (loop i) = ua eqv i
We will later need the âactionâ associated with an equivalence valued at a path with free endpoint Taking recovers a more vanilla notion of âaction on â.
equivâaction : â {y} (e : X â X) â base ⥠y â X â equivâfamily e y equivâaction e p x = subst (equivâfamily e) p x _ : X â X â base ⥠base â X â X _ = equivâaction {y = base}
The first thing we will do is assume an elimination principle for
which will be used in showing uniqueness of the universal map
associated to an equivalence
We must also equip
with an auto-equivalence, which corresponds in some way to taking
successors: since loop
corresponds to âthe
number 1â, the equivalence we go with is thus âadding 1â:
postcomposition with the loop
.
ΩSÂč-elim : â {â} (P : Path SÂč base base â Type â) â (pr : P refl) â (pl : P â[ â-post-equiv loop ] P) â â x â P x private rotΩSÂč : (base ⥠base) â (base ⥠base) rotΩSÂč = â-post-equiv {x = base} loop ΩSÂč-integers : Integers (Path SÂč base base) ΩSÂč-integers .point = refl ΩSÂč-integers .rotate = rotΩSÂč
It is easy to see that transporting the basepoint along the family
associated to an automorphism of
commutes with our chosen automorphism of
modulo a tactic application, it is refl
.
ΩSÂč-integers .map-out x e l = equivâaction e l x ΩSÂč-integers .map-out-point x e = Regularity.precise! refl ΩSÂč-integers .map-out-rotate x e l = Regularity.precise! refl
The difficult part of the proof is showing that equivâaction
is the unique
map
with these properties. We will show this is the case assuming first that
we have an elimination principle for
ΩSÂč-integers .map-out-unique f {p} {r} frefl floop = ΩSÂč-elim _ (Regularity.precise! frefl) $ over-leftâover rotΩSÂč λ a â (f a ⥠go a) ââš ap-equiv r â©â (r .fst (f a) ⥠r .fst (go a)) ââš â-pre-equiv (floop a) â©â (f (a â loop) ⥠r .fst (go a)) ââš â-post-equiv (Regularity.precise! refl) â©â (f (a â loop) ⥠go (a â loop)) ââ where go : _ â _ go l = equivâaction r l p
Loop inductionđ
We must now show the elimination principle for that was promised above. Note that, while this is a path type, both of the endpoints are fixed (here, to be constructors), so we can not directly use path induction. Instead, we will mimic the construction of induction from initiality, turning our induction methods into a total algebra which can be mapped into universally.
Applying the universal map at then gives us a pair of an index and a proof in If we have a proper initial object, we could then show that the composite which defines is an algebra map so it must be the identity; thus and we have the desired Here, however, weâre trying to show initiality, so weâll need a hand-crafted coherence.
We note that the induction methods for ΩSÂč-elim
fit together into
a basepoint and auto-equivalence of the type
The family associated to this action will be called totl
.
ΩSÂč-elim P pr pl l = subst P (pathÎČ base l) attempt where totl : SÂč â Type _ totl = equivâfamily (overâtotal rotΩSÂč pl)
By rotating the basepoint (given by the method
we get a value in
but its type appears to be way off. Essentially, to show that our attempt
landed in the
right fibre, we would like to reduce to the case where
since there the index is essentially trivially correct.
attempt : P (subst totl l (refl , pr) .fst) attempt = subst totl l (refl , pr) .snd
However, this statement depends critically on
being a loop, preventing us from using path induction: if
is instead a path
then transport takes us to a fibre of totl
which is not a sigma
type, hence not something we can project from. To generalise this, we
must define a fibrewise transformation from totl
to the based path
space of
which, at the basepoint, is the first projection function.
This turns out to be pretty easy: using the helper function uaâ
to simplify the
coherence condition, we are left with filling a square with the boundary
below, which we have by the definition of path composition: it is â-filler
.
path : â y â totl y â base ⥠y path = SÂč-elim fst $ uaâ λ _ â â-filler _ loop
Now we have a statement which is sufficiently general to prove by
path induction: projecting the index using path
from the result of applying
our universal map, even at an arbitrary based path
is the identity function; And, by construction, when
this statement reduces to precisely the identification between indices
we were looking for.
pathÎČ : â y l â path y (subst totl l (refl , pr)) ⥠l pathÎČ y = J (λ y l â path y (subst totl l (refl , pr)) ⥠l) (transport-refl refl)
ΩSÂčâInt : (base ⥠base) â Int ΩSÂčâInt = Integers-unique ΩSÂč-integers Int-integers open Equiv ΩSÂčâInt renaming (from to loopâż) using ()
It immediately follows from this that the circle is a groupoid, since it is connected and its loop space is a set.
opaque SÂč-is-groupoid : is-groupoid SÂč SÂč-is-groupoid = SÂč-elim (SÂč-elim (Equivâis-hlevel 2 ΩSÂčâInt (hlevel 2)) prop!) prop!
instance H-Level-SÂč : â {k} â H-Level SÂč (3 + k) H-Level-SÂč = basic-instance 3 SÂč-is-groupoid opaque loopâżâșÂč : (n : Int) â loopâż (suc†n) ⥠loopâż n â loop loopâżâșÂč n = Int-integers .map-out-rotate refl rotΩSÂč n
By induction, we can show that this equivalence respects group composition (that is, so that we have a proper isomorphism of groups.
loopâż-+ : (a b : Int) â loopâż (a +†b) ⥠loopâż a â loopâż b loopâż-+ a = Integers.induction Int-integers (ap loopâż (+â€-zeror a) â sym (â-idr _)) λ b â loopâż (a +†b) ⥠loopâż a â loopâż b ââš ap (_â loop) , equivâcancellable (â-post-equiv loop .snd) â©â loopâż (a +†b) â loop ⥠(loopâż a â loopâż b) â loop ââš â-post-equiv (sym (â-assoc _ _ _)) â©â loopâż (a +†b) â loop ⥠loopâż a â loopâż b â loop ââš â-post-equiv (ap (loopâż a â_) (sym (loopâżâșÂč b))) â©â loopâż (a +†b) â loop ⥠loopâż a â loopâż (suc†b) ââš â-pre-equiv (loopâżâșÂč (a +†b)) â©â loopâż (suc†(a +†b)) ⥠loopâż a â loopâż (suc†b) ââš â-pre-equiv (ap loopâż (+â€-sucr a b)) â©â loopâż (a +†suc†b) ⥠loopâż a â loopâż (suc†b) ââ ÏâSÂčâĄâ€ : ÏâGroupoid.Ïâ SÂčâ SÂč-is-groupoid ⥠†ÏâSÂčâĄâ€ = sym $ â«-Path (â«hom (Equiv.from ΩSÂčâInt) (record { pres-â = loopâż-+ })) ((ΩSÂčâInt eâ»Âč) .snd)
Furthermore, since the loop space of the circle is a set, we automatically get that all of its higher homotopy groups are trivial.
ΩâżâșÂČSÂč-is-contr : â n â is-contr â Ω⿠(2 + n) SÂčâ â ΩâżâșÂČSÂč-is-contr zero = is-propââis-contr (hlevel 1) refl ΩâżâșÂČSÂč-is-contr (suc n) = Path-is-hlevel 0 (ΩâżâșÂČSÂč-is-contr n) ÏâââSÂčâĄ0 : â n â Ïâââ (suc n) SÂčâ ⥠Zero-group {lzero} ÏâââSÂčâĄ0 n = â«-Path (Zero-group-is-terminal _ .centre) (is-contrââ (is-contrââ„-â„â-is-contr (ΩâżâșÂČSÂč-is-contr n)) (hlevel 0) .snd)