Definition interlaced_prebilattice_transportf {X1 X2 : hSet} (b1 : interlaced_prebilattice X1) (b2 : interlaced_prebilattice X2) (p : X1 = X2) (m : meet (transportf interlaced_prebilattice p b1) ~ meet b2) (j : join (transportf interlaced_prebilattice p b1) ~ join b2) (c : consensus (transportf interlaced_prebilattice p b1) ~ consensus b2) (g : gullibility (transportf interlaced_prebilattice p b1) ~ gullibility b2) : transportf interlaced_prebilattice p b1 = b2. Proof. use total2_paths_f. - unfold interlaced_prebilattice. rewrite (pr1_transportf p b1). use prebilattice_transportf; [set (i := m) | set (i := j) | set (i := c) | set (i := g)]; use (homotcomp _ i); induction p; use homotrefl. - apply isaprop_is_interlaced. Defined.
Require Import UniMath.OrderTheory.Prebilattice.Prebilattice. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.Algebra.BinaryOperations.