The universal property of the circle

module synthetic-homotopy-theory.universal-property-circle where

open import foundation.contractible-maps
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.fibers-of-maps
open import foundation.function-extensionality
open import foundation.functions
open import foundation.functoriality-dependent-pair-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.propositions
open import foundation.sections
open import foundation.universe-levels

open import synthetic-homotopy-theory.free-loops

Definitions

Evaluating an ordinary function at a free loop

module _
  {l1 l2 : Level} {X : UU l1} (α : free-loop X) (Y : UU l2)
  where

  ev-free-loop : (X → Y) → free-loop Y
  ev-free-loop f = pair (f (base-free-loop α)) (ap f (loop-free-loop α))

The universal property of the circle

module _
  {l1 : Level} (l2 : Level) {X : UU l1} (α : free-loop X)
  where

  universal-property-circle : UU (l1 ⊔ lsuc l2)
  universal-property-circle = (Y : UU l2) → is-equiv (ev-free-loop α Y)

Evaluating a dependent function at a free loop

module _
  {l1 l2 : Level} {X : UU l1} (α : free-loop X) (P : X → UU l2)
  where

  ev-free-loop-Π : ((x : X) → P x) → free-dependent-loop α P
  pr1 (ev-free-loop-Π f) = f (base-free-loop α)
  pr2 (ev-free-loop-Π f) = apd f (loop-free-loop α)

The induction principle of the circle

module _
  {l1 : Level} (l2 : Level) {X : UU l1} (α : free-loop X)
  where

  induction-principle-circle : UU ((lsuc l2) ⊔ l1)
  induction-principle-circle = (P : X → UU l2) → sec (ev-free-loop-Π α P)

module _
  {l1 l2 : Level} {X : UU l1} (α : free-loop X)
  (H : {l : Level} → induction-principle-circle l α) (P : X → UU l2)
  (β : free-dependent-loop α P)
  where

  function-induction-principle-circle : (x : X) → P x
  function-induction-principle-circle = pr1 (H P) β

  compute-induction-principle-circle :
    (ev-free-loop-Π α P function-induction-principle-circle) ＝ β
  compute-induction-principle-circle = pr2 (H P) β

The dependent universal property of the circle

module _
  {l1 : Level} (l2 : Level) {X : UU l1} (α : free-loop X)
  where

  dependent-universal-property-circle : UU ((lsuc l2) ⊔ l1)
  dependent-universal-property-circle =
    (P : X → UU l2) → is-equiv (ev-free-loop-Π α P)

Properties

The induction principle of the circle implies the dependent universal property of the circle

To prove this, we have to show that the section of ev-free-loop-Π is also a retraction. This construction is also by the induction principle of the circle, but it requires (a minimal amount of) preparations.

module _
  {l1 : Level} {X : UU l1} (α : free-loop X)
  where

  free-dependent-loop-htpy :
    {l2 : Level} {P : X → UU l2} {f g : (x : X) → P x} →
    ( Eq-free-dependent-loop α P
      ( ev-free-loop-Π α P f)
      ( ev-free-loop-Π α P g)) →
    ( free-dependent-loop α (λ x → Id (f x) (g x)))
  pr1 (free-dependent-loop-htpy {l2} {P} {f} {g} (p , q)) = p
  pr2 (free-dependent-loop-htpy {l2} {P} {f} {g} (p , q)) =
    map-compute-path-over-eq-value f g (loop-free-loop α) p p q

  isretr-ind-circle :
    ( ind-circle : {l : Level} → induction-principle-circle l α)
    { l2 : Level} (P : X → UU l2) →
    ( ( function-induction-principle-circle α ind-circle P) ∘
      ( ev-free-loop-Π α P)) ~
    ( id)
  isretr-ind-circle ind-circle P f =
    eq-htpy
      ( function-induction-principle-circle α ind-circle
        ( eq-value
          ( function-induction-principle-circle α ind-circle P
            ( ev-free-loop-Π α P f))
          ( f))
        ( free-dependent-loop-htpy
          ( Eq-free-dependent-loop-eq α P _ _
            ( compute-induction-principle-circle α ind-circle P
              ( ev-free-loop-Π α P f)))))

  abstract
    dependent-universal-property-induction-principle-circle :
      ({l : Level} → induction-principle-circle l α) →
      ({l : Level} → dependent-universal-property-circle l α)
    dependent-universal-property-induction-principle-circle ind-circle P =
      is-equiv-has-inverse
        ( function-induction-principle-circle α ind-circle P)
        ( compute-induction-principle-circle α ind-circle P)
        ( isretr-ind-circle ind-circle P)

