proposition: Lemma nat_irrelevance : ∀ (f g : ∀ {X}, F X ~> G X) n n', @f = @g -> {| transport := @f; naturality := n |} = {| transport := @g; naturality := n' |}.
proof: Proof. intros. subst. f_equal. apply proof_irrelevance. Qed.
imports: Category