module Cat.Functor.Naturality where

Working with natural transformations🔗

Working with natural transformations can often be more cumbersome than working directly with the underlying families of morphisms; moreover, we often have to convert between a property of natural transformations and a (universally quantified) property of the underlying morphisms. This module collects some notation that will help us with that task.

We’ll refer to the natural-transformation versions of predicates on morphisms by a superscript ⁿ. A natural isomorphism is simply an isomorphism in a functor category.

  Inversesⁿ : {F G : Functor C D} → F => G → G => F → Type _
  Inversesⁿ = CD.Inverses

  is-invertibleⁿ : {F G : Functor C D} → F => G → Type _
  is-invertibleⁿ = CD.is-invertible

  _≅ⁿ_ : Functor C D → Functor C D → Type _
  F ≅ⁿ G = CD.Isomorphism F G

A fundamental lemma that will let us work with natural isomorphisms more conveniently is the following: if is a natural transformation which is componentwise inverted by then is itself a natural transformation This means that, when constructing a natural isomorphism from scratch, we only have to establish naturality in one direction, rather than both.

  inverse-is-natural
    : ∀ {F G : Functor C D} (α : F => G) (β : ∀ x → D.Hom (G .F₀ x) (F .F₀ x) )
    → (∀ x → α .η x D.∘ β x ≡ D.id)
    → (∀ x → β x D.∘ α .η x ≡ D.id)
    → is-natural-transformation G F β
  inverse-is-natural {F = F} {G = G} α β invl invr x y f =
    β y D.∘ G .F₁ f                    ≡⟨ D.refl⟩∘⟨ D.intror (invl x) ⟩≡
    β y D.∘ G .F₁ f D.∘ α .η x D.∘ β x ≡⟨ D.refl⟩∘⟨ D.extendl (sym (α .is-natural x y f)) ⟩≡
    β y D.∘ α .η y D.∘ F .F₁ f D.∘ β x ≡⟨ D.cancell (invr y) ⟩≡
    F .F₁ f D.∘ β x ∎

