Skip to content

Instantly share code, notes, and snippets.

@ma82
Created Oct 1, 2013
Embed
What would you like to do?
Instance resolution-friendly iterated loop space definitions for HoTT-Agda.
{-# OPTIONS --without-K #-}
open import lib.Basics
open import lib.types.Nat
open import lib.types.TLevel
open import lib.types.Empty
open import lib.types.Pi
open import lib.types.Truncation
open import lib.types.Pointed
open import lib.types.Group
module lib.types.LoopSpace where
-- Being "pointed" (inhabited) as a predicate.
record [_]∙ {i}(A : Type i) : Type i where
constructor <_>
field >_< : A
pointed : {i}⦃ X : Ptd i ⦄ [ fst X ]∙
pointed ⦃ _ , p ⦄ = < p >
thePoint : {i}{X : Type i}⦃ _ : [ X ]∙ ⦄ X
thePoint ⦃ < x > ⦄ = x
-- The original version.
module Orig {i} where
Ptd-Ω : Ptd i Ptd i
Ptd-Ω (A , a) = ∙[ (a == a) , idp ]
Ω : Ptd i Type i
Ω = fst ∘ Ptd-Ω
Ptd-Ω^ : (n : ℕ) Ptd i Ptd i
Ptd-Ω^ O X = X
Ptd-Ω^ (S n) X = Ptd-Ω (Ptd-Ω^ n X)
Ω^ : (n : ℕ) Ptd i Type i
Ω^ n X = fst (Ptd-Ω^ n X)
idp^ : (n : ℕ) {X : Ptd i} Ω^ n X
idp^ n {X} = snd (Ptd-Ω^ n X)
private
test : {X} Ptd-Ω^ 1 X == Ptd-Ω X
test = idp
-- To obtain better instance resolution we should prevent `Ω^ 0 A`
-- from being definitionally equal to `A`. We can use a specialised
-- "newtype" for `Orig.Ω^`.
module OrigWrap {i} where
record Ω^ (n : ℕ)(X : Ptd i) : Type i where
constructor <_>
field >_< : Orig.Ω^ n X
idp^ : (n : ℕ) {X : Ptd i} Ω^ n X
idp^ n = < Orig.idp^ n >
Ptd-Ω^ : (n : ℕ) Ptd i Ptd i
Ptd-Ω^ n X = Ω^ n X , idp^ n
Ptd-Ω : Ptd i Ptd i
Ptd-Ω = Ptd-Ω^ 1
Ω : Ptd i Type i
Ω = Ω^ 1
orig≃origwrap : n {i}{A : Ptd i} Orig.Ω^ n A ≃ OrigWrap.Ω^ n A
orig≃origwrap n = <_> , record { g = >_<
; f-g = λ _ idp
; g-f = λ _ idp
; adj = λ _ idp }
where open OrigWrap ; open Ω^
orig==origwrap-ua : n {i}{A : Ptd i}
Orig.Ptd-Ω^ n A == OrigWrap.Ptd-Ω^ n A
orig==origwrap-ua n = ptd-ua (orig≃origwrap n) idp
-- One can also give a more "direct" definition of the iterated loop
-- space. I guess that having `Alt.Ptd-Ω^ n X` definitionally equal to
-- a pair might turn out to be handy. There is a mutually recursive
-- definition, though: I have not tried to obtain such a definition
-- using the eliminator for natural numbers.
module Alt {i} where
Ω^ : (n : ℕ) Ptd i Type i
idp^ : (n : ℕ){A : Ptd i} Ω^ n A
Ω^ O (X , _) = X
Ω^ (S n) A = _==_ {A = Ω^ n A} (idp^ n) (idp^ n)
idp^ O {A , a} = a
idp^ (S n) = idp
Ptd-Ω^ : (n : ℕ) Ptd i Ptd i
Ptd-Ω^ n X = Ω^ n X , idp^ n
Ptd-Ω : Ptd i Ptd i
Ptd-Ω = Ptd-Ω^ 1
Ω : Ptd i Type i
Ω = Ω^ 1
-- Orig.Ptd-Ω^ is isomorphic to Alt.Ptd-Ω^.
-- In fact, they are provably identical.
orig==alt : n {i}{A : Ptd i} Orig.Ptd-Ω^ n A == Alt.Ptd-Ω^ n A
orig==alt O = idp
orig==alt (S n) {i}{A} =
transport (λ X _==_ {A = Ptd i}
(snd X == snd X , idp {A = fst X})
(Alt.idp^ n == Alt.idp^ n , idp {A = Alt.Ω^ n A}))
(! (orig==alt n))
idp
orig≃alt : n {i}{A : Ptd i} Orig.Ω^ n A ≃ Alt.Ω^ n A
orig≃alt n = coe-equiv (ap fst (orig==alt n))
-- We can wrap Alt as well.
module AltWrap {i} where
record Ω^ (n : ℕ)(X : Ptd i) : Type i where
constructor <_>
field >_< : Alt.Ω^ n X
idp^ : (n : ℕ){A : Ptd i} Ω^ n A
idp^ n = < Alt.idp^ n >
Ptd-Ω^ : (n : ℕ) Ptd i Ptd i
Ptd-Ω^ n X = Ω^ n X , idp^ n
Ptd-Ω : Ptd i Ptd i
Ptd-Ω = Ptd-Ω^ 1
Ω : Ptd i Type i
Ω = Ω^ 1
alt≃altwrap : n {i}{A : Ptd i} Alt.Ω^ n A ≃ AltWrap.Ω^ n A
alt≃altwrap n = Ω^.<_> , record { g = Ω^.>_<
; f-g = λ _ idp
; g-f = λ _ idp
; adj = λ _ idp }
where open AltWrap
alt==altwrap-ua : n {i}{A : Ptd i}
Alt.Ptd-Ω^ n A == AltWrap.Ptd-Ω^ n A
alt==altwrap-ua n = ptd-ua (alt≃altwrap n) idp
-- Using *specialised* wrappers improves inference of instance
-- arguments.
module InstanceInferenceExample where
-- Please choose one of the following.
-- open Orig -- does not work
-- open OrigWrap -- works
-- open Alt -- does not work
open AltWrap -- works
inst1 : [ Unit ]∙
inst1 = < unit >
Unit∙ : Ptd _
Unit∙ = Unit , unit
ptd = λ {n} Ptd-Ω^ n Unit∙
inst2 : {n} [ Ω^ n Unit∙ ]∙
inst2 = pointed
example1 : Unit
example1 = thePoint
example2 : {n} Ω^ n Unit∙
example2 = thePoint
example3 : Ω^ 0 Unit∙
example3 = thePoint
-- I haven't touched the rest so it only typechecks with Orig or Alt,
-- but this could be easily fixed.
-- open Orig
open Alt
{- for n ≥ 1, we have a group structure on the loop space -}
module _ {i} where
!^ : (n : ℕ) ⦃ _ : n ≠ O ⦄ {X : Ptd i} Ω^ n X Ω^ n X
!^ O ⦃ posi ⦄ = ⊥-rec (posi idp)
!^ (S n) = !
conc^ : (n : ℕ) ⦃ _ : n ≠ O ⦄ {X : Ptd i} Ω^ n X Ω^ n X Ω^ n X
conc^ O ⦃ posi ⦄ = ⊥-rec (posi idp)
conc^ (S n) = _∙_
ap^ : {i j} (n : ℕ) {X : Ptd i} {Y : Ptd j}
fst (X ∙→ Y) fst (Ptd-Ω^ n X ∙→ Ptd-Ω^ n Y)
ap^ O F = F
ap^ (S n) F =
let (g , gpt) = ap^ n F
in (λ p ! gpt ∙ ap g p ∙ gpt), !-inv-l gpt
module _ {i} {X : Ptd i} where
{- Prove these as lemmas now
- so we don't have to deal with the n = O case later -}
conc^-unit-l : (n : ℕ) ⦃ _ : n ≠ O ⦄ (q : Ω^ n X)
(conc^ n (idp^ n) q) == q
conc^-unit-l O ⦃ posi ⦄ _ = ⊥-rec (posi idp)
conc^-unit-l (S n) _ = idp
conc^-unit-r : (n : ℕ) ⦃ _ : n ≠ O ⦄ (q : Ω^ n X)
(conc^ n q (idp^ n)) == q
conc^-unit-r O ⦃ posi ⦄ = ⊥-rec (posi idp)
conc^-unit-r (S n) = ∙-unit-r
conc^-assoc : (n : ℕ) ⦃ _ : n ≠ O ⦄ (p q r : Ω^ n X)
conc^ n (conc^ n p q) r == conc^ n p (conc^ n q r)
conc^-assoc O ⦃ posi ⦄ = ⊥-rec (posi idp)
conc^-assoc (S n) = ∙-assoc
!^-inv-l : (n : ℕ) ⦃ _ : n ≠ O ⦄ (p : Ω^ n X)
conc^ n (!^ n p) p == idp^ n
!^-inv-l O ⦃ posi ⦄ = ⊥-rec (posi idp)
!^-inv-l (S n) = !-inv-l
!^-inv-r : (n : ℕ) ⦃ _ : n ≠ O ⦄ (p : Ω^ n X)
conc^ n p (!^ n p) == idp^ n
!^-inv-r O ⦃ posi ⦄ = ⊥-rec (posi idp)
!^-inv-r (S n) = !-inv-r
abstract
ap^-conc^ : {i j} (n : ℕ) ⦃ _ : n ≠ O ⦄
{X : Ptd i} {Y : Ptd j} (F : fst (X ∙→ Y)) (p q : Ω^ n X)
fst (ap^ n F) (conc^ n p q) == conc^ n (fst (ap^ n F) p) (fst (ap^ n F) q)
ap^-conc^ O ⦃ posi ⦄ _ _ = ⊥-rec (posi idp)
ap^-conc^ (S n) {X = X} {Y = Y} F p q =
! gpt ∙ ap g (p ∙ q) ∙ gpt
=⟨ ap-∙ g p q |in-ctx (λ w ! gpt ∙ w ∙ gpt) ⟩
! gpt ∙ (ap g p ∙ ap g q) ∙ gpt
=⟨ lemma (ap g p) (ap g q) gpt ⟩
(! gpt ∙ ap g p ∙ gpt) ∙ (! gpt ∙ ap g q ∙ gpt) ∎
where
g : Ω^ n X Ω^ n Y
g = fst (ap^ n F)
gpt : g (idp^ n) == idp^ n
gpt = snd (ap^ n F)
lemma : {i} {A : Type i} {x y : A}
(p q : x == x) (r : x == y)
! r ∙ (p ∙ q) ∙ r == (! r ∙ p ∙ r) ∙ (! r ∙ q ∙ r)
lemma p q idp = ∙-unit-r (p ∙ q) ∙ (! (∙-unit-r p) ∙2 ! (∙-unit-r q))
{- ap^ preserves (pointed) equivalences -}
module _ {i j} {X : Ptd i} {Y : Ptd j} where
is-equiv-ap^ : (n : ℕ) (F : fst (X ∙→ Y)) (e : is-equiv (fst F))
is-equiv (fst (ap^ n F))
is-equiv-ap^ O F e = e
is-equiv-ap^ (S n) F e =
pre∙-is-equiv (! (snd (ap^ n F)))
∘ise post∙-is-equiv (snd (ap^ n F))
∘ise snd (equiv-ap (_ , is-equiv-ap^ n F e) _ _)
equiv-ap^ : (n : ℕ) (F : fst (X ∙→ Y)) (e : is-equiv (fst F))
Ω^ n X ≃ Ω^ n Y
equiv-ap^ n F e = (fst (ap^ n F) , is-equiv-ap^ n F e)
Ω^-level-in : {i} (m : ℕ₋₂) (n : ℕ) (X : Ptd i)
(has-level ((n -2) +2+ m) (fst X) has-level m (Ω^ n X))
Ω^-level-in m O X pX = pX
Ω^-level-in m (S n) X pX =
Ω^-level-in (S m) n X
(transport (λ k has-level k (fst X)) (! (+2+-βr (n -2) m)) pX)
(idp^ n) (idp^ n)
{- Pushing truncation through loop space -}
module _ {i} where
Trunc-Ω^ : (m : ℕ₋₂) (n : ℕ) (X : Ptd i)
Ptd-Trunc m (Ptd-Ω^ n X) == Ptd-Ω^ n (Ptd-Trunc ((n -2) +2+ m) X)
Trunc-Ω^ m O X = idp
Trunc-Ω^ m (S n) X =
Ptd-Trunc m (Ptd-Ω^ (S n) X)
=⟨ ! (pair= (Trunc=-path [ _ ] [ _ ]) (↓-idf-ua-in _ idp)) ⟩
Ptd-Ω (Ptd-Trunc (S m) (Ptd-Ω^ n X))
=⟨ ap Ptd-Ω (Trunc-Ω^ (S m) n X) ⟩
Ptd-Ω^ (S n) (Ptd-Trunc ((n -2) +2+ S m) X)
=⟨ +2+-βr (n -2) m |in-ctx (λ k Ptd-Ω^ (S n) (Ptd-Trunc k X)) ⟩
Ptd-Ω^ (S n) (Ptd-Trunc (S (n -2) +2+ m) X) ∎
Ω-Trunc-equiv : (m : ℕ₋₂) (X : Ptd i)
Ω (Ptd-Trunc (S m) X) ≃ Trunc m (Ω X)
Ω-Trunc-equiv m X = Trunc=-equiv [ snd X ] [ snd X ]
{- A loop space is a group if it has the right level -}
module _ {i} (n : ℕ) ⦃ _ : n ≠ O ⦄ (X : Ptd i) (pX : has-level ⟨ n ⟩ (fst X))
where
Ω^-group-structure : GroupStructure
(Ω^ n X)
(Ω^-level-in ⟨0⟩ n X $
transport (λ t has-level t (fst X)) (+2+-comm ⟨0⟩ (n -2)) pX)
Ω^-group-structure = record {
ident = idp^ n;
inv = !^ n;
comp = conc^ n;
unitl = conc^-unit-l n;
unitr = conc^-unit-r n;
assoc = conc^-assoc n;
invr = !^-inv-r n;
invl = !^-inv-l n
}
Ω^-group : Group i
Ω^-group = group _ _ Ω^-group-structure
{- Our definition of Ω^ builds up loops on the outside,
- but this is equivalent to building up on the inside -}
module _ {i} where
Ptd-Ω^-inner-path : (n : ℕ) (X : Ptd i)
Ptd-Ω^ (S n) X == Ptd-Ω^ n (Ptd-Ω X)
Ptd-Ω^-inner-path O X = idp
Ptd-Ω^-inner-path (S n) X = ap Ptd-Ω (Ptd-Ω^-inner-path n X)
Ptd-Ω^-inner-out : (n : ℕ) (X : Ptd i)
fst (Ptd-Ω^ (S n) X ∙→ Ptd-Ω^ n (Ptd-Ω X))
Ptd-Ω^-inner-out O _ = (idf _ , idp)
Ptd-Ω^-inner-out (S n) X = ap^ 1 (Ptd-Ω^-inner-out n X)
Ω^-inner-out : (n : ℕ) (X : Ptd i)
(Ω^ (S n) X Ω^ n (Ptd-Ω X))
Ω^-inner-out n X = fst (Ptd-Ω^-inner-out n X)
Ω^-inner-out-conc^ : (n : ℕ) ⦃ _ : n ≠ O ⦄ (X : Ptd i) (p q : Ω^ (S n) X)
Ω^-inner-out n X (conc^ (S n) p q)
== conc^ n (Ω^-inner-out n X p) (Ω^-inner-out n X q)
Ω^-inner-out-conc^ O ⦃ posi ⦄ X = ⊥-rec (posi idp)
Ω^-inner-out-conc^ (S n) X p q =
ap^-conc^ 1 (Ptd-Ω^-inner-out n X) p q
Ω^-inner-is-equiv : (n : ℕ) (X : Ptd i)
is-equiv (fst (Ptd-Ω^-inner-out n X))
Ω^-inner-is-equiv O X = is-eq (idf _) (idf _) (λ _ idp) (λ _ idp)
Ω^-inner-is-equiv (S n) X =
is-equiv-ap^ 1 (Ptd-Ω^-inner-out n X) (Ω^-inner-is-equiv n X)
Ω^-inner-equiv : (n : ℕ) (X : Ptd i) Ω^ (S n) X ≃ Ω^ n (Ptd-Ω X)
Ω^-inner-equiv n X = _ , Ω^-inner-is-equiv n X
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment