Created
November 13, 2022 18:21
-
-
Save XiaohuWang0921/ca84a677b4b2ef26078ab0b9634f88c1 to your computer and use it in GitHub Desktop.
A proof that the fundamental group of the pointed circle is isomorphic to the integers in cubical type theory, using Arend.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| \import Function | |
| \import Paths | |
| \import Arith.Int | |
| \open Nat (-) | |
| \open IntRing (negative) | |
| -- # Raising a loop to an natural power | |
| -- | Concatenate a certain loop to itself ``n`` times. | |
| \func repeat {A : \Type} {a : A} (p : a = a) (n : Nat) : a = a \elim n | |
| | 0 => idp | |
| | suc n => repeat p n *> p | |
| -- # Algebraic properties of ``repeat``, i. e. ``repeat p`` is a monoid homomorphism from the additive monoid of natural | |
| -- # numbers to the space of loops | |
| -- | ``repeat`` turns sum of natural numbers into concatenation of paths. | |
| \func repeat_+ {A : \Type} {a : A} {p : a = a} (m n : Nat) : repeat p (m Nat.+ n) = repeat p m *> repeat p n \elim n | |
| | 0 => idp | |
| | suc n => | |
| repeat p (m Nat.+ suc n) ==< idp >== | |
| repeat p (suc (m Nat.+ n)) ==< idp >== | |
| repeat p (m Nat.+ n) *> p ==< pmap (`*> p) (repeat_+ m n) >== | |
| (repeat p m *> repeat p n) *> p ==< *>-assoc (repeat p m) (repeat p n) p >== | |
| repeat p m *> repeat p n *> p ==< idp >== | |
| repeat p m *> repeat p (suc n) `qed | |
| -- | ``repeat`` also turns successor of natural number into concatenation to the left (concatenation to the right is already | |
| -- | satisfied by definition of the function). | |
| \func repeat_suc {A : \Type} {a : A} {p : a = a} (n : Nat) : repeat p (suc n) = p *> repeat p n => | |
| repeat p (suc n) ==< idp >== | |
| repeat p (n Nat.+ 1) ==< idp >== | |
| repeat p (1 Nat.+ n) ==< repeat_+ 1 n >== | |
| repeat p 1 *> repeat p n ==< idp >== | |
| (idp *> p) *> repeat p n ==< pmap (`*> repeat p n) (idp_*> p) >== | |
| p *> repeat p n `qed | |
| -- | Repetition of an inverted path is the same as the inversion of the repetition. | |
| \func repeat_inv {A : \Type} {a : A} {p : a = a} (n : Nat) : repeat (inv p) n = inv (repeat p n) \elim n | |
| | 0 => idp | |
| | suc n => | |
| repeat (inv p) (suc n) ==< idp >== | |
| repeat (inv p) n *> inv p ==< pmap (`*> _) (repeat_inv _) >== | |
| inv (repeat p n) *> inv p ==< inv (*>_inv-comm _ _) >== | |
| inv (p *> repeat p n) ==< pmap inv (inv (repeat_suc _)) >== | |
| inv (repeat p (suc n)) `qed | |
| -- # Raising loops to an integer power | |
| -- | Like ``repeat``, but also accepts negative integers, in which case the output is a repeated concatenation of the | |
| -- | original path inverted. | |
| \func irepeat {A : \Type} {a : A} (p : a = a) (k : Int) : a = a \elim k | |
| | pos n => repeat p n | |
| | neg n => repeat (inv p) n | |
| -- # Algebraic properties of irepeat, i.e. ``irepeat p`` is a group homomorphism from the integers to the space of loops | |
| -- | ``irepeat`` turns subtraction of natural numbers into repeated concatenation of a path with its own inversion. | |
| \func repeat_*>_inv {A : \Type} {a : A} {p : a = a} (m n : Nat) : irepeat p (m - n) = repeat p m *> repeat (inv p) n \elim m, n | |
| | 0, n => inv (idp_*> (repeat (inv p) n)) | |
| | m, 0 => idp | |
| | suc m, suc n => | |
| irepeat p (m - n) ==< repeat_*>_inv m n >== | |
| repeat p m *> repeat (inv p) n ==< idp >== | |
| (repeat p m *> idp) *> repeat (inv p) n ==< pmap ((`*> _) o (_ *>)) (inv (*>_inv p)) >== | |
| (repeat p m *> p *> inv p) *> repeat (inv p) n ==< pmap (`*> repeat (inv p) n) (inv (*>-assoc _ _ _)) >== | |
| ((repeat p m *> p) *> inv p) *> repeat (inv p) n ==< *>-assoc _ _ _ >== | |
| (repeat p m *> p) *> inv p *> repeat (inv p) n ==< idp >== | |
| repeat p (suc m) *> inv p *> repeat (inv p) n ==< pmap (repeat p (suc m) *>) (inv (repeat_suc n)) >== | |
| repeat p (suc m) *> repeat (inv p) (suc n) `qed | |
| -- | ``irepeat`` turns successor of an integer into a concatenation with the original path. | |
| \func irepeat_isuc {A : \Type} {a : A} {p : a = a} (k : Int) : irepeat p (isuc k) = irepeat p k *> p \elim k | |
| | pos n => idp | |
| | neg (suc n) => | |
| irepeat p (isuc (neg (suc n))) ==< idp >== | |
| irepeat p (neg n) ==< idp >== | |
| repeat (inv p) n ==< idp >== | |
| repeat (inv p) n *> idp ==< pmap (_ *>) (inv (inv_*> p)) >== | |
| repeat (inv p) n *> inv p *> p ==< inv (*>-assoc _ _ _) >== | |
| (repeat (inv p) n *> inv p) *> p ==< idp >== | |
| repeat (inv p) (suc n) *> p ==< idp >== | |
| irepeat p (neg (suc n)) *> p `qed | |
| -- | ``irepeat`` turns predecessor of an integer into a concatenation with the original path inverted. | |
| \func irepeat_ipred {A : \Type} {a : A} {p : a = a} (k : Int) : irepeat p (ipred k) = irepeat p k *> inv p \elim k | |
| | 0 => idp | |
| | pos (suc n) => | |
| irepeat p (ipred (pos (suc n))) ==< idp >== | |
| irepeat p (pos n) ==< idp >== | |
| repeat p n ==< idp >== | |
| repeat p n *> idp ==< pmap (_ *>) (inv (*>_inv p)) >== | |
| repeat p n *> p *> inv p ==< inv (*>-assoc _ _ _) >== | |
| (repeat p n *> p) *> inv p ==< idp >== | |
| repeat p (suc n) *> inv p ==< idp >== | |
| irepeat p (pos (suc n)) *> inv p `qed | |
| | neg n => idp | |
| -- | Same as ``repeat_*>_inv``, but on the rhs we have first the repetition of the inverted path and then the repetition of | |
| -- | the original path. | |
| \func repeat_inv_*> {A : \Type} {a : A} {p : a = a} (m n : Nat) : irepeat p (m - n) = repeat (inv p) n *> repeat p m \elim m, n | |
| | 0, n => idp | |
| | m, 0 => inv (idp_*> _) | |
| | suc m, suc n => | |
| irepeat p (m - n) ==< repeat_inv_*> m n >== | |
| repeat (inv p) n *> repeat p m ==< idp >== | |
| (repeat (inv p) n *> idp) *> repeat p m ==< pmap ((`*> _) o (_ *>)) (inv (inv_*> p)) >== | |
| (repeat (inv p) n *> inv p *> p) *> repeat p m ==< pmap (`*> _) (inv (*>-assoc _ _ _)) >== | |
| ((repeat (inv p) n *> inv p) *> p) *> repeat p m ==< *>-assoc _ _ _ >== | |
| (repeat (inv p) n *> inv p) *> p *> repeat p m ==< pmap (_ *>) (inv (repeat_suc _)) >== | |
| repeat (inv p) (suc n) *> repeat p (suc m) `qed | |
| -- | ``irepeat`` turns addition of integers into concatenation of paths. | |
| \func irepeat_+ {A : \Type} {a : A} {p : a = a} (j k : Int) : irepeat p (j IntRing.+ k) = irepeat p j *> irepeat p k \elim j, k | |
| | pos m, pos n => repeat_+ m n | |
| | pos m, neg (suc n) => repeat_*>_inv m (suc n) | |
| | neg (suc m), pos n => repeat_inv_*> n (suc m) | |
| | neg (suc m), neg (suc n) => repeat_+ (suc m) (suc n) | |
| -- | ``irepeat`` turns negation of an integer into inversion of a path. | |
| \func irepeat_negative {A : \Type} {a : A} {p : a = a} (k : Int) : irepeat p (negative k) = inv (irepeat p k) \elim k | |
| | pos n => | |
| irepeat p (negative (pos n)) ==< idp >== | |
| irepeat p (neg n) ==< idp >== | |
| repeat (inv p) n ==< repeat_inv n >== | |
| inv (repeat p n) ==< idp >== | |
| inv (irepeat p (pos n)) `qed | |
| | neg n => | |
| irepeat p (negative (neg n)) ==< idp >== | |
| irepeat p (pos n) ==< idp >== | |
| repeat p n ==< pmap (repeat __ n) (inv (inv_inv p)) >== | |
| repeat (inv (inv p)) n ==< repeat_inv n >== | |
| inv (repeat (inv p) n) ==< idp >== | |
| inv (irepeat p (neg n)) `qed | |
| -- # Extending irepeat to the "reals" | |
| {- | The path from ``Int`` to itself representing the bijection Z -> Z, k |-> k + 1. | |
| - | If one interprets the interval type ``I`` as the real interval [0, 1], ``left`` as 0 and ``right`` as 1, then one | |
| - | can view this path as the function that assigns to each i in [0, 1] the set Z + i, i.e. the embedding of Z in R | |
| - | shifted by i. | |
| - | Going from i to j would correspond to the the bijection Z + i -> Z + j, k + i |-> k + j, so going from 0 all the | |
| - | way to 1 would correspond to the original bijection Z -> Z + 1 = Z, k |-> k + 1. | |
| - | This intuition is important for understanding the rest of the proof. | |
| -} | |
| \func Int=Int : I -> \Set => iso isuc ipred ipred_isuc isuc_ipred | |
| {- | When we say we want to extend irepeat to the "real" inputs, what we really mean is finding a function rrepeat that | |
| - | takes a loop ``p : a = a``, an i from [0, 1] and an x from Z + i as input and produces a path ``a = p @ i`` as | |
| - | output, in such a way that both ``rrepeat p left`` : Z + 0 -> a = a and ``rrepeat p right`` : Z + 1 -> a = a behave | |
| - | identically to ``irepeat p`` : Z -> a = a. In order to do this, I have come up with the following idea: Given an i | |
| - | from [0, 1] and an x from Z + i, first shift x up to the next integer, which would be x + 1 - i. As this is an | |
| - | integer, we may apply ``irepeat`` to it and obtain a path ``p : a = a``. As we have previously shifted x up by | |
| - | 1 - i, we now wind ``p`` back by exactly that much, i.e. 1 - i, which allows us to obtain a path base = loop i. If | |
| - | i is ``left``, then we would have concatenated ``p`` to itself x + 1 times, followed by a concatenation with | |
| - | ``inv p``, which is identical (up to homotopy) to just concatenating ``p`` to itself x times, which is also what | |
| - | ``irepeat`` would give as a result; If i is ``right``, then we would have neither the shifting-up in the beginning | |
| - | nor the winding-back in the end, so this process would also be simply identical to ``irepeat``. | |
| - | The first part of this process, i.e. shifting from Z + i to Z + 1, is fulfilled by this function, which I call | |
| - | ``dialUp`` rather than ``shiftUp`` as we are really shifting in circles: Z + i is a copy of Z shifted by i, and we | |
| - | are shifting Z + i further up till we reach Z again. | |
| -} | |
| \func dialUp (i : I) (k : Int=Int i) : Int => coe2 Int=Int i k right | |
| -- | The actual function ``rrepeat``, as described in the doc for ``dialUp``. | |
| \func rrepeat {A : \Type} {a : A} (p : a = a) (i : I) (k : Int=Int i) : a = p @ i => | |
| irepeat p (dialUp i k) *> inv (path ((p @) o I.squeezeR i)) | |
| -- | ``rrepeat p left`` behaves the same as ``irepeat p``. The equation ``rrepeat p right = irepeat p`` already holds | |
| -- | definitionally. | |
| \func rrepeat-left {A : \Type} {a : A} {p : a = a} (k : Int) : rrepeat p left k = irepeat p k => | |
| rrepeat p left k ==< idp >== | |
| irepeat p (dialUp left k) *> inv (path ((p @) o I.squeezeR left)) ==< idp >== | |
| irepeat p (coe2 Int=Int left k right) *> inv (path \lam j => p @ I.squeezeR left j) ==< idp >== | |
| irepeat p (coe Int=Int k right) *> inv (path \lam j => p @ j) ==< idp >== | |
| irepeat p (isuc k) *> inv (path (p @)) ==< pmap (`*> _) (irepeat_isuc k) >== | |
| (irepeat p k *> p) *> inv p ==< *>-assoc _ _ _ >== | |
| irepeat p k *> p *> inv p ==< pmap (_ *>) (*>_inv p) >== | |
| irepeat p k *> idp ==< idp >== | |
| irepeat p k `qed | |
| -- | Functional extensionality. Can't seem to find it in the standard library, so I copied it here from Arend's website. | |
| \func funExt {A : \Type} (B : A -> \Type) (f g : \Pi (x : A) -> B x) (h : \Pi (x : A) -> f x = g x) : f = g => | |
| path \lam i a => h a @ i | |
| -- | ``rrepeat`` is indeed a continuation of ``irepeat``. | |
| \func rrepeat-compat {A : \Type} {a : A} (p : a = a) : Path (\lam i => Int=Int i -> a = p @ i) (irepeat p) (irepeat p) => | |
| transport (Path _ __ _) (funExt _ _ _ rrepeat-left) (path (rrepeat p)) | |
| -- # The circle, winding and unwinding | |
| -- | The ``Circle`` type, which can be thought of representing S1 with a fixed base point | |
| \data Circle | |
| | base | |
| | loop I \with { | |
| | left => base | |
| | right => base | |
| } | |
| -- | The simple loop, which is the generator of the fundamental group of ``base``. | |
| \func ploop : base = base => path loop | |
| -- | The inverse of ``ploop``. | |
| \func iploop : base = base => inv ploop | |
| -- | We wrap the ``Circle`` (S1) around ``Int`` (Z) in the space of types, with the simple loop mapped to the path represented | |
| -- | by ``Int=Int``. | |
| \func wrap (_ : Circle) : \Set \with | |
| | base => Int | |
| | loop i => Int=Int i | |
| -- | Winding ``ploop`` around ``base``. | |
| \func wind {c : Circle} : wrap c -> base = c \elim c | |
| | base => irepeat ploop | |
| | loop i => rrepeat-compat ploop @ i | |
| -- | Compute the winding number for a path starting at ``base``. | |
| \func unwind {c : Circle} (p : base = c) : wrap c => | |
| transport wrap p 0 | |
| -- | Transporting an integer along ``wind j`` is the same as adding ``j`` to it. | |
| -- | One can in fact prove a more general version of this equality where ``j`` doesn't have to be an ``Int`` (Z), but | |
| -- | any ``Int=Int i`` (Z + i). But in order to formulate this more general theorem one first needs to extend integer | |
| -- | addition to all ``Int=Int i``, which I am to lazy to do. | |
| \lemma wrap_wind (j k : Int) : transport wrap (wind {base} j) k = j IntRing.+ k \elim j | |
| | 0 => inv IntRing.zro-left | |
| | pos (suc m) => | |
| transport wrap (wind {base} (pos (suc m))) k ==< idp >== | |
| transport wrap (repeat ploop (suc m)) k ==< idp >== | |
| transport wrap (repeat ploop m *> ploop) k ==< transport_*> wrap _ _ k >== | |
| transport wrap ploop (transport wrap (repeat ploop m) k) ==< idp >== | |
| isuc (transport wrap (wind {base} (pos m)) k) ==< pmap isuc (wrap_wind (pos m) k) >== | |
| isuc (pos m IntRing.+ k) ==< inv IntRing.suc-left >== | |
| pos (suc m) IntRing.+ k `qed | |
| | neg (suc m) => | |
| transport wrap (wind {base} (neg (suc m))) k ==< inv (ipred_isuc _) >== | |
| ipred (isuc (transport wrap (wind {base} (neg (suc m))) k)) ==< idp >== | |
| ipred (transport wrap ploop (transport wrap (wind {base} (neg (suc m))) k)) ==< pmap ipred (inv (transport_*> wrap _ ploop k)) >== | |
| ipred (transport wrap (wind (neg (suc m)) *> ploop) k) ==< idp >== | |
| ipred (transport wrap (repeat iploop (suc m) *> ploop) k) ==< idp >== | |
| ipred (transport wrap ((repeat iploop m *> iploop) *> ploop) k) ==< pmap (\lam p => ipred (transport wrap p _)) (*>-assoc _ _ _) >== | |
| ipred (transport wrap (repeat iploop m *> iploop *> ploop) k) ==< pmap (\lam p => ipred (transport wrap (repeat iploop m *> p) k)) (inv_*> _) >== | |
| ipred (transport wrap (repeat iploop m *> idp) k) ==< idp >== | |
| ipred (transport wrap (repeat iploop m) k) ==< idp >== | |
| ipred (transport wrap (wind {base} (neg m)) k) ==< pmap ipred (wrap_wind (neg m) k) >== | |
| ipred (neg m IntRing.+ k) ==< inv IntRing.pred-left >== | |
| neg (suc m) IntRing.+ k `qed | |
| -- | ``unwind o wind = id`` | |
| \lemma unwind_wind (k : Int) : unwind (wind {base} k) = k => | |
| wrap_wind k 0 *> IntRing.zro-right | |
| -- | ``wind o unwind = id`` | |
| \func wind_unwind {c : Circle} (p : base = c) : wind (unwind p) = p \with | |
| | idp => idp | |
| -- | Finally, ``Int`` and ``base = base`` are homeomorphic and therefore equal. This together with the algebraic | |
| -- | properties of ``irepeat`` we proved earlier establish the well-known fact that the fundamental group of the pointed | |
| -- | circle (here represented as the type ``Circle`` with base at ``base``) is isomorphic to the group of integers. | |
| \func Int=loops : Int = (base = base) => | |
| iso wind unwind unwind_wind wind_unwind |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment