proposition: Lemma fun_irrelevance `(C : Category) `(D : Category) : ∀ (a : C → D) (f g : ∀ {X Y : C}, (X ~> Y) → (a X ~> a Y)) i i' c c', @f = @g → {| fobj := @a ; fmap := @f ; functor_id_law := i ; functor_compose_law := c |} = {| fobj := @a ; fmap := @g ; functor_id_law := i' ; functor_compose_law := c' |}.
proof: Proof. intros. subst. f_equal. apply proof_irrelevance. apply proof_irrelevance. Qed.
imports: Category