We can then create a natural isomorphism from the following data:

  record make-natural-iso (F G : Functor C D) : Type (o ⊔ ℓ ⊔ ℓ') where
    no-eta-equality
    field
      eta : ∀ x → D.Hom (F .F₀ x) (G .F₀ x)
      inv : ∀ x → D.Hom (G .F₀ x) (F .F₀ x)
      eta∘inv : ∀ x → eta x D.∘ inv x ≡ D.id
      inv∘eta : ∀ x → inv x D.∘ eta x ≡ D.id
      natural : ∀ x y f → G .F₁ f D.∘ eta x ≡ eta y D.∘ F .F₁ f

  open make-natural-iso

  to-natural-iso : ∀ {F G} → make-natural-iso F G → F ≅ⁿ G
  to-natural-iso mk .Isoⁿ.to .η                = mk .eta
  to-natural-iso mk .Isoⁿ.to .is-natural x y f = sym (mk .natural x y f)
  to-natural-iso mk .Isoⁿ.from .η = mk .inv
  to-natural-iso {F = F} {G} mk .Isoⁿ.from .is-natural =
    inverse-is-natural {F} {G} (NT _ (λ x y f → sym (mk .natural x y f)))
      (mk .inv) (mk .eta∘inv) (mk .inv∘eta)
  to-natural-iso mk .Isoⁿ.inverses .Inversesⁿ.invl = ext (mk .eta∘inv)
  to-natural-iso mk .Isoⁿ.inverses .Inversesⁿ.invr = ext (mk .inv∘eta)

Moreover, the following family of functions project out the componentwise invertibility, resp. componentwise isomorphism, associated to an invertible natural transformation, resp. natural isomorphism.

  is-invertibleⁿ→is-invertible
    : ∀ {F G} {α : F => G}
    → is-invertibleⁿ α
    → ∀ x → D.is-invertible (α .η x)
  is-invertibleⁿ→is-invertible inv x =
    D.make-invertible
      (CD.is-invertible.inv inv .η x)
      (CD.is-invertible.invl inv ηₚ x)
      (CD.is-invertible.invr inv ηₚ x)

  isoⁿ→iso
    : ∀ {F G} → F ≅ⁿ G
    → ∀ x → F .F₀ x D.≅ G .F₀ x
  isoⁿ→iso α x =
    D.make-iso (α.to .η x) (α.from .η x) (α.invl ηₚ x) (α.invr ηₚ x)
    where module α = Isoⁿ α

  iso→isoⁿ
    : ∀ {F G}
    → (is : ∀ x → F .F₀ x D.≅ G .F₀ x)
    → (∀ {x y} f → G .F₁ f D.∘ is x .D.to ≡ is y .D.to D.∘ F .F₁ f)
    → F ≅ⁿ G
  iso→isoⁿ {F} {G} is nat = to-natural-iso mk where
    mk : make-natural-iso F G
    mk .eta x = is x .D.to
    mk .inv x = is x .D.from
    mk .eta∘inv x = is x .D.invl
    mk .inv∘eta x = is x .D.invr
    mk .natural _ _ = nat

  is-invertibleⁿ→isoⁿ : ∀ {F G} {α : F => G} → is-invertibleⁿ α → F ≅ⁿ G
  is-invertibleⁿ→isoⁿ nat-inv = CD.invertible→iso _ nat-inv

  isoⁿ→is-invertible
    : ∀ {F G} (α : F ≅ⁿ G)
    → ∀ x → D.is-invertible (α .Isoⁿ.to .η x)
  isoⁿ→is-invertible α x = D.iso→invertible (isoⁿ→iso α x)
  to-inversesⁿ
    : {F G : Functor C D} {α : F => G} {β : G => F}
    → (∀ x → α .η x D.∘ β .η x ≡ D.id)
    → (∀ x → β .η x D.∘ α .η x ≡ D.id)
    → Inversesⁿ α β
  to-inversesⁿ p q = CD.make-inverses (ext p) (ext q)

  to-is-invertibleⁿ
    : {F G : Functor C D} {α : F => G}
    → (β : G => F)
    → (∀ x → α .η x D.∘ β .η x ≡ D.id)
    → (∀ x → β .η x D.∘ α .η x ≡ D.id)
    → is-invertibleⁿ α
  to-is-invertibleⁿ β p q = CD.make-invertible β (ext p) (ext q)

  inversesⁿ→inverses
    : ∀ {F G} {α : F => G} {β : G => F}
    → Inversesⁿ α β
    → ∀ x → D.Inverses (α .η x) (β .η x)
  inversesⁿ→inverses inv x =
    D.make-inverses
      (CD.Inverses.invl inv ηₚ x)
      (CD.Inverses.invr inv ηₚ x)

  isoⁿ→is-invertibleⁿ : ∀ {F G : Functor C D} (i : F ≅ⁿ G) → is-invertibleⁿ (Isoⁿ.to i)
  isoⁿ→is-invertibleⁿ i = CD.iso→invertible i

  invertible→invertibleⁿ
    : ∀ {F G} (eta : F => G)
    → (∀ x → D.is-invertible (eta .η x))
    → is-invertibleⁿ eta
  invertible→invertibleⁿ eta i = to-is-invertibleⁿ ate (λ x → D.is-invertible.invl (i x)) λ x → D.is-invertible.invr (i x) where
    ate : _ => _
    ate .η x = D.is-invertible.inv (i x)
    ate .is-natural = inverse-is-natural eta _ (λ x → D.is-invertible.invl (i x)) (λ x → D.is-invertible.invr (i x))

  push-eqⁿ : ∀ {F G} (α : F ≅ⁿ G) {a b} {f g : C.Hom a b} → F .F₁ f ≡ F .F₁ g → G .F₁ f ≡ G .F₁ g
  push-eqⁿ {F = F} {G = G} α {f = f} {g} p =
    G .F₁ f                                           ≡⟨ D.insertl (α .Isoⁿ.invl ηₚ _) ⟩≡
    α .Isoⁿ.to .η _ D.∘ α .Isoⁿ.from .η _ D.∘ G .F₁ f ≡⟨ D.refl⟩∘⟨ α .Isoⁿ.from .is-natural _ _ _ ⟩≡
    α .Isoⁿ.to .η _ D.∘ F .F₁ f D.∘ α .Isoⁿ.from .η _ ≡⟨ D.refl⟩∘⟨ p D.⟩∘⟨refl ⟩≡
    α .Isoⁿ.to .η _ D.∘ F .F₁ g D.∘ α .Isoⁿ.from .η _ ≡˘⟨ D.refl⟩∘⟨ α .Isoⁿ.from .is-natural _ _ _ ⟩≡˘
    α .Isoⁿ.to .η _ D.∘ α .Isoⁿ.from .η _ D.∘ G .F₁ g ≡⟨ D.cancell (α .Isoⁿ.invl ηₚ _) ⟩≡
    G .F₁ g                                           ∎