Definition folds_iso_comp_data : folds_iso_data a c. Proof. repeat split. - intro x; apply (weqcomp (ϕ₁ i) (ϕ₁ i')). - intro z; apply (weqcomp (ϕ₂ i) (ϕ₂ i')). - apply (weqcomp (ϕ∙ i) (ϕ∙ i')). Defined.
Require Import UniMath.Folds.UnicodeNotations. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.Folds.folds_precat. Require Import UniMath.Folds.from_precats_to_folds_and_back.