Definition nattrans_naturality {B C:category} {F F':[B, C]} {b b':B} (p : F --> F') (f : b --> b') : p ◽ b' ∘ F ▭ f = F' ▭ f ∘ p ◽ b := nat_trans_ax p _ _ f.
Require Import UniMath.MoreFoundations.Tactics.