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)