proposition: Proposition lens_mor_put {s₁ s₂ v₁ v₂ : C} {l₁ : lens s₁ v₁} {l₂ : lens s₂ v₂} {f : s₁ --> s₂} {g : v₁ --> v₂} (fg : lens_mor l₁ l₂ f g) : lens_put l₁ · f = BinProductOfArrows C (prodC v₂ s₂) (prodC v₁ s₁) g f · lens_put l₂.
proof: Proof. exact (pr21 fg). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Projection UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence UniMath.CategoryTheory.TwoSidedDisplayedCats.Total UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.FiberwiseProduct UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.DispCatOnTwoSidedDispCat