Lemma weqinv_respects_prebilattice_structure {X1 : hSet} {X2 : hSet} (b1 : prebilattice X1) (b2 : prebilattice X2) (f : weq X1 X2) (p : respects_prebilattice_structure b1 b2 f) : respects_prebilattice_structure b2 b1 (invmap f). Proof. intros x y. do 3 (try use make_dirprod); rewrite <- (homotweqinvweq f x), <- (homotweqinvweq f y); [ rewrite (pr1 (p (invmap f x) (invmap f y))) | rewrite (pr12 (p (invmap f x) (invmap f y))) | rewrite (pr122 (p (invmap f x) (invmap f y))) | rewrite (pr222 (p (invmap f x) (invmap f y))) ]; now rewrite homotweqinvweq, homotweqinvweq, homotinvweqweq. Qed.
Require Import UniMath.OrderTheory.Prebilattice.Prebilattice. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.SIP. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.Tactics.