Morphisms of the slice category of types

module foundation.slice where
Imports
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.homotopies
open import foundation.structure-identity-principle
open import foundation.type-theoretic-principle-of-choice
open import foundation.univalence

open import foundation-core.contractible-types
open import foundation-core.dependent-pair-types
open import foundation-core.embeddings
open import foundation-core.equality-dependent-pair-types
open import foundation-core.fibers-of-maps
open import foundation-core.functions
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.fundamental-theorem-of-identity-types
open import foundation-core.identity-types
open import foundation-core.injective-maps
open import foundation-core.propositional-maps
open import foundation-core.propositions
open import foundation-core.type-arithmetic-dependent-pair-types
open import foundation-core.universe-levels

open import trees.polynomial-endofunctors

Idea

The slice of a category over an object X is the category of morphisms into X. A morphism in the slice from f : A → X to g : B → X consists of a function h : A → B such that the triangle f ~ g ∘ h commutes. We make these definitions for types.

Definition

The objects of the slice category of types

Slice : (l : Level) {l1 : Level} (A : UU l1)  UU (l1  lsuc l)
Slice l = type-polynomial-endofunctor (UU l)  X  X)

The morphisms of the slice category of types

module _
  {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : UU l3}
  where

  hom-slice :
    (A  X)  (B  X)  UU (l1  l2  l3)
  hom-slice f g = Σ (A  B)  h  f ~ (g  h))

  map-hom-slice :
    (f : A  X) (g : B  X)  hom-slice f g  A  B
  map-hom-slice f g h = pr1 h

  triangle-hom-slice :
    (f : A  X) (g : B  X) (h : hom-slice f g) 
    f ~ (g  (map-hom-slice f g h))
  triangle-hom-slice f g h = pr2 h

Properties

We characterize the identity type of hom-slice

