# Natural transformations

Authors: Benedikt Ahrens, Chris Kapulkin, Mike Shulman (January 2013)

## Contents

• Definition of natural transformations
• Equality is pointwise equality
• Identity natural transformation
• Composition of natural transformations
• Natural isomorphisms

## Definition of natural transformations

Definition nat_trans_data {C C' : precategory_ob_mor} (F F' : functor_data C C'): UU :=
x : ob C, F x --> F' x.

Definition is_nat_trans {C C' : precategory_data}
(F F' : functor_data C C') (t : nat_trans_data F F') :=
(x x' : ob C)(f : x --> x'), # F f · t x' = t x · #F' f.

Lemma isaprop_is_nat_trans (C C' : precategory_data) (hs: has_homsets C')
(F F' : functor_data C C') (t : nat_trans_data F F'):
isaprop (is_nat_trans F F' t).
Proof.
repeat (apply impred; intro).
apply hs.
Qed.

Definition nat_trans {C C' : precategory_data} (F F' : functor_data C C') : UU :=
total2 (fun t : nat_trans_data F F'is_nat_trans F F' t).

Notation "F ⟹ G" := (nat_trans F G) (at level 39) : cat.

Definition make_nat_trans {C C' : precategory_data} (F F' : functor_data C C')
(t : nat_trans_data F F') (H : is_nat_trans F F' t) :
nat_trans F F'.
Proof.
t.
exact H.
Defined.

Lemma isaset_nat_trans {C C' : precategory_data} (hs: has_homsets C')
(F F' : functor_data C C') : isaset (nat_trans F F').
Proof.
apply (isofhleveltotal2 2).
+ apply impred; intro t; apply hs.
+ intro x; apply isasetaprop, isaprop_is_nat_trans, hs.
Qed.

Definition nat_trans_data_from_nat_trans {C C' : precategory_data}
{F F' : functor_data C C'}(a : nat_trans F F') :
nat_trans_data F F' := pr1 a.

Definition nat_trans_data_from_nat_trans_funclass {C C' : precategory_data}
{F F' : functor_data C C'}(a : nat_trans F F') :
x : ob C, F x --> F' x := pr1 a.
Coercion nat_trans_data_from_nat_trans_funclass : nat_trans >-> Funclass.

Definition nat_trans_ax {C C' : precategory_data}
{F F' : functor_data C C'} (a : nat_trans F F') :
(x x' : ob C)(f : x --> x'),
#F f · a x' = a x · #F' f := pr2 a.

Equality between two natural transformations

Lemma nat_trans_eq {C C' : precategory_data} (hs: has_homsets C')
(F F' : functor_data C C')(a a' : nat_trans F F'):
( x, a x = a' x) a = a'.
Proof.
intro H.
assert (H' : pr1 a = pr1 a').
{ now apply funextsec. }
apply (total2_paths_f H'), proofirrelevance, isaprop_is_nat_trans, hs.
Qed.

Section nat_trans_eq.

Context {C D : precategory}.
Variable hsD : has_homsets D.
Context {F G : functor C D}.
Variables alpha beta : nat_trans F G.

Definition nat_trans_eq_weq : (alpha = beta) ( c, alpha c = beta c).
Proof.
eapply weqcomp.
- apply subtypeInjectivity.
intro x. apply isaprop_is_nat_trans. apply hsD.
- apply weqtoforallpaths.
Defined.

End nat_trans_eq.

Definition nat_trans_eq_pointwise {C C' : precategory_data}
{F F' : functor_data C C'} {a a' : nat_trans F F'}:
a = a' x, a x = a' x.
Proof.
intro; apply toforallpaths, maponpaths; assumption.
Qed.

a more intuitive variant of functor_data_eq
Lemma functor_data_eq_from_nat_trans (C C': precategory) (F F' : functor_data C C')
(H : F ¬ F') (H1 : is_nat_trans F F' (fun c:Cidtomor _ _ (H c))) :
F = F'.
Proof.
apply (functor_data_eq _ _ _ _ H).
intros c1 c2 f.
rewrite double_transport_idtoiso.
rewrite <- assoc.
apply iso_inv_on_right.
unfold morphism_from_iso.
do 2 rewrite eq_idtoiso_idtomor.
apply H1.
Qed.

## Identity natural transformation

Lemma is_nat_trans_id {C : precategory_data}{C' : precategory}
(F : functor_data C C') : is_nat_trans F F
(λ c : ob C, identity (F c)).
Proof.
intros ? ? ? .
now rewrite id_left, id_right.
Qed.

Definition nat_trans_id {C:precategory_data}{C' : precategory}
(F : functor_data C C') : nat_trans F F :=
tpair _ _ (is_nat_trans_id F).

## Composition of natural transformations

Lemma is_nat_trans_comp {C : precategory_data}{C' : precategory}
{F G H : functor_data C C'}
(a : nat_trans F G)
(b : nat_trans G H): is_nat_trans F H
(λ x : ob C, a x · b x).
Proof.
intros ? ? ?.
now rewrite assoc, nat_trans_ax, <- assoc, nat_trans_ax, assoc.
Qed.

Definition nat_trans_comp {C:precategory_data}{C' : precategory}
(F G H: functor_data C C')
(a : nat_trans F G)
(b : nat_trans G H): nat_trans F H :=
tpair _ _ (is_nat_trans_comp a b).

Natural transformations for reasoning about various compositions of functors
Section nat_trans_functor.

Context {A B C D : precategory}.

Definition nat_trans_functor_id_right (F : functor A B) :
nat_trans (functor_composite F (functor_identity B)) F.
Proof.
(λ x, identity _).
abstract (now intros a b f; rewrite id_left, id_right).
Defined.

Definition nat_trans_functor_id_right_inv (F : functor A B) :
nat_trans F (functor_composite F (functor_identity B)) :=
nat_trans_functor_id_right F.

Definition nat_trans_functor_id_left (F : functor A B) :
nat_trans (functor_composite (functor_identity A) F) F :=
nat_trans_functor_id_right F.

Definition nat_trans_functor_id_left_inv (F : functor A B) :
nat_trans F (functor_composite (functor_identity A) F) :=
nat_trans_functor_id_right F.

Definition nat_trans_functor_assoc (F1 : functor A B) (F2 : functor B C) (F3 : functor C D) :
nat_trans (functor_composite (functor_composite F1 F2) F3)
(functor_composite F1 (functor_composite F2 F3)).
Proof.
(λ x, identity _).
abstract (now intros a b f; rewrite id_right, id_left).
Defined.

Definition nat_trans_functor_assoc_inv (F1 : functor A B) (F2 : functor B C) (F3 : functor C D) :
nat_trans (functor_composite F1 (functor_composite F2 F3))
(functor_composite (functor_composite F1 F2) F3) :=
nat_trans_functor_assoc F1 F2 F3.

End nat_trans_functor.

## Natural isomorphisms

Definition is_nat_iso {C D : precategory} {F G : C D} (μ : F G) : UU :=
(c : C), is_iso (μ c).

Definition isaprop_is_nat_iso
{C D : category}
{F G : C D}
(α : F G)
: isaprop (is_nat_iso α).
Proof.
apply impred.
intro.
apply isaprop_is_iso.
Defined.

Definition is_nat_id {C D : precategory} {F : C D} (μ : F F) : UU :=
(c : C), μ c = identity (F c).

Definition nat_iso {C D : precategory} (F G : C D) : UU
:= (μ : F G), is_nat_iso μ.

Definition make_nat_iso {C D : precategory} (F G : C D) (μ : F G) (is_iso : is_nat_iso μ) : nat_iso F G.
Proof.
μ.
exact is_iso.
Defined.

Definition iso_inv_after_iso' {C : precategory} {a b : C} (f : a --> b) (f' : iso a b) (deref : pr1 f' = f) : f · inv_from_iso f' = identity _.
Proof.
rewrite <- deref.
exact (iso_inv_after_iso f').
Defined.

Definition iso_after_iso_inv' {C : precategory} {a b : C} (f : a --> b) (f' : iso a b) (deref : pr1 f' = f) : inv_from_iso f' · f = identity _.
Proof.
rewrite <- deref.
exact (iso_after_iso_inv f').
Defined.

Definition nat_iso_inv {C D : precategory} {F G : C D} (μ : nat_iso F G) : nat_iso G F.
Proof.
pose (iso := (λ c, make_iso _ (pr2 μ c))).
pose (inv := (λ c, inv_from_iso (iso c))).
use tpair.
- inv.
intros c c' f.
pose (coher := pr2 (pr1 μ) c c' f).
pose (coher_inv := maponpaths (λ p, inv c · p · inv c') coher).
simpl in coher_inv.
repeat rewrite <- assoc in coher_inv.
unfold inv in coher_inv.
assert (coher_inv' : (inv_from_iso (iso c) · (# F f · ((pr1 μ) c' · inv_from_iso (iso c'))) = inv_from_iso (iso c) · (pr1 (pr1 μ) c · (# G f · inv_from_iso (iso c'))))) by assumption.
clear coher_inv; rename coher_inv' into coher_inv.
assert (deref' : pr1 (iso c') = (pr1 μ) c') by reflexivity.
rewrite (iso_inv_after_iso' ((pr1 μ) c') (iso c') deref') in coher_inv.
rewrite id_right in coher_inv.
repeat rewrite assoc in coher_inv.
assert (deref : pr1 (iso c) = (pr1 μ) c) by reflexivity.
assert (coher_inv' : (inv_from_iso (iso c) · # F f = inv_from_iso (iso c) · (pr1 μ) c · # G f · inv_from_iso (iso c'))) by assumption.
clear coher_inv; rename coher_inv' into coher_inv.
rewrite (iso_after_iso_inv' ((pr1 μ) c) (iso c) deref) in coher_inv.
rewrite id_left in coher_inv.
unfold inv.
symmetry.
assumption.
- intro c.
exact (is_iso_inv_from_iso (iso c)).
Defined.

Definition nat_iso_to_trans {C D : precategory} {F G : C D} (ν : nat_iso F G) : F G :=
pr1 ν.

Coercion nat_iso_to_trans : nat_iso >-> nat_trans.

Definition nat_iso_to_trans_inv {C D : precategory} {F G : C D} (ν : nat_iso F G) : G F :=
pr1 (nat_iso_inv ν).

Definition nat_comp_to_endo {C D : precategory} {F G : C D} (eq : F = G) {c : C} (f : F c --> G c) : F c --> F c.
Proof.
rewrite <- eq in f.
assumption.
Defined.

Definition is_nat_iso_id {C D : precategory} {F G : C D} (eq : F = G) (ν : nat_iso F G) : UU :=
(c : C), nat_comp_to_endo eq (nat_iso_to_trans ν c) = identity (F c).

Definition induced_precategory_incl {M : precategory} {X:Type} (j : X ob M) :
induced_precategory M j M.
Proof.
use make_functor.
- use make_functor_data.
+ exact j.
+ intros a b f. exact f.
- repeat split.
Defined.

End nat_trans.

Notation "F ⟹ G" := (nat_trans F G) (at level 39) : cat.