proposition: Lemma fun_irrelevance `(F : Functor) : ∀ (f g : ∀ {X Y}, (X -> Y) → (F X -> F Y)) i i' c c', @f = @g → {| fmap := @f ; fun_identity := i ; fun_composition := c |} = {| fmap := @g ; fun_identity := i' ; fun_composition := c' |}.
proof: Proof. intros. subst. f_equal. apply proof_irrelevance. apply proof_irrelevance. Qed.
imports: Basics