Retracts of types

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-11-09.
Last modified on 2024-02-06.

module foundation.retracts-of-types where
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import foundation-core.identity-types
open import foundation-core.precomposition-functions
open import foundation-core.retractions
open import foundation-core.sections


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

and 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.


The type of witnesses that A is a retract of B

The predicate retract B is used to assert that a type is a retract of B, i.e., the type retract B A is the type of maps from A to B that come equipped with a retraction.

We also introduce more intuitive infix notation A retract-of B to assert that A is a retract of B.

retract : {l1 l2 : Level}  UU l1  UU l2  UU (l1  l2)
retract B A = Σ (A  B) retraction

infix 6 _retract-of_

_retract-of_ :
  {l1 l2 : Level}  UU l1  UU l2  UU (l1  l2)
A retract-of B = retract B A

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (R : retract B A)

  inclusion-retract : A  B
  inclusion-retract = pr1 R

  retraction-retract : retraction inclusion-retract
  retraction-retract = pr2 R

  map-retraction-retract : B  A
  map-retraction-retract = map-retraction inclusion-retract retraction-retract

  is-retraction-map-retraction-retract :
    is-section map-retraction-retract inclusion-retract
  is-retraction-map-retraction-retract =
    is-retraction-map-retraction inclusion-retract retraction-retract

  section-retract : section map-retraction-retract
  pr1 section-retract = inclusion-retract
  pr2 section-retract = is-retraction-map-retraction-retract


If A is a retract of B with inclusion i : A → B, then x = y is a retract of i x = i y for any two elements x y : A

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (R : A retract-of B) (x y : A)

  retract-eq :
    (x  y) retract-of (inclusion-retract R x  inclusion-retract R y)
  pr1 retract-eq =
    ap (inclusion-retract R)
  pr2 retract-eq =
    retraction-ap (inclusion-retract R) (retraction-retract R) x y

If A is a retract of B then A → S is a retract of B → S via precomposition

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (R : A retract-of B) (S : UU l3)

  retract-precomp :
    (A  S) retract-of (B  S)
  pr1 retract-precomp =
    precomp (map-retraction-retract R) S
  pr1 (pr2 retract-precomp) =
    precomp (inclusion-retract R) S
  pr2 (pr2 retract-precomp) h =
    eq-htpy (h ·l is-retraction-map-retraction-retract R)

See also

Recent changes