Uniqueness of the maps obtained from the universal property of the circle

module _
  {l1 : Level} {X : UU l1} (α : free-loop X)
  where

  abstract
    uniqueness-universal-property-circle :
      ({l : Level} → universal-property-circle l α) →
      {l2 : Level} (Y : UU l2) (α' : free-loop Y) →
      is-contr (Σ (X → Y) (λ f → Eq-free-loop (ev-free-loop α Y f) α'))
    uniqueness-universal-property-circle up-circle Y α' =
      is-contr-is-equiv'
        ( fib (ev-free-loop α Y) α')
        ( tot (λ f → Eq-eq-free-loop (ev-free-loop α Y f) α'))
        ( is-equiv-tot-is-fiberwise-equiv
          ( λ f → is-equiv-Eq-eq-free-loop (ev-free-loop α Y f) α'))
        ( is-contr-map-is-equiv (up-circle Y) α')

Uniqueness of the dependent functions obtained from the dependent universal property of the circle

module _
  {l1 : Level} {X : UU l1} (α : free-loop X)
  where

  uniqueness-dependent-universal-property-circle :
    ({l : Level} → dependent-universal-property-circle l α) →
    {l2 : Level} {P : X → UU l2} (k : free-dependent-loop α P) →
    is-contr
      ( Σ ( (x : X) → P x)
          ( λ h → Eq-free-dependent-loop α P (ev-free-loop-Π α P h) k))
  uniqueness-dependent-universal-property-circle dup-circle {l2} {P} k =
    is-contr-is-equiv'
      ( fib (ev-free-loop-Π α P) k)
      ( tot (λ h → Eq-free-dependent-loop-eq α P (ev-free-loop-Π α P h) k))
      ( is-equiv-tot-is-fiberwise-equiv
        (λ h → is-equiv-Eq-free-dependent-loop-eq α P (ev-free-loop-Π α P h) k))
      ( is-contr-map-is-equiv (dup-circle P) k)

The dependent universal property of the circle implies the universal property of the circle

module _
  {l1 l2 : Level} {X : UU l1} (α : free-loop X) (Y : UU l2)
  where

  triangle-comparison-free-loop :
    ( map-compute-free-dependent-loop-const α Y ∘ (ev-free-loop α Y)) ~
    ( ev-free-loop-Π α (λ x → Y))
  triangle-comparison-free-loop f =
    eq-Eq-free-dependent-loop α
      ( λ x → Y)
      ( map-compute-free-dependent-loop-const α Y
        ( ev-free-loop α Y f))
      ( ev-free-loop-Π α (λ x → Y) f)
      ( pair refl (right-unit ∙ (inv (apd-const f (loop-free-loop α)))))

module _
  {l1 : Level} {X : UU l1} (α : free-loop X)
  where

  abstract
    universal-property-dependent-universal-property-circle :
      ({l : Level} → dependent-universal-property-circle l α) →
      ({l : Level} → universal-property-circle l α)
    universal-property-dependent-universal-property-circle dup-circle Y =
      is-equiv-right-factor-htpy
        ( ev-free-loop-Π α (λ x → Y))
        ( map-compute-free-dependent-loop-const α Y)
        ( ev-free-loop α Y)
        ( inv-htpy (triangle-comparison-free-loop α Y))
        ( is-equiv-map-equiv (compute-free-dependent-loop-const α Y))
        ( dup-circle (λ x → Y))

The induction principle of the circle implies the universal property of the circle

module _
  {l1 : Level} {X : UU l1} (α : free-loop X)
  where

  abstract
    universal-property-induction-principle-circle :
      ({l : Level} → induction-principle-circle l α) →
      ({l : Level} → universal-property-circle l α)
    universal-property-induction-principle-circle X =
      universal-property-dependent-universal-property-circle α
        ( dependent-universal-property-induction-principle-circle α X)

The dependent universal property of the circle with respect to propositions

abstract
  is-connected-circle' :
    { l1 l2 : Level} {X : UU l1} (l : free-loop X) →
    ( dup-circle : dependent-universal-property-circle l2 l)
    ( P : X → UU l2) (is-prop-P : (x : X) → is-prop (P x)) →
    P (base-free-loop l) → (x : X) → P x
  is-connected-circle' l dup-circle P is-prop-P p =
    map-inv-is-equiv
      ( dup-circle P)
      ( pair p (center (is-prop-P _ (tr P (pr2 l) p) p)))