Cones over cospan diagrams

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2024-01-28.
Last modified on 2024-03-22.

module foundation.cones-over-cospan-diagrams where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.dependent-universal-property-equivalences
open import foundation.function-extensionality
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.homotopy-induction
open import foundation.identity-types
open import foundation.multivariable-homotopies
open import foundation.structure-identity-principle
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import foundation-core.commuting-squares-of-maps
open import foundation-core.contractible-types
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.torsorial-type-families
open import foundation-core.transport-along-identifications
open import foundation-core.whiskering-identifications-concatenation

Idea

A cone over a cospan diagram A -f-> X <-g- B with domain C is a triple (p, q, H) consisting of a map p : C → A, a map q : C → B, and a homotopy H witnessing that the square

        q
    C -----> B
    |        |
  p |        | g
    ∨        ∨
    A -----> X
        f

commutes.

Definitions

Cones over cospans

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

  cone : {l4 : Level} → UU l4 → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
  cone C = Σ (C → A) (λ p → Σ (C → B) (λ q → coherence-square-maps q p g f))

module _
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
  (f : A → X) (g : B → X) (c : cone f g C)
  where

  vertical-map-cone : C → A
  vertical-map-cone = pr1 c

  horizontal-map-cone : C → B
  horizontal-map-cone = pr1 (pr2 c)

  coherence-square-cone :
    coherence-square-maps horizontal-map-cone vertical-map-cone g f
  coherence-square-cone = pr2 (pr2 c)

Dependent cones over cospan diagrams

cone-family :
  {l1 l2 l3 l4 l5 l6 l7 l8 : Level}
  {X : UU l1} {A : UU l2} {B : UU l3} {C : UU l4}
  (PX : X → UU l5) {PA : A → UU l6} {PB : B → UU l7}
  {f : A → X} {g : B → X} →
  (f' : (a : A) → PA a → PX (f a)) (g' : (b : B) → PB b → PX (g b)) →
  cone f g C → (C → UU l8) → UU (l4 ⊔ l5 ⊔ l6 ⊔ l7 ⊔ l8)
