Library UniMath.CategoryTheory.Profunctors.Squares
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.Categories.HSET.All.
Require Import UniMath.CategoryTheory.Categories.HSET.SetCoends.
Require Import UniMath.CategoryTheory.Profunctors.Core.
Require Import UniMath.CategoryTheory.Profunctors.Examples.
Require Import UniMath.CategoryTheory.Profunctors.Transformation.
Local Open Scope cat.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.Categories.HSET.All.
Require Import UniMath.CategoryTheory.Categories.HSET.SetCoends.
Require Import UniMath.CategoryTheory.Profunctors.Core.
Require Import UniMath.CategoryTheory.Profunctors.Examples.
Require Import UniMath.CategoryTheory.Profunctors.Transformation.
Local Open Scope cat.
Definition profunctor_square
{C₁ C₂ D₁ D₂ : category}
(F : C₁ ⟶ C₂)
(G : D₁ ⟶ D₂)
(P : D₁ ↛ C₁)
(Q : D₂ ↛ C₂)
: UU
:= profunctor_nat_trans P (precomp_profunctor G F Q).
Identity Coercion square_to_nat_trans : profunctor_square >-> profunctor_nat_trans.
Proposition profunctor_square_natural
{C₁ C₂ D₁ D₂ : category}
{F : C₁ ⟶ C₂}
{G : D₁ ⟶ D₂}
{P : D₁ ↛ C₁}
{Q : D₂ ↛ C₂}
(τ : profunctor_square F G P Q)
{y₁ y₂ : C₁}
{x₁ x₂ : D₁}
(g : y₂ --> y₁)
(f : x₁ --> x₂)
(h : P y₁ x₁)
: τ y₂ x₂ (P #[ g , f ] h)
=
Q #[ #F g , #G f ] (τ y₁ x₁ h).
Show proof.
Proposition profunctor_square_lmap
{C₁ C₂ D₁ D₂ : category}
{F : C₁ ⟶ C₂}
{G : D₁ ⟶ D₂}
{P : D₁ ↛ C₁}
{Q : D₂ ↛ C₂}
(τ : profunctor_square F G P Q)
{y₁ y₂ : C₁}
{x : D₁}
(g : y₂ --> y₁)
(h : P y₁ x)
: τ y₂ x (lmap P g h)
=
lmap Q (#F g) (τ y₁ x h).
Show proof.
Proposition profunctor_square_rmap
{C₁ C₂ D₁ D₂ : category}
{F : C₁ ⟶ C₂}
{G : D₁ ⟶ D₂}
{P : D₁ ↛ C₁}
{Q : D₂ ↛ C₂}
(τ : profunctor_square F G P Q)
{y : C₁}
{x₁ x₂ : D₁}
(f : x₁ --> x₂)
(h : P y x₁)
: τ y x₂ (rmap P f h)
=
rmap Q (#G f) (τ y x₁ h).
Show proof.
Proposition profunctor_square_lmap_rmap
{C₁ C₂ D₁ D₂ : category}
{F : C₁ ⟶ C₂}
{G : D₁ ⟶ D₂}
{P : D₁ ↛ C₁}
{Q : D₂ ↛ C₂}
(τ : profunctor_square F G P Q)
{y₁ y₂ : C₁}
{x₁ x₂ : D₁}
(g : y₂ --> y₁)
(f : x₁ --> x₂)
(h : P y₁ x₁)
: τ y₂ x₂ (lmap P g (rmap P f h))
=
lmap Q (#F g) (rmap Q (#G f) (τ y₁ x₁ h)).
Show proof.
Definition profunctor_iso_square
{C₁ C₂ D₁ D₂ : category}
(F : C₁ ⟶ C₂)
(G : D₁ ⟶ D₂)
(P : D₁ ↛ C₁)
(Q : D₂ ↛ C₂)
: UU
:= ∑ (τ : profunctor_square F G P Q), is_profunctor_nat_iso τ.
Coercion profunctor_iso_square_to_square
{C₁ C₂ D₁ D₂ : category}
{F : C₁ ⟶ C₂}
{G : D₁ ⟶ D₂}
{P : D₁ ↛ C₁}
{Q : D₂ ↛ C₂}
(τ : profunctor_iso_square F G P Q)
: profunctor_square F G P Q
:= pr1 τ.
Coercion profunctor_iso_square_is_iso
{C₁ C₂ D₁ D₂ : category}
{F : C₁ ⟶ C₂}
{G : D₁ ⟶ D₂}
{P : D₁ ↛ C₁}
{Q : D₂ ↛ C₂}
(τ : profunctor_iso_square F G P Q)
: is_profunctor_nat_iso τ
:= pr2 τ.
{C₁ C₂ D₁ D₂ : category}
(F : C₁ ⟶ C₂)
(G : D₁ ⟶ D₂)
(P : D₁ ↛ C₁)
(Q : D₂ ↛ C₂)
: UU
:= profunctor_nat_trans P (precomp_profunctor G F Q).
Identity Coercion square_to_nat_trans : profunctor_square >-> profunctor_nat_trans.
Proposition profunctor_square_natural
{C₁ C₂ D₁ D₂ : category}
{F : C₁ ⟶ C₂}
{G : D₁ ⟶ D₂}
{P : D₁ ↛ C₁}
{Q : D₂ ↛ C₂}
(τ : profunctor_square F G P Q)
{y₁ y₂ : C₁}
{x₁ x₂ : D₁}
(g : y₂ --> y₁)
(f : x₁ --> x₂)
(h : P y₁ x₁)
: τ y₂ x₂ (P #[ g , f ] h)
=
Q #[ #F g , #G f ] (τ y₁ x₁ h).
Show proof.
pose (eqtohomot (pr2 τ (y₁ ,, x₁) (y₂ ,, x₂) (g ,, f)) h) as p.
cbn in p.
refine (p @ _).
rewrite lmap_rmap_functor.
apply idpath.
cbn in p.
refine (p @ _).
rewrite lmap_rmap_functor.
apply idpath.
Proposition profunctor_square_lmap
{C₁ C₂ D₁ D₂ : category}
{F : C₁ ⟶ C₂}
{G : D₁ ⟶ D₂}
{P : D₁ ↛ C₁}
{Q : D₂ ↛ C₂}
(τ : profunctor_square F G P Q)
{y₁ y₂ : C₁}
{x : D₁}
(g : y₂ --> y₁)
(h : P y₁ x)
: τ y₂ x (lmap P g h)
=
lmap Q (#F g) (τ y₁ x h).
Show proof.
pose (eqtohomot (pr2 τ (y₁ ,, x) (y₂ ,, x) (g ,, identity _)) h) as p.
cbn in p.
rewrite functor_id in p.
rewrite rmap_id in p.
exact p.
cbn in p.
rewrite functor_id in p.
rewrite rmap_id in p.
exact p.
Proposition profunctor_square_rmap
{C₁ C₂ D₁ D₂ : category}
{F : C₁ ⟶ C₂}
{G : D₁ ⟶ D₂}
{P : D₁ ↛ C₁}
{Q : D₂ ↛ C₂}
(τ : profunctor_square F G P Q)
{y : C₁}
{x₁ x₂ : D₁}
(f : x₁ --> x₂)
(h : P y x₁)
: τ y x₂ (rmap P f h)
=
rmap Q (#G f) (τ y x₁ h).
Show proof.
pose (eqtohomot (pr2 τ (y ,, x₁) (y ,, x₂) (identity _ ,, f)) h) as p.
cbn in p.
rewrite functor_id in p.
rewrite lmap_id in p.
exact p.
cbn in p.
rewrite functor_id in p.
rewrite lmap_id in p.
exact p.
Proposition profunctor_square_lmap_rmap
{C₁ C₂ D₁ D₂ : category}
{F : C₁ ⟶ C₂}
{G : D₁ ⟶ D₂}
{P : D₁ ↛ C₁}
{Q : D₂ ↛ C₂}
(τ : profunctor_square F G P Q)
{y₁ y₂ : C₁}
{x₁ x₂ : D₁}
(g : y₂ --> y₁)
(f : x₁ --> x₂)
(h : P y₁ x₁)
: τ y₂ x₂ (lmap P g (rmap P f h))
=
lmap Q (#F g) (rmap Q (#G f) (τ y₁ x₁ h)).
Show proof.
Definition profunctor_iso_square
{C₁ C₂ D₁ D₂ : category}
(F : C₁ ⟶ C₂)
(G : D₁ ⟶ D₂)
(P : D₁ ↛ C₁)
(Q : D₂ ↛ C₂)
: UU
:= ∑ (τ : profunctor_square F G P Q), is_profunctor_nat_iso τ.
Coercion profunctor_iso_square_to_square
{C₁ C₂ D₁ D₂ : category}
{F : C₁ ⟶ C₂}
{G : D₁ ⟶ D₂}
{P : D₁ ↛ C₁}
{Q : D₂ ↛ C₂}
(τ : profunctor_iso_square F G P Q)
: profunctor_square F G P Q
:= pr1 τ.
Coercion profunctor_iso_square_is_iso
{C₁ C₂ D₁ D₂ : category}
{F : C₁ ⟶ C₂}
{G : D₁ ⟶ D₂}
{P : D₁ ↛ C₁}
{Q : D₂ ↛ C₂}
(τ : profunctor_iso_square F G P Q)
: is_profunctor_nat_iso τ
:= pr2 τ.
Definition profunctor_square_data
{C₁ C₂ D₁ D₂ : category}
(F : C₁ ⟶ C₂)
(G : D₁ ⟶ D₂)
(P : D₁ ↛ C₁)
(Q : D₂ ↛ C₂)
: UU
:= ∏ (y : C₁) (x : D₁), P y x → Q (F y) (G x).
Definition profunctor_square_laws
{C₁ C₂ D₁ D₂ : category}
{F : C₁ ⟶ C₂}
{G : D₁ ⟶ D₂}
{P : D₁ ↛ C₁}
{Q : D₂ ↛ C₂}
(τ : profunctor_square_data F G P Q)
: UU
:= ∏ (y₁ y₂ : C₁)
(x₁ x₂ : D₁)
(g : y₂ --> y₁)
(f : x₁ --> x₂)
(h : P y₁ x₁),
τ y₂ x₂ (lmap P g (rmap P f h))
=
lmap Q (#F g) (rmap Q (#G f) (τ y₁ x₁ h)).
Section ProfunctorSquareBuilder.
Context {C₁ C₂ D₁ D₂ : category}
{F : C₁ ⟶ C₂}
{G : D₁ ⟶ D₂}
{P : D₁ ↛ C₁}
{Q : D₂ ↛ C₂}
(τ : profunctor_square_data F G P Q)
(Hτ : profunctor_square_laws τ).
Definition make_profunctor_square_data
: profunctor_nat_trans_data P (precomp_profunctor G F Q)
:= τ.
Arguments make_profunctor_square_data /.
Proposition make_profunctor_square_law
: profunctor_nat_trans_law make_profunctor_square_data.
Show proof.
Definition make_profunctor_square
: profunctor_square F G P Q.
Show proof.
Arguments make_profunctor_square_data {C₁ C₂ D₁ D₂ F G P Q} τ /.
Proposition eq_profunctor_square
{C₁ C₂ D₁ D₂ : category}
{F : C₁ ⟶ C₂}
{G : D₁ ⟶ D₂}
{P : D₁ ↛ C₁}
{Q : D₂ ↛ C₂}
{τ τ' : profunctor_square F G P Q}
(p : ∏ (y : C₁) (x : D₁)
(h : P y x),
τ y x h = τ' y x h)
: τ = τ'.
Show proof.
Proposition profunctor_square_eq_pointwise
{C₁ C₂ D₁ D₂ : category}
{F : C₁ ⟶ C₂}
{G : D₁ ⟶ D₂}
{P : D₁ ↛ C₁}
{Q : D₂ ↛ C₂}
{τ τ' : profunctor_square F G P Q}
(p : τ = τ')
{y : C₁} {x : D₁}
(h : P y x)
: τ y x h = τ' y x h.
Show proof.
Proposition isaset_profunctor_square
{C₁ C₂ D₁ D₂ : category}
(F : C₁ ⟶ C₂)
(G : D₁ ⟶ D₂)
(P : D₁ ↛ C₁)
(Q : D₂ ↛ C₂)
: isaset (profunctor_square F G P Q).
Show proof.
{C₁ C₂ D₁ D₂ : category}
(F : C₁ ⟶ C₂)
(G : D₁ ⟶ D₂)
(P : D₁ ↛ C₁)
(Q : D₂ ↛ C₂)
: UU
:= ∏ (y : C₁) (x : D₁), P y x → Q (F y) (G x).
Definition profunctor_square_laws
{C₁ C₂ D₁ D₂ : category}
{F : C₁ ⟶ C₂}
{G : D₁ ⟶ D₂}
{P : D₁ ↛ C₁}
{Q : D₂ ↛ C₂}
(τ : profunctor_square_data F G P Q)
: UU
:= ∏ (y₁ y₂ : C₁)
(x₁ x₂ : D₁)
(g : y₂ --> y₁)
(f : x₁ --> x₂)
(h : P y₁ x₁),
τ y₂ x₂ (lmap P g (rmap P f h))
=
lmap Q (#F g) (rmap Q (#G f) (τ y₁ x₁ h)).
Section ProfunctorSquareBuilder.
Context {C₁ C₂ D₁ D₂ : category}
{F : C₁ ⟶ C₂}
{G : D₁ ⟶ D₂}
{P : D₁ ↛ C₁}
{Q : D₂ ↛ C₂}
(τ : profunctor_square_data F G P Q)
(Hτ : profunctor_square_laws τ).
Definition make_profunctor_square_data
: profunctor_nat_trans_data P (precomp_profunctor G F Q)
:= τ.
Arguments make_profunctor_square_data /.
Proposition make_profunctor_square_law
: profunctor_nat_trans_law make_profunctor_square_data.
Show proof.
intros y₁ y₂ x₁ x₂ g f h ; cbn -[lmap rmap].
rewrite lmap_precomp_profunctor, rmap_precomp_profunctor.
apply Hτ.
rewrite lmap_precomp_profunctor, rmap_precomp_profunctor.
apply Hτ.
Definition make_profunctor_square
: profunctor_square F G P Q.
Show proof.
use make_profunctor_nat_trans.
- exact make_profunctor_square_data.
- exact make_profunctor_square_law.
End ProfunctorSquareBuilder.- exact make_profunctor_square_data.
- exact make_profunctor_square_law.
Arguments make_profunctor_square_data {C₁ C₂ D₁ D₂ F G P Q} τ /.
Proposition eq_profunctor_square
{C₁ C₂ D₁ D₂ : category}
{F : C₁ ⟶ C₂}
{G : D₁ ⟶ D₂}
{P : D₁ ↛ C₁}
{Q : D₂ ↛ C₂}
{τ τ' : profunctor_square F G P Q}
(p : ∏ (y : C₁) (x : D₁)
(h : P y x),
τ y x h = τ' y x h)
: τ = τ'.
Show proof.
Proposition profunctor_square_eq_pointwise
{C₁ C₂ D₁ D₂ : category}
{F : C₁ ⟶ C₂}
{G : D₁ ⟶ D₂}
{P : D₁ ↛ C₁}
{Q : D₂ ↛ C₂}
{τ τ' : profunctor_square F G P Q}
(p : τ = τ')
{y : C₁} {x : D₁}
(h : P y x)
: τ y x h = τ' y x h.
Show proof.
Proposition isaset_profunctor_square
{C₁ C₂ D₁ D₂ : category}
(F : C₁ ⟶ C₂)
(G : D₁ ⟶ D₂)
(P : D₁ ↛ C₁)
(Q : D₂ ↛ C₂)
: isaset (profunctor_square F G P Q).
Show proof.
Definition profunctor_nat_trans_to_square
{C D : category}
{P Q : D ↛ C}
(τ : profunctor_nat_trans P Q)
: profunctor_square (functor_identity _) (functor_identity _) P Q.
Show proof.
Definition profunctor_square_to_profunctor_nat_trans
{C D : category}
{P Q : D ↛ C}
(τ : profunctor_square (functor_identity _) (functor_identity _) P Q)
: profunctor_nat_trans P Q.
Show proof.
Definition profunctor_nat_trans_weq_square
{C D : category}
(P Q : D ↛ C)
: profunctor_nat_trans P Q
≃
profunctor_square (functor_identity _) (functor_identity _) P Q.
Show proof.
Definition profunctor_nat_iso_weq_iso_square
{C D : category}
(P Q : D ↛ C)
: profunctor_nat_iso P Q
≃
profunctor_iso_square (functor_identity _) (functor_identity _) P Q.
Show proof.
Definition profunctor_square_to_nat_trans
{C₁ C₂ : category}
{F G : C₁ ⟶ C₂}
(τ : profunctor_square G F (id_profunctor C₁) (id_profunctor C₂))
: G ⟹ F.
Show proof.
{C D : category}
{P Q : D ↛ C}
(τ : profunctor_nat_trans P Q)
: profunctor_square (functor_identity _) (functor_identity _) P Q.
Show proof.
use make_profunctor_square.
- exact (λ y x h, τ y x h).
- abstract
(intros y₁ y₂ x₁ x₂ g f h ; cbn -[lmap rmap] ;
rewrite profunctor_nat_trans_lmap_rmap ;
apply idpath).
- exact (λ y x h, τ y x h).
- abstract
(intros y₁ y₂ x₁ x₂ g f h ; cbn -[lmap rmap] ;
rewrite profunctor_nat_trans_lmap_rmap ;
apply idpath).
Definition profunctor_square_to_profunctor_nat_trans
{C D : category}
{P Q : D ↛ C}
(τ : profunctor_square (functor_identity _) (functor_identity _) P Q)
: profunctor_nat_trans P Q.
Show proof.
use make_profunctor_nat_trans.
- exact (λ y x h, τ y x h).
- abstract
(intros y₁ y₂ x₁ x₂ g f h ; cbn -[lmap rmap] ;
rewrite profunctor_square_lmap_rmap ; cbn ;
apply idpath).
- exact (λ y x h, τ y x h).
- abstract
(intros y₁ y₂ x₁ x₂ g f h ; cbn -[lmap rmap] ;
rewrite profunctor_square_lmap_rmap ; cbn ;
apply idpath).
Definition profunctor_nat_trans_weq_square
{C D : category}
(P Q : D ↛ C)
: profunctor_nat_trans P Q
≃
profunctor_square (functor_identity _) (functor_identity _) P Q.
Show proof.
use weq_iso.
- exact profunctor_nat_trans_to_square.
- exact profunctor_square_to_profunctor_nat_trans.
- abstract
(intros τ ;
use eq_profunctor_nat_trans ;
intros ; cbn ;
apply idpath).
- abstract
(intros τ ;
use eq_profunctor_square ;
intros ; cbn ;
apply idpath).
- exact profunctor_nat_trans_to_square.
- exact profunctor_square_to_profunctor_nat_trans.
- abstract
(intros τ ;
use eq_profunctor_nat_trans ;
intros ; cbn ;
apply idpath).
- abstract
(intros τ ;
use eq_profunctor_square ;
intros ; cbn ;
apply idpath).
Definition profunctor_nat_iso_weq_iso_square
{C D : category}
(P Q : D ↛ C)
: profunctor_nat_iso P Q
≃
profunctor_iso_square (functor_identity _) (functor_identity _) P Q.
Show proof.
use (weqtotal2 (profunctor_nat_trans_weq_square P Q)).
intro τ.
use weqimplimpl.
- intros Hτ y x.
exact (Hτ y x).
- intros Hτ y x.
exact (Hτ y x).
- apply isaprop_is_profunctor_nat_iso.
- apply isaprop_is_profunctor_nat_iso.
intro τ.
use weqimplimpl.
- intros Hτ y x.
exact (Hτ y x).
- intros Hτ y x.
exact (Hτ y x).
- apply isaprop_is_profunctor_nat_iso.
- apply isaprop_is_profunctor_nat_iso.
Definition profunctor_square_to_nat_trans
{C₁ C₂ : category}
{F G : C₁ ⟶ C₂}
(τ : profunctor_square G F (id_profunctor C₁) (id_profunctor C₂))
: G ⟹ F.
Show proof.
use make_nat_trans.
- exact (λ x, τ x x (identity x)).
- abstract
(intros x y f ; cbn ;
pose (profunctor_square_natural τ (identity x) f (identity x)) as p ;
cbn in p ;
rewrite !functor_id in p ;
rewrite !id_left in p ;
rewrite <- p ;
pose (profunctor_square_natural τ f (identity y) (identity y)) as q ;
cbn in q ;
rewrite !functor_id in q ;
rewrite !id_right in q ;
rewrite <- q ;
apply idpath).
- exact (λ x, τ x x (identity x)).
- abstract
(intros x y f ; cbn ;
pose (profunctor_square_natural τ (identity x) f (identity x)) as p ;
cbn in p ;
rewrite !functor_id in p ;
rewrite !id_left in p ;
rewrite <- p ;
pose (profunctor_square_natural τ f (identity y) (identity y)) as q ;
cbn in q ;
rewrite !functor_id in q ;
rewrite !id_right in q ;
rewrite <- q ;
apply idpath).
Definition id_h_profunctor_square
{C D : category}
(P : D ↛ C)
: profunctor_square (functor_identity C) (functor_identity D) P P.
Show proof.
Definition id_v_profunctor_square
{C D : category}
(F : C ⟶ D)
: profunctor_square F F (id_profunctor C) (id_profunctor D).
Show proof.
{C D : category}
(P : D ↛ C)
: profunctor_square (functor_identity C) (functor_identity D) P P.
Show proof.
use make_profunctor_square.
- exact (λ y x h, h).
- abstract
(intros y₁ y₂ x₁ x₂ g f h ; cbn -[lmap rmap] ;
apply idpath).
- exact (λ y x h, h).
- abstract
(intros y₁ y₂ x₁ x₂ g f h ; cbn -[lmap rmap] ;
apply idpath).
Definition id_v_profunctor_square
{C D : category}
(F : C ⟶ D)
: profunctor_square F F (id_profunctor C) (id_profunctor D).
Show proof.
use make_profunctor_square.
- exact (λ y x h, #F h).
- abstract
(intros y₁ y₂ x₁ x₂ g f h ; cbn -[lmap rmap] ;
rewrite !lmap_id_profunctor, !rmap_id_profunctor ;
rewrite !functor_comp ;
apply idpath).
- exact (λ y x h, #F h).
- abstract
(intros y₁ y₂ x₁ x₂ g f h ; cbn -[lmap rmap] ;
rewrite !lmap_id_profunctor, !rmap_id_profunctor ;
rewrite !functor_comp ;
apply idpath).
Definition comp_h_profunctor_square
{C₁ C₂ C₃ D₁ D₂ D₃ : category}
{F₁ : C₁ ⟶ C₂}
{F₂ : C₂ ⟶ C₃}
{G₁ : D₁ ⟶ D₂}
{G₂ : D₂ ⟶ D₃}
{P₁ : D₁ ↛ C₁}
{P₂ : D₂ ↛ C₂}
{P₃ : D₃ ↛ C₃}
(τ : profunctor_square F₁ G₁ P₁ P₂)
(θ : profunctor_square F₂ G₂ P₂ P₃)
: profunctor_square (F₁ ∙ F₂) (G₁ ∙ G₂) P₁ P₃.
Show proof.
Definition comp_v_profunctor_square_mor
{C₁ C₂ D₁ D₂ E₁ E₂ : category}
{F₁ : C₁ ⟶ C₂}
{F₂ : D₁ ⟶ D₂}
{F₃ : E₁ ⟶ E₂}
{P₁ : C₁ ↛ D₁}
{Q₁ : D₁ ↛ E₁}
{P₂ : C₂ ↛ D₂}
{Q₂ : D₂ ↛ E₂}
(τ : profunctor_square F₂ F₁ P₁ P₂)
(θ : profunctor_square F₃ F₂ Q₁ Q₂)
(z : E₁)
(x : C₁)
: comp_profunctor P₁ Q₁ z x → comp_profunctor P₂ Q₂ (F₃ z) (F₁ x).
Show proof.
Proposition comp_v_profunctor_square_mor_comm
{C₁ C₂ D₁ D₂ E₁ E₂ : category}
{F₁ : C₁ ⟶ C₂}
{F₂ : D₁ ⟶ D₂}
{F₃ : E₁ ⟶ E₂}
{P₁ : C₁ ↛ D₁}
{Q₁ : D₁ ↛ E₁}
{P₂ : C₂ ↛ D₂}
{Q₂ : D₂ ↛ E₂}
(τ : profunctor_square F₂ F₁ P₁ P₂)
(θ : profunctor_square F₃ F₂ Q₁ Q₂)
(z : E₁)
(x : C₁)
(y : D₁)
(h₁ : P₁ y x)
(h₂ : Q₁ z y)
: comp_v_profunctor_square_mor
τ θ z x
(comp_profunctor_ob_in _ _ y h₁ h₂)
=
comp_profunctor_ob_in P₂ Q₂ (F₂ y) (τ y x h₁) (θ z y h₂).
Show proof.
Proposition comp_v_profunctor_square_laws
{C₁ C₂ D₁ D₂ E₁ E₂ : category}
{F₁ : C₁ ⟶ C₂}
{F₂ : D₁ ⟶ D₂}
{F₃ : E₁ ⟶ E₂}
{P₁ : C₁ ↛ D₁}
{Q₁ : D₁ ↛ E₁}
{P₂ : C₂ ↛ D₂}
{Q₂ : D₂ ↛ E₂}
(τ : profunctor_square F₂ F₁ P₁ P₂)
(θ : profunctor_square F₃ F₂ Q₁ Q₂)
: profunctor_square_laws (comp_v_profunctor_square_mor τ θ).
Show proof.
Definition comp_v_profunctor_square
{C₁ C₂ D₁ D₂ E₁ E₂ : category}
{F₁ : C₁ ⟶ C₂}
{F₂ : D₁ ⟶ D₂}
{F₃ : E₁ ⟶ E₂}
{P₁ : C₁ ↛ D₁}
{Q₁ : D₁ ↛ E₁}
{P₂ : C₂ ↛ D₂}
{Q₂ : D₂ ↛ E₂}
(τ : profunctor_square F₂ F₁ P₁ P₂)
(θ : profunctor_square F₃ F₂ Q₁ Q₂)
: profunctor_square F₃ F₁ (comp_profunctor P₁ Q₁) (comp_profunctor P₂ Q₂).
Show proof.
{C₁ C₂ C₃ D₁ D₂ D₃ : category}
{F₁ : C₁ ⟶ C₂}
{F₂ : C₂ ⟶ C₃}
{G₁ : D₁ ⟶ D₂}
{G₂ : D₂ ⟶ D₃}
{P₁ : D₁ ↛ C₁}
{P₂ : D₂ ↛ C₂}
{P₃ : D₃ ↛ C₃}
(τ : profunctor_square F₁ G₁ P₁ P₂)
(θ : profunctor_square F₂ G₂ P₂ P₃)
: profunctor_square (F₁ ∙ F₂) (G₁ ∙ G₂) P₁ P₃.
Show proof.
use make_profunctor_square.
- exact (λ y x h, θ (F₁ y) (G₁ x) (τ y x h)).
- abstract
(intros y₁ y₂ x₁ x₂ g f h ; cbn -[lmap rmap] ;
rewrite (profunctor_square_lmap_rmap τ) ;
rewrite (profunctor_square_lmap_rmap θ) ;
apply idpath).
- exact (λ y x h, θ (F₁ y) (G₁ x) (τ y x h)).
- abstract
(intros y₁ y₂ x₁ x₂ g f h ; cbn -[lmap rmap] ;
rewrite (profunctor_square_lmap_rmap τ) ;
rewrite (profunctor_square_lmap_rmap θ) ;
apply idpath).
Definition comp_v_profunctor_square_mor
{C₁ C₂ D₁ D₂ E₁ E₂ : category}
{F₁ : C₁ ⟶ C₂}
{F₂ : D₁ ⟶ D₂}
{F₃ : E₁ ⟶ E₂}
{P₁ : C₁ ↛ D₁}
{Q₁ : D₁ ↛ E₁}
{P₂ : C₂ ↛ D₂}
{Q₂ : D₂ ↛ E₂}
(τ : profunctor_square F₂ F₁ P₁ P₂)
(θ : profunctor_square F₃ F₂ Q₁ Q₂)
(z : E₁)
(x : C₁)
: comp_profunctor P₁ Q₁ z x → comp_profunctor P₂ Q₂ (F₃ z) (F₁ x).
Show proof.
use from_comp_profunctor_ob.
- exact (λ y h h', comp_profunctor_ob_in P₂ Q₂ (F₂ y) (τ y x h) (θ z y h')).
- abstract
(intros y₁ y₂ g h h' ; cbn ;
rewrite (profunctor_square_rmap θ) ;
rewrite (profunctor_square_lmap τ) ;
rewrite comp_profunctor_ob_in_comm ;
apply idpath).
- exact (λ y h h', comp_profunctor_ob_in P₂ Q₂ (F₂ y) (τ y x h) (θ z y h')).
- abstract
(intros y₁ y₂ g h h' ; cbn ;
rewrite (profunctor_square_rmap θ) ;
rewrite (profunctor_square_lmap τ) ;
rewrite comp_profunctor_ob_in_comm ;
apply idpath).
Proposition comp_v_profunctor_square_mor_comm
{C₁ C₂ D₁ D₂ E₁ E₂ : category}
{F₁ : C₁ ⟶ C₂}
{F₂ : D₁ ⟶ D₂}
{F₃ : E₁ ⟶ E₂}
{P₁ : C₁ ↛ D₁}
{Q₁ : D₁ ↛ E₁}
{P₂ : C₂ ↛ D₂}
{Q₂ : D₂ ↛ E₂}
(τ : profunctor_square F₂ F₁ P₁ P₂)
(θ : profunctor_square F₃ F₂ Q₁ Q₂)
(z : E₁)
(x : C₁)
(y : D₁)
(h₁ : P₁ y x)
(h₂ : Q₁ z y)
: comp_v_profunctor_square_mor
τ θ z x
(comp_profunctor_ob_in _ _ y h₁ h₂)
=
comp_profunctor_ob_in P₂ Q₂ (F₂ y) (τ y x h₁) (θ z y h₂).
Show proof.
Proposition comp_v_profunctor_square_laws
{C₁ C₂ D₁ D₂ E₁ E₂ : category}
{F₁ : C₁ ⟶ C₂}
{F₂ : D₁ ⟶ D₂}
{F₃ : E₁ ⟶ E₂}
{P₁ : C₁ ↛ D₁}
{Q₁ : D₁ ↛ E₁}
{P₂ : C₂ ↛ D₂}
{Q₂ : D₂ ↛ E₂}
(τ : profunctor_square F₂ F₁ P₁ P₂)
(θ : profunctor_square F₃ F₂ Q₁ Q₂)
: profunctor_square_laws (comp_v_profunctor_square_mor τ θ).
Show proof.
intros z₁ z₂ x₁ x₂ k f h.
cbn.
use (mor_from_comp_profunctor_ob_eq
P₁ Q₁
z₁ x₁
(λ h,
comp_v_profunctor_square_mor
τ θ z₂ x₂
(comp_profunctor_mor
P₁ Q₁ k (identity x₂)
(comp_profunctor_mor
P₁ Q₁ (identity z₁) f
h)))
(λ h,
comp_profunctor_mor
P₂ Q₂ (# F₃ k) (identity (F₁ x₂))
(comp_profunctor_mor
P₂ Q₂ (identity (F₃ z₁)) (# F₁ f)
(comp_v_profunctor_square_mor
τ θ z₁ x₁
h)))).
clear h.
intros y h h'.
cbn.
rewrite !comp_profunctor_mor_comm.
etrans.
{
exact (comp_v_profunctor_square_mor_comm τ θ z₂ x₂ y _ _).
}
refine (!_).
etrans.
{
do 2 apply maponpaths.
exact (comp_v_profunctor_square_mor_comm τ θ z₁ x₁ y _ _).
}
rewrite !comp_profunctor_mor_comm.
rewrite !lmap_id.
rewrite !rmap_id.
rewrite (profunctor_square_lmap θ).
rewrite (profunctor_square_rmap τ).
apply idpath.
cbn.
use (mor_from_comp_profunctor_ob_eq
P₁ Q₁
z₁ x₁
(λ h,
comp_v_profunctor_square_mor
τ θ z₂ x₂
(comp_profunctor_mor
P₁ Q₁ k (identity x₂)
(comp_profunctor_mor
P₁ Q₁ (identity z₁) f
h)))
(λ h,
comp_profunctor_mor
P₂ Q₂ (# F₃ k) (identity (F₁ x₂))
(comp_profunctor_mor
P₂ Q₂ (identity (F₃ z₁)) (# F₁ f)
(comp_v_profunctor_square_mor
τ θ z₁ x₁
h)))).
clear h.
intros y h h'.
cbn.
rewrite !comp_profunctor_mor_comm.
etrans.
{
exact (comp_v_profunctor_square_mor_comm τ θ z₂ x₂ y _ _).
}
refine (!_).
etrans.
{
do 2 apply maponpaths.
exact (comp_v_profunctor_square_mor_comm τ θ z₁ x₁ y _ _).
}
rewrite !comp_profunctor_mor_comm.
rewrite !lmap_id.
rewrite !rmap_id.
rewrite (profunctor_square_lmap θ).
rewrite (profunctor_square_rmap τ).
apply idpath.
Definition comp_v_profunctor_square
{C₁ C₂ D₁ D₂ E₁ E₂ : category}
{F₁ : C₁ ⟶ C₂}
{F₂ : D₁ ⟶ D₂}
{F₃ : E₁ ⟶ E₂}
{P₁ : C₁ ↛ D₁}
{Q₁ : D₁ ↛ E₁}
{P₂ : C₂ ↛ D₂}
{Q₂ : D₂ ↛ E₂}
(τ : profunctor_square F₂ F₁ P₁ P₂)
(θ : profunctor_square F₃ F₂ Q₁ Q₂)
: profunctor_square F₃ F₁ (comp_profunctor P₁ Q₁) (comp_profunctor P₂ Q₂).
Show proof.
use make_profunctor_square.
- exact (λ z x, comp_v_profunctor_square_mor τ θ z x).
- exact (comp_v_profunctor_square_laws τ θ).
- exact (λ z x, comp_v_profunctor_square_mor τ θ z x).
- exact (comp_v_profunctor_square_laws τ θ).
Definition dwhisker_profunctor_square
{C₁ C₂ D₁ D₂ : category}
{F F' : C₁ ⟶ C₂}
{G : D₁ ⟶ D₂}
{P : D₁ ↛ C₁}
{Q : D₂ ↛ C₂}
(τ : F ⟹ F')
(θ : profunctor_square F' G P Q)
: profunctor_square F G P Q.
Show proof.
Definition uwhisker_profunctor_square
{C₁ C₂ D₁ D₂ : category}
{F : C₁ ⟶ C₂}
{G G' : D₁ ⟶ D₂}
{P : D₁ ↛ C₁}
{Q : D₂ ↛ C₂}
(τ : G ⟹ G')
(θ : profunctor_square F G P Q)
: profunctor_square F G' P Q.
Show proof.
Definition lwhisker_profunctor_square
{C₁ C₂ D₁ D₂ : category}
{F : C₁ ⟶ C₂}
{G : D₁ ⟶ D₂}
{P P' : D₁ ↛ C₁}
{Q : D₂ ↛ C₂}
(τ : profunctor_nat_trans P P')
(θ : profunctor_square F G P' Q)
: profunctor_square F G P Q.
Show proof.
Definition rwhisker_profunctor_square
{C₁ C₂ D₁ D₂ : category}
{F : C₁ ⟶ C₂}
{G : D₁ ⟶ D₂}
{P : D₁ ↛ C₁}
{Q Q' : D₂ ↛ C₂}
(τ : profunctor_nat_trans Q Q')
(θ : profunctor_square F G P Q)
: profunctor_square F G P Q'.
Show proof.
{C₁ C₂ D₁ D₂ : category}
{F F' : C₁ ⟶ C₂}
{G : D₁ ⟶ D₂}
{P : D₁ ↛ C₁}
{Q : D₂ ↛ C₂}
(τ : F ⟹ F')
(θ : profunctor_square F' G P Q)
: profunctor_square F G P Q.
Show proof.
use make_profunctor_square.
- exact (λ y x h, lmap Q (τ y) (θ y x h)).
- abstract
(intros y₁ y₂ x₁ x₂ g f h ; cbn -[lmap rmap] ;
rewrite (profunctor_square_lmap_rmap θ) ;
rewrite <- lmap_rmap ;
rewrite <- !lmap_comp ;
rewrite (nat_trans_ax τ _ _ g) ;
apply idpath).
- exact (λ y x h, lmap Q (τ y) (θ y x h)).
- abstract
(intros y₁ y₂ x₁ x₂ g f h ; cbn -[lmap rmap] ;
rewrite (profunctor_square_lmap_rmap θ) ;
rewrite <- lmap_rmap ;
rewrite <- !lmap_comp ;
rewrite (nat_trans_ax τ _ _ g) ;
apply idpath).
Definition uwhisker_profunctor_square
{C₁ C₂ D₁ D₂ : category}
{F : C₁ ⟶ C₂}
{G G' : D₁ ⟶ D₂}
{P : D₁ ↛ C₁}
{Q : D₂ ↛ C₂}
(τ : G ⟹ G')
(θ : profunctor_square F G P Q)
: profunctor_square F G' P Q.
Show proof.
use make_profunctor_square.
- exact (λ y x h, rmap Q (τ x) (θ y x h)).
- abstract
(intros y₁ y₂ x₁ x₂ g f h ; cbn -[lmap rmap] ;
rewrite (profunctor_square_lmap_rmap θ) ;
rewrite <- lmap_rmap ;
apply maponpaths ;
rewrite <- !rmap_comp ;
rewrite (nat_trans_ax τ _ _ f) ;
apply idpath).
- exact (λ y x h, rmap Q (τ x) (θ y x h)).
- abstract
(intros y₁ y₂ x₁ x₂ g f h ; cbn -[lmap rmap] ;
rewrite (profunctor_square_lmap_rmap θ) ;
rewrite <- lmap_rmap ;
apply maponpaths ;
rewrite <- !rmap_comp ;
rewrite (nat_trans_ax τ _ _ f) ;
apply idpath).
Definition lwhisker_profunctor_square
{C₁ C₂ D₁ D₂ : category}
{F : C₁ ⟶ C₂}
{G : D₁ ⟶ D₂}
{P P' : D₁ ↛ C₁}
{Q : D₂ ↛ C₂}
(τ : profunctor_nat_trans P P')
(θ : profunctor_square F G P' Q)
: profunctor_square F G P Q.
Show proof.
use make_profunctor_square.
- exact (λ y x h, θ y x (τ y x h)).
- abstract
(intros y₁ y₂ x₁ x₂ g f h ; cbn -[lmap rmap] ;
rewrite profunctor_nat_trans_lmap_rmap ;
rewrite profunctor_square_lmap_rmap ;
apply idpath).
- exact (λ y x h, θ y x (τ y x h)).
- abstract
(intros y₁ y₂ x₁ x₂ g f h ; cbn -[lmap rmap] ;
rewrite profunctor_nat_trans_lmap_rmap ;
rewrite profunctor_square_lmap_rmap ;
apply idpath).
Definition rwhisker_profunctor_square
{C₁ C₂ D₁ D₂ : category}
{F : C₁ ⟶ C₂}
{G : D₁ ⟶ D₂}
{P : D₁ ↛ C₁}
{Q Q' : D₂ ↛ C₂}
(τ : profunctor_nat_trans Q Q')
(θ : profunctor_square F G P Q)
: profunctor_square F G P Q'.
Show proof.
use make_profunctor_square.
- exact (λ y x h, τ (F y) (G x) (θ y x h)).
- abstract
(intros y₁ y₂ x₁ x₂ g f h ; cbn -[lmap rmap] ;
rewrite profunctor_square_lmap_rmap ;
rewrite profunctor_nat_trans_lmap_rmap ;
apply idpath).
- exact (λ y x h, τ (F y) (G x) (θ y x h)).
- abstract
(intros y₁ y₂ x₁ x₂ g f h ; cbn -[lmap rmap] ;
rewrite profunctor_square_lmap_rmap ;
rewrite profunctor_nat_trans_lmap_rmap ;
apply idpath).
Definition lunitor_profunctor_square
{C₁ C₂ : category}
(P : C₁ ↛ C₂)
: profunctor_square
(functor_identity C₂)
(functor_identity C₁)
(comp_profunctor (id_profunctor C₁) P)
P.
Show proof.
Definition runitor_profunctor_square
{C₁ C₂ : category}
(P : C₁ ↛ C₂)
: profunctor_square
(functor_identity C₂)
(functor_identity C₁)
(comp_profunctor P (id_profunctor C₂))
P.
Show proof.
Definition associator_profunctor_square
{C₁ C₂ C₃ C₄ : category}
(P₁ : C₁ ↛ C₂)
(P₂ : C₂ ↛ C₃)
(P₃ : C₃ ↛ C₄)
: profunctor_square
(functor_identity C₄)
(functor_identity C₁)
(comp_profunctor P₁ (comp_profunctor P₂ P₃))
(comp_profunctor (comp_profunctor P₁ P₂) P₃).
Show proof.
{C₁ C₂ : category}
(P : C₁ ↛ C₂)
: profunctor_square
(functor_identity C₂)
(functor_identity C₁)
(comp_profunctor (id_profunctor C₁) P)
P.
Show proof.
Definition runitor_profunctor_square
{C₁ C₂ : category}
(P : C₁ ↛ C₂)
: profunctor_square
(functor_identity C₂)
(functor_identity C₁)
(comp_profunctor P (id_profunctor C₂))
P.
Show proof.
Definition associator_profunctor_square
{C₁ C₂ C₃ C₄ : category}
(P₁ : C₁ ↛ C₂)
(P₂ : C₂ ↛ C₃)
(P₃ : C₃ ↛ C₄)
: profunctor_square
(functor_identity C₄)
(functor_identity C₁)
(comp_profunctor P₁ (comp_profunctor P₂ P₃))
(comp_profunctor (comp_profunctor P₁ P₂) P₃).
Show proof.
Definition representable_profunctor_left_unit
{C₁ C₂ : category}
(F : C₁ ⟶ C₂)
: profunctor_square
(functor_identity C₂)
F
(representable_profunctor_left F)
(id_profunctor C₂).
Show proof.
Definition representable_profunctor_left_counit
{C₁ C₂ : category}
(F : C₁ ⟶ C₂)
: profunctor_square
F
(functor_identity C₁)
(id_profunctor C₁)
(representable_profunctor_left F).
Show proof.
{C₁ C₂ : category}
(F : C₁ ⟶ C₂)
: profunctor_square
(functor_identity C₂)
F
(representable_profunctor_left F)
(id_profunctor C₂).
Show proof.
use make_profunctor_square.
- exact (λ y x f, f).
- abstract
(intros y₁ y₂ x₁ x₂ g f h ; cbn in * ;
rewrite functor_id ;
rewrite !id_left, !id_right ;
apply idpath).
- exact (λ y x f, f).
- abstract
(intros y₁ y₂ x₁ x₂ g f h ; cbn in * ;
rewrite functor_id ;
rewrite !id_left, !id_right ;
apply idpath).
Definition representable_profunctor_left_counit
{C₁ C₂ : category}
(F : C₁ ⟶ C₂)
: profunctor_square
F
(functor_identity C₁)
(id_profunctor C₁)
(representable_profunctor_left F).
Show proof.
use make_profunctor_square.
- exact (λ y x f, #F f).
- abstract
(intros y₁ y₂ x₁ x₂ g f h ; cbn in * ;
rewrite functor_id ;
rewrite !id_left, !id_right ;
rewrite !functor_comp ;
apply idpath).
- exact (λ y x f, #F f).
- abstract
(intros y₁ y₂ x₁ x₂ g f h ; cbn in * ;
rewrite functor_id ;
rewrite !id_left, !id_right ;
rewrite !functor_comp ;
apply idpath).
Definition representable_profunctor_right_unit
{C₁ C₂ : category}
(F : C₁ ⟶ C₂)
: profunctor_square
(functor_identity C₁)
F
(id_profunctor C₁)
(representable_profunctor_right F).
Show proof.
Definition representable_profunctor_right_counit
{C₁ C₂ : category}
(F : C₁ ⟶ C₂)
: profunctor_square
F
(functor_identity C₂)
(representable_profunctor_right F)
(id_profunctor C₂).
Show proof.
{C₁ C₂ : category}
(F : C₁ ⟶ C₂)
: profunctor_square
(functor_identity C₁)
F
(id_profunctor C₁)
(representable_profunctor_right F).
Show proof.
use make_profunctor_square.
- exact (λ y x f, #F f).
- abstract
(intros y₁ y₂ x₁ x₂ g f h ; cbn in * ;
rewrite functor_id ;
rewrite !id_left, !id_right ;
rewrite !functor_comp ;
apply idpath).
- exact (λ y x f, #F f).
- abstract
(intros y₁ y₂ x₁ x₂ g f h ; cbn in * ;
rewrite functor_id ;
rewrite !id_left, !id_right ;
rewrite !functor_comp ;
apply idpath).
Definition representable_profunctor_right_counit
{C₁ C₂ : category}
(F : C₁ ⟶ C₂)
: profunctor_square
F
(functor_identity C₂)
(representable_profunctor_right F)
(id_profunctor C₂).
Show proof.