Proposition comp_lens_laws {x y z : C} (l₁ : lens x y) (l₂ : lens y z) : lenses_laws (comp_lens_data l₁ l₂). Proof. repeat split ; cbn. - rewrite !assoc'. etrans. { do 2 apply maponpaths. rewrite !assoc. rewrite lens_put_get. apply idpath. } etrans. { apply maponpaths. rewrite !assoc. rewrite BinProductOfArrowsPr1. rewrite !assoc'. rewrite lens_put_get. apply idpath. } rewrite !assoc. rewrite !BinProductPr1Commutes. rewrite id_left. rewrite BinProductOfArrowsPr1. rewrite id_right. apply idpath. - rewrite !assoc. etrans. { apply maponpaths_2. rewrite !assoc'. rewrite !postcompWithBinProductArrow. rewrite id_right. rewrite precompWithBinProductArrow. rewrite BinProductPr2Commutes. apply idpath. } refine (_ @ lens_get_put l₁). do 2 apply maponpaths_2. refine (_ @ id_right _). rewrite <- (lens_get_put l₂). rewrite !assoc. apply maponpaths_2. rewrite !precompWithBinProductArrow. rewrite id_right. rewrite id_right. rewrite postcompWithBinProductArrow. rewrite id_left, id_right. apply idpath. - pose (p₁ := lens_put_get l₁). pose (p₂ := lens_put_put l₂). pose (p₃ := lens_put_put l₁). etrans. { rewrite !assoc. apply maponpaths_2. rewrite !postcompWithBinProductArrow. rewrite precompWithBinProductArrow. rewrite !postcompWithBinProductArrow. rewrite !id_left. rewrite !id_right. rewrite BinProductOfArrowsPr2. rewrite !assoc. rewrite precompWithBinProductArrow. apply maponpaths_2. rewrite BinProductOfArrows_comp. rewrite id_left. rewrite !assoc'. rewrite p₁. rewrite BinProductPr1Commutes. etrans. { do 2 apply maponpaths_2. exact (!(id_left _)). } rewrite <- BinProductOfArrows_comp. rewrite !assoc'. rewrite p₂. rewrite !assoc. rewrite precompWithBinProductArrow. rewrite BinProductOfArrowsPr1. rewrite id_right. rewrite !assoc. rewrite !BinProductOfArrowsPr2. rewrite !assoc'. rewrite BinProductOfArrowsPr2. apply idpath. } clear p₁ p₂. etrans. { etrans. { do 2 apply maponpaths_2. exact (!(id_right _)). } etrans. { apply maponpaths_2. refine (!_). apply (postcompWithBinProductArrow _ (prodC _ _) (prodC _ _)). } rewrite !assoc'. rewrite p₃. rewrite !assoc. rewrite precompWithBinProductArrow. rewrite !assoc. rewrite !BinProductPr1Commutes. rewrite !BinProductPr2Commutes. apply idpath. } rewrite !assoc. apply maponpaths_2. rewrite !precompWithBinProductArrow. rewrite !postcompWithBinProductArrow. rewrite !id_right. rewrite !BinProductPr2Commutes. apply maponpaths_2. rewrite !assoc. apply maponpaths_2. rewrite !postcompWithBinProductArrow. rewrite id_right. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Projection. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Total. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.FiberwiseProduct. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.DispCatOnTwoSidedDispCat.