# Right extensions in precategories ```agda module category-theory.right-extensions-precategories where ``` <details><summary>Imports</summary> ```agda open import category-theory.functors-precategories open import category-theory.natural-transformations-functors-precategories open import category-theory.precategories open import foundation.action-on-equivalences-functions open import foundation.action-on-identifications-functions open import foundation.contractible-types open import foundation.dependent-identifications open import foundation.dependent-pair-types open import foundation.equality-dependent-function-types open import foundation.equality-dependent-pair-types open import foundation.equivalences open import foundation.function-extensionality open import foundation.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.multivariable-homotopies open import foundation.propositions open import foundation.retractions open import foundation.sections open import foundation.sets open import foundation.structure-identity-principle open import foundation.torsorial-type-families open import foundation.unit-type open import foundation.universe-levels open import foundation-core.functoriality-dependent-function-types ``` </details> ## Idea A {{#concept "right extension" Disambiguation="of a functor between precategories" Agda=right-extension-Precategory}} of a [functor](category-theory.functors-precategories.md) `F : C → D` between [precategories](category-theory.precategories.md) along another functor `p : C → C'` is a functor `G : C' → D` together with a [natural transformation](category-theory.natural-transformations-functors-precategories.md) `φ : G ∘ p → F`. ```text C | \ p F | \ ∨ ∨ C' - G -> D ``` We note that this is not a standard definition, but it inspired by the notion of a [right kan extension](category-theory.right-kan-extensions-precategories.md). ## Definition ### Right extensions ```agda module _ {l1 l2 l3 l4 l5 l6 : Level} (C : Precategory l1 l2) (C' : Precategory l3 l4) (D : Precategory l5 l6) (p : functor-Precategory C C') (F : functor-Precategory C D) where right-extension-Precategory : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6) right-extension-Precategory = Σ ( functor-Precategory C' D) ( λ G → natural-transformation-Precategory C D ( comp-functor-Precategory C C' D G p) ( F)) module _ (R : right-extension-Precategory) where extension-right-extension-Precategory : functor-Precategory C' D extension-right-extension-Precategory = pr1 R natural-transformation-right-extension-Precategory : natural-transformation-Precategory C D ( comp-functor-Precategory C C' D ( extension-right-extension-Precategory) ( p)) ( F) natural-transformation-right-extension-Precategory = pr2 R hom-family-right-extension-Precategory : hom-family-functor-Precategory C D ( comp-functor-Precategory C C' D ( extension-right-extension-Precategory) ( p)) ( F) hom-family-right-extension-Precategory = hom-family-natural-transformation-Precategory C D ( comp-functor-Precategory C C' D ( extension-right-extension-Precategory) ( p)) ( F) ( natural-transformation-right-extension-Precategory) naturality-right-extension-Precategory : is-natural-transformation-Precategory C D ( comp-functor-Precategory C C' D ( extension-right-extension-Precategory) ( p)) ( F) ( hom-family-right-extension-Precategory) naturality-right-extension-Precategory = naturality-natural-transformation-Precategory C D ( comp-functor-Precategory C C' D ( extension-right-extension-Precategory) ( p)) ( F) ( natural-transformation-right-extension-Precategory) ``` ### Precomposing right extensions ```agda right-extension-map-Precategory : ( G : functor-Precategory C' D) → ( natural-transformation-Precategory C' D G extension-right-extension-Precategory) → ( natural-transformation-Precategory C D ( comp-functor-Precategory C C' D G p) F) right-extension-map-Precategory G φ = comp-natural-transformation-Precategory C D ( comp-functor-Precategory C C' D G p) ( comp-functor-Precategory C C' D extension-right-extension-Precategory p) ( F) ( natural-transformation-right-extension-Precategory) ( right-whisker-natural-transformation-Precategory C' D C ( G) ( extension-right-extension-Precategory) ( φ) ( p)) ``` ## Properties ### Characterization of equality right extensions of functors between precategories ```agda coherence-htpy-right-extension-Precategory : (R S : right-extension-Precategory) (e : (extension-right-extension-Precategory R) = (extension-right-extension-Precategory S)) → UU (l1 ⊔ l6) coherence-htpy-right-extension-Precategory R S e = (x : obj-Precategory C) → comp-hom-Precategory D ( hom-family-right-extension-Precategory S x) ( hom-family-natural-transformation-Precategory C' D (pr1 R) (pr1 S) ( natural-transformation-eq-Precategory C' D ( extension-right-extension-Precategory R) ( extension-right-extension-Precategory S) ( e)) ( obj-functor-Precategory C C' p x)) = hom-family-right-extension-Precategory R x htpy-right-extension-Precategory : (R S : right-extension-Precategory) → UU (l1 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6) htpy-right-extension-Precategory R S = Σ ( extension-right-extension-Precategory R = extension-right-extension-Precategory S) ( coherence-htpy-right-extension-Precategory R S) is-torsorial-htpy-right-extension-Precategory : (R : right-extension-Precategory) → is-torsorial (htpy-right-extension-Precategory R) is-torsorial-htpy-right-extension-Precategory R = is-torsorial-Eq-structure ( is-torsorial-Id (extension-right-extension-Precategory R)) ( pair (extension-right-extension-Precategory R) refl) ( is-contr-equiv ( Σ ( natural-transformation-Precategory C D ( comp-functor-Precategory C C' D ( extension-right-extension-Precategory R) p) ( F)) ( λ τ → τ = natural-transformation-right-extension-Precategory R)) ( equiv-tot ( λ τ → inv-equiv ( extensionality-natural-transformation-Precategory C D ( comp-functor-Precategory C C' D ( extension-right-extension-Precategory R) p) ( F) _ _) ∘e equiv-Π-equiv-family ( λ x → equiv-inv-concat ( right-unit-law-comp-hom-Precategory D _) ( hom-family-right-extension-Precategory R x)))) ( is-torsorial-Id' ( natural-transformation-right-extension-Precategory R))) refl-htpy-right-extension-Precategory : (R : right-extension-Precategory) → htpy-right-extension-Precategory R R pr1 (refl-htpy-right-extension-Precategory R) = refl pr2 (refl-htpy-right-extension-Precategory R) x = right-unit-law-comp-hom-Precategory D _ htpy-eq-right-extension-Precategory : (R S : right-extension-Precategory) → R = S → htpy-right-extension-Precategory R S htpy-eq-right-extension-Precategory R .R refl = refl-htpy-right-extension-Precategory R is-equiv-htpy-eq-right-extension-Precategory : (R S : right-extension-Precategory) → is-equiv (htpy-eq-right-extension-Precategory R S) is-equiv-htpy-eq-right-extension-Precategory R = fundamental-theorem-id ( is-torsorial-htpy-right-extension-Precategory R) ( htpy-eq-right-extension-Precategory R) equiv-htpy-eq-right-extension-Precategory : (R S : right-extension-Precategory) → (R = S) ≃ htpy-right-extension-Precategory R S pr1 (equiv-htpy-eq-right-extension-Precategory R S) = htpy-eq-right-extension-Precategory R S pr2 (equiv-htpy-eq-right-extension-Precategory R S) = is-equiv-htpy-eq-right-extension-Precategory R S eq-htpy-right-extension-Precategory : (R S : right-extension-Precategory) → htpy-right-extension-Precategory R S → R = S eq-htpy-right-extension-Precategory R S = map-inv-equiv (equiv-htpy-eq-right-extension-Precategory R S) ```