module _
  {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : UU l3}
  (f : A  X) (g : B  X)
  where

  htpy-hom-slice : (h h' : hom-slice f g)  UU (l1  l2  l3)
  htpy-hom-slice h h' =
    Σ ( map-hom-slice f g h ~ map-hom-slice f g h')
      ( λ K 
        ( (triangle-hom-slice f g h) ∙h (g ·l K)) ~
        ( triangle-hom-slice f g h'))

  extensionality-hom-slice :
    (h h' : hom-slice f g)  (h  h')  htpy-hom-slice h h'
  extensionality-hom-slice (pair h H) =
    extensionality-Σ
      ( λ {h'} H' (K : h ~ h')  (H ∙h (g ·l K)) ~ H')
      ( refl-htpy)
      ( right-unit-htpy)
      ( λ h'  equiv-funext)
      ( λ H'  equiv-concat-htpy right-unit-htpy H' ∘e equiv-funext)

  eq-htpy-hom-slice :
    (h h' : hom-slice f g)  htpy-hom-slice h h'  h  h'
  eq-htpy-hom-slice h h' = map-inv-equiv (extensionality-hom-slice h h')
comp-hom-slice :
  {l1 l2 l3 l4 : Level} {X : UU l1} {A : UU l2} {B : UU l3} {C : UU l4}
  (f : A  X) (g : B  X) (h : C  X) 
  hom-slice g h  hom-slice f g  hom-slice f h
pr1 (comp-hom-slice f g h j i) = map-hom-slice g h j  map-hom-slice f g i
pr2 (comp-hom-slice f g h j i) =
  ( triangle-hom-slice f g i) ∙h
  ( (triangle-hom-slice g h j) ·r (map-hom-slice f g i))

id-hom-slice :
  {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A  X)  hom-slice f f
pr1 (id-hom-slice f) = id
pr2 (id-hom-slice f) = refl-htpy

is-equiv-hom-slice :
  {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : UU l3}
  (f : A  X) (g : B  X)  hom-slice f g  UU (l2  l3)
is-equiv-hom-slice f g h = is-equiv (map-hom-slice f g h)

Morphisms in the slice are equivalently described as families of maps between fibers

module _
  {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : UU l3}
  where

  fiberwise-hom : (A  X)  (B  X)  UU (l1  l2  l3)
  fiberwise-hom f g = (x : X)  fib f x  fib g x

module _
  {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : UU l3}
  (f : A  X) (g : B  X)
  where

  fiberwise-hom-hom-slice : hom-slice f g  fiberwise-hom f g
  fiberwise-hom-hom-slice (pair h H) = fib-triangle f g h H

  hom-slice-fiberwise-hom : fiberwise-hom f g  hom-slice f g
  pr1 (hom-slice-fiberwise-hom α) a = pr1 (α (f a) (pair a refl))
  pr2 (hom-slice-fiberwise-hom α) a = inv (pr2 (α (f a) (pair a refl)))

  issec-hom-slice-fiberwise-hom-eq-htpy :
    (α : fiberwise-hom f g) (x : X) 
    (fiberwise-hom-hom-slice (hom-slice-fiberwise-hom α) x) ~ (α x)
  issec-hom-slice-fiberwise-hom-eq-htpy α .(f a) (pair a refl) =
    eq-pair-Σ refl (inv-inv (pr2 (α (f a) (pair a refl))))

  issec-hom-slice-fiberwise-hom :
    (fiberwise-hom-hom-slice  hom-slice-fiberwise-hom) ~ id
  issec-hom-slice-fiberwise-hom α =
    eq-htpy  x  eq-htpy (issec-hom-slice-fiberwise-hom-eq-htpy α x))

  isretr-hom-slice-fiberwise-hom :
    (hom-slice-fiberwise-hom  fiberwise-hom-hom-slice) ~ id
  isretr-hom-slice-fiberwise-hom (pair h H) =
    eq-pair-Σ refl (eq-htpy (inv-inv  H))

  abstract
    is-equiv-fiberwise-hom-hom-slice : is-equiv (fiberwise-hom-hom-slice)
    is-equiv-fiberwise-hom-hom-slice =
      is-equiv-has-inverse
        ( hom-slice-fiberwise-hom)
        ( issec-hom-slice-fiberwise-hom)
        ( isretr-hom-slice-fiberwise-hom)

  equiv-fiberwise-hom-hom-slice : hom-slice f g  fiberwise-hom f g
  pr1 equiv-fiberwise-hom-hom-slice = fiberwise-hom-hom-slice
  pr2 equiv-fiberwise-hom-hom-slice = is-equiv-fiberwise-hom-hom-slice

  abstract
    is-equiv-hom-slice-fiberwise-hom : is-equiv hom-slice-fiberwise-hom
    is-equiv-hom-slice-fiberwise-hom =
      is-equiv-has-inverse
        ( fiberwise-hom-hom-slice)
        ( isretr-hom-slice-fiberwise-hom)
        ( issec-hom-slice-fiberwise-hom)

  equiv-hom-slice-fiberwise-hom :
    fiberwise-hom f g  hom-slice f g
  pr1 equiv-hom-slice-fiberwise-hom = hom-slice-fiberwise-hom
  pr2 equiv-hom-slice-fiberwise-hom = is-equiv-hom-slice-fiberwise-hom

A morphism in the slice over X is an equivalence if and only if the induced map between fibers is a fiberwise equivalence

module _
  {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : UU l3}
  where

  equiv-slice : (A  X)  (B  X)  UU (l1  l2  l3)
  equiv-slice f g = Σ (A  B)  e  f ~ (g  map-equiv e))

  hom-equiv-slice :
    (f : A  X) (g : B  X)  equiv-slice f g  hom-slice f g
  pr1 (hom-equiv-slice f g e) = pr1 (pr1 e)
  pr2 (hom-equiv-slice f g e) = pr2 e

module _
  {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : UU l3}
  (f : A  X) (g : B  X)
  where

  abstract
    is-fiberwise-equiv-fiberwise-equiv-equiv-slice :
      (t : hom-slice f g)  is-equiv (pr1 t) 
      is-fiberwise-equiv (fiberwise-hom-hom-slice f g t)
    is-fiberwise-equiv-fiberwise-equiv-equiv-slice (pair h H) =
      is-fiberwise-equiv-is-equiv-triangle f g h H

  abstract
    is-equiv-hom-slice-is-fiberwise-equiv-fiberwise-hom-hom-slice :
      (t : hom-slice f g) 
      ((x : X)  is-equiv (fiberwise-hom-hom-slice f g t x)) 
      is-equiv (pr1 t)
    is-equiv-hom-slice-is-fiberwise-equiv-fiberwise-hom-hom-slice
      (pair h H) =
      is-equiv-triangle-is-fiberwise-equiv f g h H

  equiv-fiberwise-equiv-equiv-slice :
    equiv-slice f g  fiberwise-equiv (fib f) (fib g)
  equiv-fiberwise-equiv-equiv-slice =
    equiv-Σ is-fiberwise-equiv (equiv-fiberwise-hom-hom-slice f g) α ∘e
    equiv-right-swap-Σ
    where
      α :
        (h : hom-slice f g) 
        is-equiv (pr1 h) 
        is-fiberwise-equiv (map-equiv (equiv-fiberwise-hom-hom-slice f g) h)
      α h = equiv-prop
        ( is-property-is-equiv _)
        ( is-prop-Π  _  is-property-is-equiv _))
        ( is-fiberwise-equiv-fiberwise-equiv-equiv-slice h)
        ( is-equiv-hom-slice-is-fiberwise-equiv-fiberwise-hom-hom-slice h)

  equiv-equiv-slice-fiberwise-equiv :
    fiberwise-equiv (fib f) (fib g)  equiv-slice f g
  equiv-equiv-slice-fiberwise-equiv =
    inv-equiv equiv-fiberwise-equiv-equiv-slice

  fiberwise-equiv-equiv-slice :
    equiv-slice f g  fiberwise-equiv (fib f) (fib g)
  fiberwise-equiv-equiv-slice =
    map-equiv equiv-fiberwise-equiv-equiv-slice

  equiv-fam-equiv-equiv-slice :
    equiv-slice f g  ((x : X)  fib f x  fib g x) -- fam-equiv (fib f) (fib g)
  equiv-fam-equiv-equiv-slice =
    inv-distributive-Π-Σ ∘e equiv-fiberwise-equiv-equiv-slice

The type of slice morphisms into an embedding is a proposition

module _
  {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : UU l3}
  where

  abstract
    is-prop-hom-slice :
     (f : A  X) (i : B  X)  is-prop (hom-slice f (map-emb i))
    is-prop-hom-slice f i =
      is-prop-is-equiv
        ( is-equiv-fiberwise-hom-hom-slice f (map-emb i))
        ( is-prop-Π
          ( λ x  is-prop-Π
            ( λ p  is-prop-map-is-emb (is-emb-map-emb i) x)))

  abstract
    is-equiv-hom-slice-emb :
      (f : A  X) (g : B  X) (h : hom-slice (map-emb f) (map-emb g)) 
      hom-slice (map-emb g) (map-emb f) 
      is-equiv-hom-slice (map-emb f) (map-emb g) h
    is-equiv-hom-slice-emb f g h i =
      is-equiv-has-inverse
        ( map-hom-slice (map-emb g) (map-emb f) i)
        ( λ y 
          is-injective-emb g
          ( inv
            ( ( triangle-hom-slice
                ( map-emb g)
                ( map-emb f)
                ( i)
                ( y)) 
              ( triangle-hom-slice
                ( map-emb f)
                ( map-emb g)
                ( h)
                ( map-hom-slice (map-emb g) (map-emb f) i y)))))
        ( λ x 
          is-injective-emb f
          ( inv
            ( ( triangle-hom-slice (map-emb f) (map-emb g) h x) 
              ( triangle-hom-slice (map-emb g) (map-emb f) i
                ( map-hom-slice
                  ( map-emb f)
                  ( map-emb g)
                  ( h)
                  ( x))))))

Characterization of the identity type of Slice l A

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

  equiv-slice' : (f g : Slice l2 A)  UU (l1  l2)
  equiv-slice' f g = equiv-slice (pr2 f) (pr2 g)

  id-equiv-Slice : (f : Slice l2 A)  equiv-slice' f f
  pr1 (id-equiv-Slice f) = id-equiv
  pr2 (id-equiv-Slice f) = refl-htpy

  equiv-eq-Slice : (f g : Slice l2 A)  f  g  equiv-slice' f g
  equiv-eq-Slice f .f refl = id-equiv-Slice f

Univalence in a slice

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

  abstract
    is-contr-total-equiv-slice' :
      (f : Slice l2 A)  is-contr (Σ (Slice l2 A) (equiv-slice' f))
    is-contr-total-equiv-slice' (pair X f) =
      is-contr-total-Eq-structure
        ( λ Y g e  f ~ (g  map-equiv e))
        ( is-contr-total-equiv X)
        ( pair X id-equiv)
        ( is-contr-total-htpy f)

  abstract
    is-equiv-equiv-eq-Slice :
      (f g : Slice l2 A)  is-equiv (equiv-eq-Slice f g)
    is-equiv-equiv-eq-Slice f =
      fundamental-theorem-id
        ( is-contr-total-equiv-slice' f)
        ( equiv-eq-Slice f)

  extensionality-Slice :
    (f g : Slice l2 A)  (f  g)  equiv-slice' f g
  pr1 (extensionality-Slice f g) = equiv-eq-Slice f g
  pr2 (extensionality-Slice f g) = is-equiv-equiv-eq-Slice f g

  eq-equiv-slice :
    (f g : Slice l2 A)  equiv-slice' f g  f  g
  eq-equiv-slice f g =
    map-inv-is-equiv (is-equiv-equiv-eq-Slice f g)

See also