Natural isomorphisms between functors on large precategories

Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Elisabeth Bonnevier.

Created on 2022-03-11.
Last modified on 2023-09-19.

module category-theory.natural-isomorphisms-large-precategories where
open import category-theory.functors-large-precategories
open import category-theory.isomorphisms-in-large-precategories
open import category-theory.large-precategories
open import category-theory.natural-transformations-large-precategories

open import foundation.universe-levels


A natural isomorphism γ from functor F : C → D to G : C → D is a natural transformation from F to G such that the morphism γ x : hom (F x) (G x) is an isomorphism, for every object x in C.


module _
  {αC αD γF γG : Level  Level} {βC βD : Level  Level  Level}
  {C : Large-Precategory αC βC} {D : Large-Precategory αD βD}
  (F : functor-Large-Precategory C D γF)
  (G : functor-Large-Precategory C D γG)

  record natural-isomorphism-Large-Precategory : UUω
    constructor make-natural-isomorphism
      obj-natural-isomorphism-Large-Precategory :
        { l1 : Level} (X : obj-Large-Precategory C l1) 
        iso-Large-Precategory D
          ( obj-functor-Large-Precategory F X)
          ( obj-functor-Large-Precategory G X)
      coherence-square-natural-isomorphism-Large-Precategory :
        { l1 l2 : Level}
        { X : obj-Large-Precategory C l1}
        { Y : obj-Large-Precategory C l2}
        ( f : type-hom-Large-Precategory C X Y) 
        square-Large-Precategory D
          ( hom-iso-Large-Precategory D
            ( obj-natural-isomorphism-Large-Precategory X))
          ( hom-functor-Large-Precategory F f)
          ( hom-functor-Large-Precategory G f)
          ( hom-iso-Large-Precategory D
            ( obj-natural-isomorphism-Large-Precategory Y))

  open natural-isomorphism-Large-Precategory public

  natural-transformation-natural-isomorphism-Large-Precategory :
    natural-transformation-Large-Precategory F G
    ( natural-transformation-natural-isomorphism-Large-Precategory γ) X =
    hom-iso-Large-Precategory D
      ( obj-natural-isomorphism-Large-Precategory γ X)
    (natural-transformation-natural-isomorphism-Large-Precategory γ) =
      coherence-square-natural-isomorphism-Large-Precategory γ

Recent changes