proposition: Lemma ixfun_irrelevance `(F : IxFunctor) : ∀ (f g : ∀ {I O X Y}, (X -> Y) → (F I O X -> F I O Y)) i i' c c', @f = @g → {| ixmap := @f ; ixfun_identity := i ; ixfun_composition := c |} = {| ixmap := @g ; ixfun_identity := i' ; ixfun_composition := c' |}.
proof: Proof. intros. subst. f_equal. apply proof_irrelevance. apply proof_irrelevance. Qed.
imports: Hask.Ltac Coq.Program.Equality Coq.Unicode.Utf8 FunctionalExtensionality Iso Tuple