cone-family {C = C} PX {f = f} {g} f' g' c PC =
  (x : C) →
  cone
    ( ( tr PX (coherence-square-cone f g c x)) ∘
      ( f' (vertical-map-cone f g c x)))
    ( g' (horizontal-map-cone f g c x))
    ( PC x)

Characterizing identifications of cones over cospan diagrams

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

  coherence-htpy-cone :
    (c c' : cone f g C)
    (K : vertical-map-cone f g c ~ vertical-map-cone f g c')
    (L : horizontal-map-cone f g c ~ horizontal-map-cone f g c') → UU (l4 ⊔ l3)
  coherence-htpy-cone c c' K L =
    ( coherence-square-cone f g c ∙h (g ·l L)) ~
    ( (f ·l K) ∙h coherence-square-cone f g c')

  htpy-cone : cone f g C → cone f g C → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
  htpy-cone c c' =
    Σ ( vertical-map-cone f g c ~ vertical-map-cone f g c')
      ( λ K →
        Σ ( horizontal-map-cone f g c ~ horizontal-map-cone f g c')
          ( coherence-htpy-cone c c' K))

  htpy-vertical-map-htpy-cone :
    (c c' : cone f g C) (H : htpy-cone c c') →
    vertical-map-cone f g c ~ vertical-map-cone f g c'
  htpy-vertical-map-htpy-cone c c' H = pr1 H

  htpy-horizontal-map-htpy-cone :
    (c c' : cone f g C) (H : htpy-cone c c') →
    horizontal-map-cone f g c ~ horizontal-map-cone f g c'
  htpy-horizontal-map-htpy-cone c c' H = pr1 (pr2 H)

  coh-htpy-cone :
    (c c' : cone f g C) (H : htpy-cone c c') →
    coherence-htpy-cone c c'
      ( htpy-vertical-map-htpy-cone c c' H)
      ( htpy-horizontal-map-htpy-cone c c' H)
  coh-htpy-cone c c' H = pr2 (pr2 H)

  refl-htpy-cone : (c : cone f g C) → htpy-cone c c
  pr1 (refl-htpy-cone c) = refl-htpy
  pr1 (pr2 (refl-htpy-cone c)) = refl-htpy
  pr2 (pr2 (refl-htpy-cone c)) = right-unit-htpy

  htpy-eq-cone : (c c' : cone f g C) → c ＝ c' → htpy-cone c c'
  htpy-eq-cone c .c refl = refl-htpy-cone c

  is-torsorial-htpy-cone :
    (c : cone f g C) → is-torsorial (htpy-cone c)
  is-torsorial-htpy-cone c =
    is-torsorial-Eq-structure
      ( is-torsorial-htpy (vertical-map-cone f g c))
      ( vertical-map-cone f g c , refl-htpy)
      ( is-torsorial-Eq-structure
        ( is-torsorial-htpy (horizontal-map-cone f g c))
        ( horizontal-map-cone f g c , refl-htpy)
        ( is-torsorial-htpy (coherence-square-cone f g c ∙h refl-htpy)))

  is-equiv-htpy-eq-cone : (c c' : cone f g C) → is-equiv (htpy-eq-cone c c')
  is-equiv-htpy-eq-cone c =
    fundamental-theorem-id (is-torsorial-htpy-cone c) (htpy-eq-cone c)

  extensionality-cone : (c c' : cone f g C) → (c ＝ c') ≃ htpy-cone c c'
  pr1 (extensionality-cone c c') = htpy-eq-cone c c'
  pr2 (extensionality-cone c c') = is-equiv-htpy-eq-cone c c'

  eq-htpy-cone : (c c' : cone f g C) → htpy-cone c c' → c ＝ c'
  eq-htpy-cone c c' = map-inv-equiv (extensionality-cone c c')

Precomposing cones over cospan diagrams with a map

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

  cone-map :
    {C : UU l4} → cone f g C → {C' : UU l5} → (C' → C) → cone f g C'
  pr1 (cone-map c h) = vertical-map-cone f g c ∘ h
  pr1 (pr2 (cone-map c h)) = horizontal-map-cone f g c ∘ h
  pr2 (pr2 (cone-map c h)) = coherence-square-cone f g c ·r h

Pasting cones horizontally

module _
  {l1 l2 l3 l4 l5 l6 : Level}
  {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} {Y : UU l5} {Z : UU l6}
  (i : X → Y) (j : Y → Z) (h : C → Z)
  where

  pasting-horizontal-cone :
    (c : cone j h B) → cone i (vertical-map-cone j h c) A → cone (j ∘ i) h A
  pr1 (pasting-horizontal-cone c (f , p , H)) = f
  pr1 (pr2 (pasting-horizontal-cone c (f , p , H))) =
    (horizontal-map-cone j h c) ∘ p
  pr2 (pr2 (pasting-horizontal-cone c (f , p , H))) =
    pasting-horizontal-coherence-square-maps p
      ( horizontal-map-cone j h c)
      ( f)
      ( vertical-map-cone j h c)
      ( h)
      ( i)
      ( j)
      ( H)
      ( coherence-square-cone j h c)

Vertical composition of cones

module _
  {l1 l2 l3 l4 l5 l6 : Level}
  {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} {Y : UU l5} {Z : UU l6}
  (f : C → Z) (g : Y → Z) (h : X → Y)
  where

  pasting-vertical-cone :
    (c : cone f g B) → cone (horizontal-map-cone f g c) h A → cone f (g ∘ h) A
  pr1 (pasting-vertical-cone c (p' , q' , H')) =
    ( vertical-map-cone f g c) ∘ p'
  pr1 (pr2 (pasting-vertical-cone c (p' , q' , H'))) = q'
  pr2 (pr2 (pasting-vertical-cone c (p' , q' , H'))) =
    pasting-vertical-coherence-square-maps q' p' h
      ( horizontal-map-cone f g c)
      ( vertical-map-cone f g c)
      ( g)
      ( f)
      ( H')
      ( coherence-square-cone f g c)

The swapping function on cones over cospans

swap-cone :
  {l1 l2 l3 l4 : Level}
  {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
  (f : A → X) (g : B → X) → cone f g C → cone g f C
pr1 (swap-cone f g c) = horizontal-map-cone f g c
pr1 (pr2 (swap-cone f g c)) = vertical-map-cone f g c
pr2 (pr2 (swap-cone f g c)) = inv-htpy (coherence-square-cone f g c)

Parallel cones over parallel cospan diagrams

Two cones with the same domain over parallel cospans are considered parallel if they are part of a fully coherent diagram: there is a fully coherent cube where all the vertical maps are identities, the top face is given by one cone, and the bottom face is given by the other.

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  {f f' : A → X} (Hf : f ~ f') {g g' : B → X} (Hg : g ~ g')
  where

  coherence-htpy-parallel-cone :
    {l4 : Level} {C : UU l4} (c : cone f g C) (c' : cone f' g' C)
    (Hp : vertical-map-cone f g c ~ vertical-map-cone f' g' c')
    (Hq : horizontal-map-cone f g c ~ horizontal-map-cone f' g' c') →
    UU (l3 ⊔ l4)
  coherence-htpy-parallel-cone c c' Hp Hq =
    ( ( coherence-square-cone f g c) ∙h
      ( (g ·l Hq) ∙h (Hg ·r horizontal-map-cone f' g' c'))) ~
    ( ( (f ·l Hp) ∙h (Hf ·r (vertical-map-cone f' g' c'))) ∙h
      ( coherence-square-cone f' g' c'))

  fam-htpy-parallel-cone :
    {l4 : Level} {C : UU l4} (c : cone f g C) → (c' : cone f' g' C) →
    (vertical-map-cone f g c ~ vertical-map-cone f' g' c') → UU (l2 ⊔ l3 ⊔ l4)
  fam-htpy-parallel-cone c c' Hp =
    Σ ( horizontal-map-cone f g c ~ horizontal-map-cone f' g' c')
      ( coherence-htpy-parallel-cone c c' Hp)

  htpy-parallel-cone :
    {l4 : Level} {C : UU l4} →
    cone f g C → cone f' g' C → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
  htpy-parallel-cone c c' =
    Σ ( vertical-map-cone f g c ~ vertical-map-cone f' g' c')
      ( fam-htpy-parallel-cone c c')

The identity cone over the identity cospan

id-cone : {l : Level} (A : UU l) → cone (id {A = A}) (id {A = A}) A
id-cone A = (id , id , refl-htpy)

Properties

Relating htpy-parallel-cone to the identity type of cones

In the following part we relate the type htpy-parallel-cone to the identity type of cones. We show that htpy-parallel-cone characterizes dependent identifications of cones on the same domain over parallel cospans.

Note. The characterization relies heavily on function extensionality.

The type family of homotopies of parallel cones is torsorial

module _
  {l1 l2 l3 l4 : Level}
  {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
  {f : A → X} {g : B → X}
  where

  refl-htpy-parallel-cone :
    (c : cone f g C) →
    htpy-parallel-cone (refl-htpy' f) (refl-htpy' g) c c
  pr1 (refl-htpy-parallel-cone c) = refl-htpy
  pr1 (pr2 (refl-htpy-parallel-cone c)) = refl-htpy
  pr2 (pr2 (refl-htpy-parallel-cone c)) = right-unit-htpy

  htpy-eq-degenerate-parallel-cone :
    (c c' : cone f g C) →
    c ＝ c' →
    htpy-parallel-cone (refl-htpy' f) (refl-htpy' g) c c'
  htpy-eq-degenerate-parallel-cone c .c refl = refl-htpy-parallel-cone c

  htpy-parallel-cone-refl-htpy-htpy-cone :
    (c c' : cone f g C) →
    htpy-cone f g c c' →
    htpy-parallel-cone (refl-htpy' f) (refl-htpy' g) c c'
  htpy-parallel-cone-refl-htpy-htpy-cone (p , q , H) (p' , q' , H') =
    tot
      ( λ K →
        tot
          ( λ L M →
            ( ap-concat-htpy H right-unit-htpy) ∙h
            ( M ∙h ap-concat-htpy' H' inv-htpy-right-unit-htpy)))

  abstract
    is-equiv-htpy-parallel-cone-refl-htpy-htpy-cone :
      (c c' : cone f g C) →
      is-equiv (htpy-parallel-cone-refl-htpy-htpy-cone c c')
    is-equiv-htpy-parallel-cone-refl-htpy-htpy-cone (p , q , H) (p' , q' , H') =
      is-equiv-tot-is-fiberwise-equiv
        ( λ K →
          is-equiv-tot-is-fiberwise-equiv
            ( λ L →
              is-equiv-comp
                ( concat-htpy
                  ( ap-concat-htpy H right-unit-htpy)
                  ( (f ·l K) ∙h refl-htpy ∙h H'))
                ( concat-htpy'
                  ( H ∙h (g ·l L))
                  ( ap-concat-htpy' H' inv-htpy-right-unit-htpy))
                ( is-equiv-concat-htpy'
                  ( H ∙h (g ·l L))
                  ( λ x → right-whisker-concat (inv right-unit) (H' x)))
                ( is-equiv-concat-htpy
                  ( λ x → left-whisker-concat (H x) right-unit)
                  ( (f ·l K) ∙h refl-htpy ∙h H'))))

  abstract
    is-torsorial-htpy-parallel-cone-refl-htpy-refl-htpy :
      (c : cone f g C) →
      is-torsorial (htpy-parallel-cone (refl-htpy' f) (refl-htpy' g) c)
    is-torsorial-htpy-parallel-cone-refl-htpy-refl-htpy c =
      is-contr-is-equiv'
        ( Σ (cone f g C) (htpy-cone f g c))
        ( tot (htpy-parallel-cone-refl-htpy-htpy-cone c))
        ( is-equiv-tot-is-fiberwise-equiv
          ( is-equiv-htpy-parallel-cone-refl-htpy-htpy-cone c))
        ( is-torsorial-htpy-cone f g c)

  abstract
    is-torsorial-htpy-parallel-cone-refl-htpy :
      {g' : B → X} (Hg : g ~ g') (c : cone f g C) →
      is-torsorial (htpy-parallel-cone (refl-htpy' f) Hg c)
    is-torsorial-htpy-parallel-cone-refl-htpy =
      ind-htpy
        ( g)
        ( λ g'' Hg' →
          (c : cone f g C) →
          is-torsorial (htpy-parallel-cone (refl-htpy' f) Hg' c))
        ( is-torsorial-htpy-parallel-cone-refl-htpy-refl-htpy)

  abstract
    is-torsorial-htpy-parallel-cone :
      {f' : A → X} (Hf : f ~ f') {g' : B → X} (Hg : g ~ g') (c : cone f g C) →
      is-torsorial (htpy-parallel-cone Hf Hg c)
    is-torsorial-htpy-parallel-cone Hf {g'} =
      ind-htpy
        ( f)
        ( λ f'' Hf' →
          (g' : B → X) (Hg : g ~ g') (c : cone f g C) →
          is-contr (Σ (cone f'' g' C) (htpy-parallel-cone Hf' Hg c)))
        ( λ g' Hg → is-torsorial-htpy-parallel-cone-refl-htpy Hg)
        ( Hf)
        ( g')

The type family of homotopies of parallel cones characterizes dependent identifications of cones on the same domain over parallel cospans

module _
  {l1 l2 l3 l4 : Level}
  {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
  {f : A → X} {g : B → X}
  where

  tr-right-tr-left-cone-eq-htpy :
    {f' : A → X} → f ~ f' → {g' : B → X} → g ~ g' → cone f g C → cone f' g' C
  tr-right-tr-left-cone-eq-htpy {f'} Hf Hg c =
    tr
      ( λ y → cone f' y C)
      ( eq-htpy Hg)
      ( tr (λ x → cone x g C) (eq-htpy Hf) c)

  compute-tr-right-tr-left-cone-eq-htpy-refl-htpy :
    (c : cone f g C) →
    tr-right-tr-left-cone-eq-htpy refl-htpy refl-htpy c ＝ c
  compute-tr-right-tr-left-cone-eq-htpy-refl-htpy c =
    ( ap
      ( λ t →
        tr
          ( λ g'' → cone f g'' C)
          ( t)
          ( tr (λ x → cone x g C) (eq-htpy (refl-htpy' f)) c))
      ( eq-htpy-refl-htpy g)) ∙
    ( ap (λ t → tr (λ f''' → cone f''' g C) t c) (eq-htpy-refl-htpy f))

  htpy-eq-parallel-cone-refl-htpy :
    (c c' : cone f g C) →
    tr-right-tr-left-cone-eq-htpy refl-htpy refl-htpy c ＝ c' →
    htpy-parallel-cone (refl-htpy' f) (refl-htpy' g) c c'
  htpy-eq-parallel-cone-refl-htpy c c' =
    map-inv-is-equiv-precomp-Π-is-equiv
      ( is-equiv-concat (compute-tr-right-tr-left-cone-eq-htpy-refl-htpy c) c')
      ( λ p → htpy-parallel-cone (refl-htpy' f) (refl-htpy' g) c c')
      ( htpy-eq-degenerate-parallel-cone c c')

  left-map-triangle-eq-parallel-cone-refl-htpy :
    (c c' : cone f g C) →
    ( ( htpy-eq-parallel-cone-refl-htpy c c') ∘
      ( concat (compute-tr-right-tr-left-cone-eq-htpy-refl-htpy c) c')) ~
    ( htpy-eq-degenerate-parallel-cone c c')
  left-map-triangle-eq-parallel-cone-refl-htpy c c' =
    is-section-map-inv-is-equiv-precomp-Π-is-equiv
      ( is-equiv-concat (compute-tr-right-tr-left-cone-eq-htpy-refl-htpy c) c')
      ( λ p → htpy-parallel-cone (refl-htpy' f) (refl-htpy' g) c c')
      ( htpy-eq-degenerate-parallel-cone c c')

  abstract
    htpy-parallel-cone-dependent-eq' :
      {g' : B → X} (Hg : g ~ g') →
      (c : cone f g C) (c' : cone f g' C) →
      tr-right-tr-left-cone-eq-htpy refl-htpy Hg c ＝ c' →
      htpy-parallel-cone (refl-htpy' f) Hg c c'
    htpy-parallel-cone-dependent-eq' =
      ind-htpy g
        ( λ g'' Hg' →
          ( c : cone f g C) (c' : cone f g'' C) →
          tr-right-tr-left-cone-eq-htpy refl-htpy Hg' c ＝ c' →
          htpy-parallel-cone refl-htpy Hg' c c')
        ( htpy-eq-parallel-cone-refl-htpy)

    left-map-triangle-parallel-cone-eq' :
      (c c' : cone f g C) →
      ( ( htpy-parallel-cone-dependent-eq' refl-htpy c c') ∘
        ( concat (compute-tr-right-tr-left-cone-eq-htpy-refl-htpy c) c')) ~
      ( htpy-eq-degenerate-parallel-cone c c')
    left-map-triangle-parallel-cone-eq' c c' =
      ( right-whisker-comp
        ( multivariable-htpy-eq 3
          ( compute-ind-htpy g
            ( λ g'' Hg' →
              ( c : cone f g C) (c' : cone f g'' C) →
              tr-right-tr-left-cone-eq-htpy refl-htpy Hg' c ＝ c' →
              htpy-parallel-cone refl-htpy Hg' c c')
            ( htpy-eq-parallel-cone-refl-htpy))
          ( c)
          ( c'))
        ( concat (compute-tr-right-tr-left-cone-eq-htpy-refl-htpy c) c')) ∙h
      ( left-map-triangle-eq-parallel-cone-refl-htpy c c')

  abstract
    htpy-parallel-cone-dependent-eq :
      {f' : A → X} (Hf : f ~ f') {g' : B → X} (Hg : g ~ g') →
      (c : cone f g C) (c' : cone f' g' C) →
      tr-right-tr-left-cone-eq-htpy Hf Hg c ＝ c' →
      htpy-parallel-cone Hf Hg c c'
    htpy-parallel-cone-dependent-eq {f'} Hf {g'} Hg c c' p =
      ind-htpy f
        ( λ f'' Hf' →
          ( g' : B → X) (Hg : g ~ g') (c : cone f g C) (c' : cone f'' g' C) →
          ( tr-right-tr-left-cone-eq-htpy Hf' Hg c ＝ c') →
          htpy-parallel-cone Hf' Hg c c')
        ( λ g' → htpy-parallel-cone-dependent-eq' {g' = g'})
        Hf g' Hg c c' p

    left-map-triangle-parallel-cone-eq :
      (c c' : cone f g C) →
      ( ( htpy-parallel-cone-dependent-eq refl-htpy refl-htpy c c') ∘
        ( concat (compute-tr-right-tr-left-cone-eq-htpy-refl-htpy c) c')) ~
      ( htpy-eq-degenerate-parallel-cone c c')
    left-map-triangle-parallel-cone-eq c c' =
      ( right-whisker-comp
        ( multivariable-htpy-eq 5
          ( compute-ind-htpy f
            ( λ f'' Hf' →
              ( g' : B → X) (Hg : g ~ g')
              (c : cone f g C) (c' : cone f'' g' C) →
              ( tr-right-tr-left-cone-eq-htpy Hf' Hg c ＝ c') →
              htpy-parallel-cone Hf' Hg c c')
            ( λ g' → htpy-parallel-cone-dependent-eq' {g' = g'}))
          ( g)
          ( refl-htpy)
          ( c)
          ( c'))
        ( concat (compute-tr-right-tr-left-cone-eq-htpy-refl-htpy c) c')) ∙h
      ( left-map-triangle-parallel-cone-eq' c c')

  abstract
    is-fiberwise-equiv-htpy-parallel-cone-dependent-eq :
      {f' : A → X} (Hf : f ~ f') {g' : B → X} (Hg : g ~ g') →
      (c : cone f g C) (c' : cone f' g' C) →
      is-equiv (htpy-parallel-cone-dependent-eq Hf Hg c c')
    is-fiberwise-equiv-htpy-parallel-cone-dependent-eq {f'} Hf {g'} Hg c c' =
      ind-htpy f
        ( λ f' Hf →
          ( g' : B → X) (Hg : g ~ g') (c : cone f g C) (c' : cone f' g' C) →
            is-equiv (htpy-parallel-cone-dependent-eq Hf Hg c c'))
        ( λ g' Hg c c' →
          ind-htpy g
            ( λ g' Hg →
              ( c : cone f g C) (c' : cone f g' C) →
                is-equiv (htpy-parallel-cone-dependent-eq refl-htpy Hg c c'))
            ( λ c c' →
              is-equiv-right-map-triangle
                ( htpy-eq-degenerate-parallel-cone c c')
                ( htpy-parallel-cone-dependent-eq refl-htpy refl-htpy c c')
                ( concat (compute-tr-right-tr-left-cone-eq-htpy-refl-htpy c) c')
                ( inv-htpy (left-map-triangle-parallel-cone-eq c c'))
                ( fundamental-theorem-id
                  ( is-torsorial-htpy-parallel-cone
                    ( refl-htpy' f)
                    ( refl-htpy' g)
                    ( c))
                  ( htpy-eq-degenerate-parallel-cone c) c')
                ( is-equiv-concat
                  ( compute-tr-right-tr-left-cone-eq-htpy-refl-htpy c)
                  ( c')))
            ( Hg)
            ( c)
            ( c'))
        ( Hf)
        ( g')
        ( Hg)
        ( c)
        ( c')

  dependent-eq-htpy-parallel-cone :
    {f' : A → X} (Hf : f ~ f') {g' : B → X} (Hg : g ~ g') →
    (c : cone f g C) (c' : cone f' g' C) →
    htpy-parallel-cone Hf Hg c c' →
    tr-right-tr-left-cone-eq-htpy Hf Hg c ＝ c'
  dependent-eq-htpy-parallel-cone Hf Hg c c' =
    map-inv-is-equiv
      ( is-fiberwise-equiv-htpy-parallel-cone-dependent-eq Hf Hg c c')

Table of files about pullbacks

The following table lists files that are about pullbacks as a general concept.

ConceptFile
Cospan diagramsfoundation.cospans
Morphisms of cospan diagramsfoundation.morphisms-cospans
Cones over cospan diagramsfoundation.cones-over-cospan-diagrams
The universal property of pullbacks (foundation-core)foundation-core.universal-property-pullbacks
The universal property of pullbacks (foundation)foundation.universal-property-pullbacks
The universal property of fiber productsfoundation.universal-property-fiber-products
Standard pullbacksfoundation.standard-pullbacks
Pullbacks (foundation-core)foundation-core.pullbacks
Pullbacks (foundation)foundation.pullbacks
Pullback conesfoundation.pullback-cones
Functoriality of pullbacksfoundation.functoriality-pullbacks
Cartesian morphisms of arrowsfoundation.cartesian-morphisms-arrows
Dependent products of pullbacksfoundation.dependent-products-pullbacks
Dependent sums of pullbacksfoundation.dependent-sums-pullbacks
Products of pullbacksfoundation.products-pullbacks
Coroducts of pullbacksfoundation.coproducts-pullbacks
Postcomposition of pullbacksfoundation.postcomposition-pullbacks
Pullbacks of subtypesfoundation.pullbacks-subtypes
The pullback-homorthogonal-factorization-systems.pullback-hom
Functoriality of the pullback-homorthogonal-factorization-systems.functoriality-pullback-hom
Pullbacks in precategoriescategory-theory.pullbacks-in-precategories

Recent changes