Dependent coforks
Content created by Egbert Rijke, Vojtěch Štěpančík and Fredrik Bakke.
Created on 2023-09-20.
Last modified on 2023-11-24.
module synthetic-homotopy-theory.dependent-coforks where
Imports
open import foundation.action-on-identifications-dependent-functions open import foundation.action-on-identifications-functions open import foundation.commuting-triangles-of-maps open import foundation.constant-type-families open import foundation.coproduct-types open import foundation.dependent-identifications open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.function-types open import foundation.functoriality-dependent-function-types open import foundation.functoriality-dependent-pair-types 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.structure-identity-principle open import foundation.torsorial-type-families open import foundation.transport-along-identifications open import foundation.universe-levels open import synthetic-homotopy-theory.coforks open import synthetic-homotopy-theory.dependent-cocones-under-spans
Idea
Given a parallel pair f, g : A → B
, a
cofork e : B → X
with vertex X
, and
a type family P : X → 𝓤
over X
, we may construct dependent coforks on P
over e
.
A dependent cofork on P
over e
consists of a dependent map
k : (b : B) → P (e b)
and a family of
dependent identifications indexed by
A
(a : A) → dependent-identification P (H a) (k (f a)) (k (g a)).
Dependent coforks are an analogue of dependent cocones under spans for parallel pairs.
Definitions
Dependent coforks
module _ { l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} (f g : A → B) {X : UU l3} ( e : cofork f g X) (P : X → UU l4) where dependent-cofork : UU (l1 ⊔ l2 ⊔ l4) dependent-cofork = Σ ( (b : B) → P (map-cofork f g e b)) ( λ k → ( a : A) → dependent-identification P ( coherence-cofork f g e a) ( k (f a)) ( k (g a))) module _ { l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} (f g : A → B) {X : UU l3} { e : cofork f g X} (P : X → UU l4) ( k : dependent-cofork f g e P) where map-dependent-cofork : (b : B) → P (map-cofork f g e b) map-dependent-cofork = pr1 k coherence-dependent-cofork : ( a : A) → dependent-identification P ( coherence-cofork f g e a) ( map-dependent-cofork (f a)) ( map-dependent-cofork (g a)) coherence-dependent-cofork = pr2 k
Homotopies of dependent coforks
A homotopy between dependent coforks is a homotopy between the underlying maps, together with a coherence condition.
module _ { l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} (f g : A → B) {X : UU l3} { e : cofork f g X} (P : X → UU l4) where coherence-htpy-dependent-cofork : ( k k' : dependent-cofork f g e P) → ( K : map-dependent-cofork f g P k ~ map-dependent-cofork f g P k') → UU (l1 ⊔ l4) coherence-htpy-dependent-cofork k k' K = ( a : A) → ( ( coherence-dependent-cofork f g P k a) ∙ (K (g a))) = ( ( ap (tr P (coherence-cofork f g e a)) (K (f a))) ∙ ( coherence-dependent-cofork f g P k' a)) htpy-dependent-cofork : ( k k' : dependent-cofork f g e P) → UU (l1 ⊔ l2 ⊔ l4) htpy-dependent-cofork k k' = Σ ( map-dependent-cofork f g P k ~ map-dependent-cofork f g P k') ( coherence-htpy-dependent-cofork k k')
Obtaining dependent coforks as postcomposition of coforks with dependent maps
One way to obtains dependent coforks is to postcompose the underlying cofork by a dependent map, according to the diagram
g
-----> e h
A -----> B -----> (x : X) -----> (P x)
f
module _ { l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f g : A → B) {X : UU l3} ( e : cofork f g X) where dependent-cofork-map : { l : Level} {P : X → UU l} → ((x : X) → P x) → dependent-cofork f g e P pr1 (dependent-cofork-map h) = h ∘ map-cofork f g e pr2 (dependent-cofork-map h) = apd h ∘ coherence-cofork f g e
Properties
Characterization of identity types of coforks
module _ { l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} (f g : A → B) {X : UU l3} { e : cofork f g X} (P : X → UU l4) where reflexive-htpy-dependent-cofork : ( k : dependent-cofork f g e P) → htpy-dependent-cofork f g P k k pr1 (reflexive-htpy-dependent-cofork k) = refl-htpy pr2 (reflexive-htpy-dependent-cofork k) = right-unit-htpy htpy-dependent-cofork-eq : ( k k' : dependent-cofork f g e P) → ( k = k') → htpy-dependent-cofork f g P k k' htpy-dependent-cofork-eq k .k refl = reflexive-htpy-dependent-cofork k abstract is-torsorial-htpy-dependent-cofork : ( k : dependent-cofork f g e P) → is-torsorial (htpy-dependent-cofork f g P k) is-torsorial-htpy-dependent-cofork k = is-torsorial-Eq-structure ( ev-pair (coherence-htpy-dependent-cofork f g P k)) ( is-torsorial-htpy (map-dependent-cofork f g P k)) ( map-dependent-cofork f g P k , refl-htpy) ( is-torsorial-htpy ( coherence-dependent-cofork f g P k ∙h refl-htpy)) is-equiv-htpy-dependent-cofork-eq : ( k k' : dependent-cofork f g e P) → is-equiv (htpy-dependent-cofork-eq k k') is-equiv-htpy-dependent-cofork-eq k = fundamental-theorem-id ( is-torsorial-htpy-dependent-cofork k) ( htpy-dependent-cofork-eq k) eq-htpy-dependent-cofork : ( k k' : dependent-cofork f g e P) → htpy-dependent-cofork f g P k k' → k = k' eq-htpy-dependent-cofork k k' = map-inv-is-equiv (is-equiv-htpy-dependent-cofork-eq k k')
Dependent coforks on constant type families are equivalent to regular coforks
module _ { l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} (f g : A → B) {X : UU l3} ( e : cofork f g X) (Y : UU l4) where compute-dependent-cofork-constant-family : dependent-cofork f g e (λ _ → Y) ≃ cofork f g Y compute-dependent-cofork-constant-family = equiv-tot ( λ h → equiv-Π-equiv-family ( λ a → equiv-concat ( inv ( tr-constant-type-family (coherence-cofork f g e a) (h (f a)))) ( h (g a)))) map-compute-dependent-cofork-constant-family : dependent-cofork f g e (λ _ → Y) → cofork f g Y map-compute-dependent-cofork-constant-family = map-equiv compute-dependent-cofork-constant-family triangle-compute-dependent-cofork-constant-family : coherence-triangle-maps ( cofork-map f g e) ( map-compute-dependent-cofork-constant-family) ( dependent-cofork-map f g e) triangle-compute-dependent-cofork-constant-family h = eq-htpy-cofork f g ( cofork-map f g e h) ( map-compute-dependent-cofork-constant-family ( dependent-cofork-map f g e h)) ( ( refl-htpy) , ( right-unit-htpy ∙h ( λ a → left-transpose-eq-concat _ _ _ ( inv (apd-constant-type-family h (coherence-cofork f g e a))))))
Dependent coforks are special cases of dependent cocones under spans
The type of dependent coforks on P
over e
is equivalent to the type of
dependent cocones
on P
over a cocone corresponding to e
via cocone-codiagonal-cofork
.
module _ { l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f g : A → B) {X : UU l3} ( e : cofork f g X) where module _ { l4 : Level} (P : X → UU l4) where dependent-cofork-dependent-cocone-codiagonal : dependent-cocone ( vertical-map-span-cocone-cofork f g) ( horizontal-map-span-cocone-cofork f g) ( cocone-codiagonal-cofork f g e) ( P) → dependent-cofork f g e P pr1 (dependent-cofork-dependent-cocone-codiagonal k) = vertical-map-dependent-cocone ( vertical-map-span-cocone-cofork f g) ( horizontal-map-span-cocone-cofork f g) ( cocone-codiagonal-cofork f g e) ( P) ( k) pr2 (dependent-cofork-dependent-cocone-codiagonal k) a = inv ( ap ( tr P (coherence-cofork f g e a)) ( coherence-square-dependent-cocone ( vertical-map-span-cocone-cofork f g) ( horizontal-map-span-cocone-cofork f g) ( cocone-codiagonal-cofork f g e) ( P) ( k) ( inl a))) ∙ coherence-square-dependent-cocone ( vertical-map-span-cocone-cofork f g) ( horizontal-map-span-cocone-cofork f g) ( cocone-codiagonal-cofork f g e) ( P) ( k) ( inr a) dependent-cocone-codiagonal-dependent-cofork : dependent-cofork f g e P → dependent-cocone ( vertical-map-span-cocone-cofork f g) ( horizontal-map-span-cocone-cofork f g) ( cocone-codiagonal-cofork f g e) ( P) pr1 (dependent-cocone-codiagonal-dependent-cofork k) = map-dependent-cofork f g P k ∘ f pr1 (pr2 (dependent-cocone-codiagonal-dependent-cofork k)) = map-dependent-cofork f g P k pr2 (pr2 (dependent-cocone-codiagonal-dependent-cofork k)) (inl a) = refl pr2 (pr2 (dependent-cocone-codiagonal-dependent-cofork k)) (inr a) = coherence-dependent-cofork f g P k a abstract is-section-dependent-cocone-codiagonal-dependent-cofork : ( ( dependent-cofork-dependent-cocone-codiagonal) ∘ ( dependent-cocone-codiagonal-dependent-cofork)) ~ ( id) is-section-dependent-cocone-codiagonal-dependent-cofork k = eq-htpy-dependent-cofork f g P ( dependent-cofork-dependent-cocone-codiagonal ( dependent-cocone-codiagonal-dependent-cofork k)) ( k) ( refl-htpy , right-unit-htpy) is-retraction-dependent-cocone-codiagonal-dependent-cofork : ( ( dependent-cocone-codiagonal-dependent-cofork) ∘ ( dependent-cofork-dependent-cocone-codiagonal)) ~ ( id) is-retraction-dependent-cocone-codiagonal-dependent-cofork d = eq-htpy-dependent-cocone ( vertical-map-span-cocone-cofork f g) ( horizontal-map-span-cocone-cofork f g) ( cocone-codiagonal-cofork f g e) ( P) ( dependent-cocone-codiagonal-dependent-cofork ( dependent-cofork-dependent-cocone-codiagonal d)) ( d) ( inv-htpy ( ( coherence-square-dependent-cocone ( vertical-map-span-cocone-cofork f g) ( horizontal-map-span-cocone-cofork f g) ( cocone-codiagonal-cofork f g e) ( P) ( d)) ∘ ( inl)) , ( refl-htpy) , ( right-unit-htpy ∙h ( λ where ( inl a) → inv ( ( ap ( _∙ coherence-square-dependent-cocone ( vertical-map-span-cocone-cofork f g) ( horizontal-map-span-cocone-cofork f g) ( cocone-codiagonal-cofork f g e) ( P) ( d) ( inl a)) ( ap-id ( inv ( coherence-square-dependent-cocone ( vertical-map-span-cocone-cofork f g) ( horizontal-map-span-cocone-cofork f g) ( cocone-codiagonal-cofork f g e) ( P) ( d) ( inl a))))) ∙ ( left-inv ( coherence-square-dependent-cocone ( vertical-map-span-cocone-cofork f g) ( horizontal-map-span-cocone-cofork f g) ( cocone-codiagonal-cofork f g e) ( P) ( d) ( inl a)))) ( inr a) → ap ( _∙ coherence-square-dependent-cocone ( vertical-map-span-cocone-cofork f g) ( horizontal-map-span-cocone-cofork f g) ( cocone-codiagonal-cofork f g e) ( P) ( d) ( inr a)) ( inv ( ap-inv ( tr P (coherence-cofork f g e a)) ( coherence-square-dependent-cocone ( vertical-map-span-cocone-cofork f g) ( horizontal-map-span-cocone-cofork f g) ( cocone-codiagonal-cofork f g e) ( P) ( d) ( inl a))))))) is-equiv-dependent-cofork-dependent-cocone-codiagonal : is-equiv dependent-cofork-dependent-cocone-codiagonal is-equiv-dependent-cofork-dependent-cocone-codiagonal = is-equiv-is-invertible ( dependent-cocone-codiagonal-dependent-cofork) ( is-section-dependent-cocone-codiagonal-dependent-cofork) ( is-retraction-dependent-cocone-codiagonal-dependent-cofork) equiv-dependent-cofork-dependent-cocone-codiagonal : dependent-cocone ( vertical-map-span-cocone-cofork f g) ( horizontal-map-span-cocone-cofork f g) ( cocone-codiagonal-cofork f g e) ( P) ≃ dependent-cofork f g e P pr1 equiv-dependent-cofork-dependent-cocone-codiagonal = dependent-cofork-dependent-cocone-codiagonal pr2 equiv-dependent-cofork-dependent-cocone-codiagonal = is-equiv-dependent-cofork-dependent-cocone-codiagonal triangle-dependent-cofork-dependent-cocone-codiagonal : { l4 : Level} (P : X → UU l4) → coherence-triangle-maps ( dependent-cofork-map f g e) ( dependent-cofork-dependent-cocone-codiagonal P) ( dependent-cocone-map ( vertical-map-span-cocone-cofork f g) ( horizontal-map-span-cocone-cofork f g) ( cocone-codiagonal-cofork f g e) ( P)) triangle-dependent-cofork-dependent-cocone-codiagonal P h = eq-htpy-dependent-cofork f g P ( dependent-cofork-map f g e h) ( dependent-cofork-dependent-cocone-codiagonal P ( dependent-cocone-map ( vertical-map-span-cocone-cofork f g) ( horizontal-map-span-cocone-cofork f g) ( cocone-codiagonal-cofork f g e) ( P) ( h))) ( refl-htpy , right-unit-htpy)
Recent changes
- 2023-11-24. Egbert Rijke. Refactor precomposition (#937).
- 2023-10-23. Vojtěch Štěpančík. Sequential colimits (#841).
- 2023-10-21. Egbert Rijke and Fredrik Bakke. Implement
is-torsorial
throughout the library (#875). - 2023-10-21. Egbert Rijke. Rename
is-contr-total
tois-torsorial
(#871). - 2023-10-12. Vojtěch Štěpančík. Derive the flattening lemma for coequalizers from the flattening lemma for pushouts (#831).