proposition: Lemma cat_irrelevance `(C : Category) `(D : Category) : ∀ (m n : ∀ {A}, A ~> A) (p q : ∀ {A B C}, (B ~> C) → (A ~> B) → (A ~> C)) l l' r r' c c', @m = @n → @p = @q → {| ob := C ; hom := @hom C ; c_id := @m ; c_comp := @p ; c_left_id := l ; c_right_id := r ; c_comp_assoc := c |} = {| ob := C ; hom := @hom C ; c_id := @n ; c_comp := @q ; c_left_id := l' ; c_right_id := r' ; c_comp_assoc := c' |}.
proof: Proof. intros. subst. f_equal. apply proof_irrelevance. apply proof_irrelevance. apply proof_irrelevance. Qed.
imports: Hask.Prelude Hask.Crush Coq.Unicode.Utf8 FunctionalExtensionality