Library UniMath.Bicategories.Modifications.Examples.ApModification
A homotopy between homotopy gives rise to a modification
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.PrecategoryBinProduct.
Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Invertible_2cells.
Require Import UniMath.Bicategories.Core.BicategoryLaws.
Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat.
Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor.
Require Import UniMath.Bicategories.Transformations.PseudoTransformation.
Require Import UniMath.Bicategories.Modifications.Modification.
Import PseudoFunctor.Notations.
Require Import UniMath.Bicategories.Core.Examples.TwoType.
Require Import UniMath.Bicategories.PseudoFunctors.Examples.ApFunctor.
Require Import UniMath.Bicategories.Transformations.Examples.ApTransformation.
Local Open Scope cat.
Definition homothomotsec_natural
{X Y : UU}
{f g : X → Y}
{e₁ e₂ : f ~ g}
(h : e₁ ~ e₂)
{x y : X}
(p : x = y)
: homotsec_natural e₁ p
@ maponpaths (λ s : f y = g y, maponpaths f p @ s) (h y)
=
maponpaths (λ s : f x = g x, s @ maponpaths g p) (h x)
@ homotsec_natural e₂ p.
Show proof.
Section ApModification.
Context {X Y : UU}
(HX : isofhlevel 4 X)
(HY : isofhlevel 4 Y)
{f g : X → Y}
{e₁ e₂ : f ~ g}
(h : e₁ ~ e₂).
Definition ap_modification_data
: modification_data
(ap_pstrans HX HY e₁)
(ap_pstrans HX HY e₂)
:= h.
Definition ap_modification_is_modification
: is_modification ap_modification_data.
Show proof.
Definition ap_modification
: modification
(ap_pstrans HX HY e₁)
(ap_pstrans HX HY e₂).
Show proof.
End ApModification.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Invertible_2cells.
Require Import UniMath.Bicategories.Core.BicategoryLaws.
Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat.
Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor.
Require Import UniMath.Bicategories.Transformations.PseudoTransformation.
Require Import UniMath.Bicategories.Modifications.Modification.
Import PseudoFunctor.Notations.
Require Import UniMath.Bicategories.Core.Examples.TwoType.
Require Import UniMath.Bicategories.PseudoFunctors.Examples.ApFunctor.
Require Import UniMath.Bicategories.Transformations.Examples.ApTransformation.
Local Open Scope cat.
Definition homothomotsec_natural
{X Y : UU}
{f g : X → Y}
{e₁ e₂ : f ~ g}
(h : e₁ ~ e₂)
{x y : X}
(p : x = y)
: homotsec_natural e₁ p
@ maponpaths (λ s : f y = g y, maponpaths f p @ s) (h y)
=
maponpaths (λ s : f x = g x, s @ maponpaths g p) (h x)
@ homotsec_natural e₂ p.
Show proof.
Section ApModification.
Context {X Y : UU}
(HX : isofhlevel 4 X)
(HY : isofhlevel 4 Y)
{f g : X → Y}
{e₁ e₂ : f ~ g}
(h : e₁ ~ e₂).
Definition ap_modification_data
: modification_data
(ap_pstrans HX HY e₁)
(ap_pstrans HX HY e₂)
:= h.
Definition ap_modification_is_modification
: is_modification ap_modification_data.
Show proof.
Definition ap_modification
: modification
(ap_pstrans HX HY e₁)
(ap_pstrans HX HY e₂).
Show proof.
End ApModification.