fact: Definition is_iso_square {C: predoublecategory_sq_hor_data} {a b : C} {g: a -v-> b} {h: a -v-> b} (α : get_predoublecat_sq_special g h): UU := ∑ (β : get_predoublecat_sq_special h g), ( (α ·sqh β) =hor_trans_id_left_sq (hor_sq_identity g)) × ( (β ·sqh α) = hor_trans_id_left_sq (hor_sq_identity h)).
imports: UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Notations UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence