proposition: Lemma pfun_irrelevance `(F : PFunctor) : ∀ (f g : ∀ {X Y}, (X :→ Y) → (F X :→ F Y)) i i' c c', @f = @g → {| pmap := @f ; pfun_identity := i ; pfun_composition := c |} = {| pmap := @g ; pfun_identity := i' ; pfun_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