proposition: Lemma iso_irrelevance `(C : Category) {X Y : C} : ∀ (f g : X ~> Y) (k h : Y ~> X) tl tl' fl fl', @f = @g → @k = @h → {| to := f ; from := k ; iso_to := tl ; iso_from := fl |} = {| to := g ; from := h ; iso_to := tl' ; iso_from := fl' |}.
proof: Proof. intros. subst. f_equal. apply proof_irrelevance. apply proof_irrelevance. Qed.
imports: Hask.Prelude Hask.Crush Coq.Unicode.Utf8 FunctionalExtensionality