Retracts of types

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-11-09.
Last modified on 2024-04-17.

module foundation.retracts-of-types where

open import foundation-core.retracts-of-types public
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.homotopy-algebra
open import foundation.homotopy-induction
open import foundation.structure-identity-principle
open import foundation.univalence
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import foundation-core.contractible-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.identity-types
open import foundation-core.torsorial-type-families


We say that a type A is a retract of a type B if the types A and B come equipped with retract data, i.e., with maps

      i        r
  A -----> B -----> A

such that r is a retraction of i, i.e., there is a homotopy r ∘ i ~ id. The map i is called the inclusion of the retract data, and the map r is called the underlying map of the retraction.


Characterizing equality of retracts

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}

  coherence-htpy-retract :
    (R S : A retract-of B)
    (I : inclusion-retract R ~ inclusion-retract S)
    (H : map-retraction-retract R ~ map-retraction-retract S) 
    UU l1
  coherence-htpy-retract R S I H =
    ( is-retraction-map-retraction-retract R) ~
    ( horizontal-concat-htpy H I ∙h is-retraction-map-retraction-retract S)

  htpy-retract : (R S : A retract-of B)  UU (l1  l2)
  htpy-retract R S =
    Σ ( inclusion-retract R ~ inclusion-retract S)
      ( λ I 
        Σ ( map-retraction-retract R ~ map-retraction-retract S)
          ( coherence-htpy-retract R S I))

  refl-htpy-retract : (R : A retract-of B)  htpy-retract R R
  refl-htpy-retract R = (refl-htpy , refl-htpy , refl-htpy)

  htpy-eq-retract : (R S : A retract-of B)  R  S  htpy-retract R S
  htpy-eq-retract R .R refl = refl-htpy-retract R

  is-torsorial-htpy-retract :
    (R : A retract-of B)  is-torsorial (htpy-retract R)
  is-torsorial-htpy-retract R =
      ( is-torsorial-htpy (inclusion-retract R))
      ( inclusion-retract R , refl-htpy)
      ( is-torsorial-Eq-structure
        ( is-torsorial-htpy (map-retraction-retract R))
        ( map-retraction-retract R , refl-htpy)
        ( is-torsorial-htpy (is-retraction-map-retraction-retract R)))

  is-equiv-htpy-eq-retract :
    (R S : A retract-of B)  is-equiv (htpy-eq-retract R S)
  is-equiv-htpy-eq-retract R =
    fundamental-theorem-id (is-torsorial-htpy-retract R) (htpy-eq-retract R)

  equiv-htpy-eq-retract : (R S : A retract-of B)  (R  S)  htpy-retract R S
  equiv-htpy-eq-retract R S =
    ( htpy-eq-retract R S , is-equiv-htpy-eq-retract R S)

  eq-htpy-retract : (R S : A retract-of B)  htpy-retract R S  R  S
  eq-htpy-retract R S = map-inv-is-equiv (is-equiv-htpy-eq-retract R S)

Characterizing equality of the total type of retracts

module _
  {l1 l2 : Level} {A : UU l1}

  equiv-retracts :
    {l3 : Level} (R : retracts l2 A) (S : retracts l3 A)  UU (l1  l2  l3)
  equiv-retracts R S =
    Σ ( type-retracts R  type-retracts S)
      ( λ e 
          ( retract-retracts R)
          ( comp-retract (retract-retracts S) (retract-equiv e)))

  refl-equiv-retracts : (R : retracts l2 A)  equiv-retracts R R
  refl-equiv-retracts R =
    ( id-equiv ,
      refl-htpy ,
      refl-htpy ,
      ( ( inv-htpy
          ( left-unit-law-left-whisker-comp
            ( is-retraction-map-retraction-retracts R))) ∙h
        ( inv-htpy-right-unit-htpy)))

  equiv-eq-retracts : (R S : retracts l2 A)  R  S  equiv-retracts R S
  equiv-eq-retracts R .R refl = refl-equiv-retracts R

  is-torsorial-equiv-retracts :
    (R : retracts l2 A)  is-torsorial (equiv-retracts R)
  is-torsorial-equiv-retracts R =
      ( is-torsorial-equiv (type-retracts R))
      ( type-retracts R , id-equiv)
      ( is-contr-equiv
        ( Σ (retract A (type-retracts R)) (htpy-retract (retract-retracts R)))
        ( equiv-tot
          ( λ S 
              ( λ I 
                  ( λ J 
                      ( is-retraction-map-retraction-retracts R)
                      ( ap-concat-htpy
                        ( horizontal-concat-htpy J I)
                        ( right-unit-htpy ∙h
                            ( is-retraction-map-retraction-retract S)))))))
        ( is-torsorial-htpy-retract (retract-retracts R)))

  is-equiv-equiv-eq-retracts :
    (R S : retracts l2 A)  is-equiv (equiv-eq-retracts R S)
  is-equiv-equiv-eq-retracts R =
    fundamental-theorem-id (is-torsorial-equiv-retracts R) (equiv-eq-retracts R)

  equiv-equiv-eq-retracts : (R S : retracts l2 A)  (R  S)  equiv-retracts R S
  equiv-equiv-eq-retracts R S =
    ( equiv-eq-retracts R S , is-equiv-equiv-eq-retracts R S)

  eq-equiv-retracts : (R S : retracts l2 A)  equiv-retracts R S  R  S
  eq-equiv-retracts R S = map-inv-is-equiv (is-equiv-equiv-eq-retracts R S)

See also

Recent changes