Proposition comp_lens_mor {x₁ x₂ y₁ y₂ z₁ z₂ : C} {v₁ : x₁ --> x₂} {v₂ : y₁ --> y₂} {v₃ : z₁ --> z₂} {l₁ : lens x₁ y₁} {l₂ : lens y₁ z₁} {l₃ : lens x₂ y₂} {l₄ : lens y₂ z₂} (φ : lens_mor l₁ l₃ v₁ v₂) (ψ : lens_mor l₂ l₄ v₂ v₃) : lens_mor (comp_lens l₁ l₂) (comp_lens l₃ l₄) v₁ v₃. Proof. use make_lens_mor ; cbn. - rewrite !assoc'. rewrite (lens_mor_get ψ). rewrite !assoc. rewrite (lens_mor_get φ). apply idpath. - rewrite !assoc'. rewrite (lens_mor_put φ). rewrite !assoc. apply maponpaths_2. rewrite !postcompWithBinProductArrow. rewrite !precompWithBinProductArrow. rewrite !postcompWithBinProductArrow. rewrite !id_right. rewrite BinProductOfArrowsPr2. apply maponpaths_2. rewrite !assoc'. rewrite (lens_mor_put ψ). rewrite !assoc. apply maponpaths_2. rewrite id_left. rewrite !BinProductOfArrows_comp. rewrite id_left, id_right. apply maponpaths. rewrite (lens_mor_get φ). 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.