Library UniMath.Bicategories.Objects.CartesianObject
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.Core.Univalence.
Require Import UniMath.CategoryTheory.limits.terminal.
Require Import UniMath.CategoryTheory.limits.initial.
Require Import UniMath.CategoryTheory.limits.binproducts.
Require Import UniMath.CategoryTheory.limits.bincoproducts.
Require Import UniMath.CategoryTheory.limits.Preservation.
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.Core.Unitors.
Require Import UniMath.Bicategories.Core.Univalence.
Require Import UniMath.Bicategories.Core.AdjointUnique.
Require Import UniMath.Bicategories.Core.UnivalenceOp.
Require Import UniMath.Bicategories.Morphisms.Adjunctions.
Require Import UniMath.Bicategories.Limits.Final.
Require Import UniMath.Bicategories.Limits.Products.
Local Open Scope cat.
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.Core.Univalence.
Require Import UniMath.CategoryTheory.limits.terminal.
Require Import UniMath.CategoryTheory.limits.initial.
Require Import UniMath.CategoryTheory.limits.binproducts.
Require Import UniMath.CategoryTheory.limits.bincoproducts.
Require Import UniMath.CategoryTheory.limits.Preservation.
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.Core.Unitors.
Require Import UniMath.Bicategories.Core.Univalence.
Require Import UniMath.Bicategories.Core.AdjointUnique.
Require Import UniMath.Bicategories.Core.UnivalenceOp.
Require Import UniMath.Bicategories.Morphisms.Adjunctions.
Require Import UniMath.Bicategories.Limits.Final.
Require Import UniMath.Bicategories.Limits.Products.
Local Open Scope cat.
1. The representable definition of cartesian objects
Definition cartesian_terminal
{B : bicat}
(b : B)
: UU
:= (∏ (x : B), Terminal (hom x b))
×
(∏ (x y : B) (f : x --> y), preserves_terminal (pre_comp b f)).
Definition cartesian_prod
{B : bicat}
(b : B)
: UU
:= (∏ (x : B), BinProducts (hom x b))
×
(∏ (x y : B) (f : x --> y), preserves_binproduct (pre_comp b f)).
Definition cartesian_ob
{B : bicat}
(b : B)
: UU
:= cartesian_terminal b × cartesian_prod b.
{B : bicat}
(b : B)
: UU
:= (∏ (x : B), Terminal (hom x b))
×
(∏ (x y : B) (f : x --> y), preserves_terminal (pre_comp b f)).
Definition cartesian_prod
{B : bicat}
(b : B)
: UU
:= (∏ (x : B), BinProducts (hom x b))
×
(∏ (x y : B) (f : x --> y), preserves_binproduct (pre_comp b f)).
Definition cartesian_ob
{B : bicat}
(b : B)
: UU
:= cartesian_terminal b × cartesian_prod b.
2. Being cartesian is a proposition
Definition isaprop_cartesian_terminal
{B : bicat}
(HB : is_univalent_2_1 B)
(b : B)
: isaprop (cartesian_terminal b).
Show proof.
Definition isaprop_cartesian_prod
{B : bicat}
(HB : is_univalent_2_1 B)
(b : B)
: isaprop (cartesian_prod b).
Show proof.
Definition isaprop_cartesian_ob
{B : bicat}
(HB : is_univalent_2_1 B)
(b : B)
: isaprop (cartesian_ob b).
Show proof.
{B : bicat}
(HB : is_univalent_2_1 B)
(b : B)
: isaprop (cartesian_terminal b).
Show proof.
use isapropdirprod.
- use impred ; intro.
apply isaprop_Terminal.
apply is_univ_hom.
exact HB.
- do 3 (use impred ; intro).
apply isaprop_preserves_terminal.
- use impred ; intro.
apply isaprop_Terminal.
apply is_univ_hom.
exact HB.
- do 3 (use impred ; intro).
apply isaprop_preserves_terminal.
Definition isaprop_cartesian_prod
{B : bicat}
(HB : is_univalent_2_1 B)
(b : B)
: isaprop (cartesian_prod b).
Show proof.
use isapropdirprod.
- do 3 (use impred ; intro).
apply isaprop_BinProduct.
apply is_univ_hom.
exact HB.
- do 3 (use impred ; intro).
apply isaprop_preserves_binproduct.
- do 3 (use impred ; intro).
apply isaprop_BinProduct.
apply is_univ_hom.
exact HB.
- do 3 (use impred ; intro).
apply isaprop_preserves_binproduct.
Definition isaprop_cartesian_ob
{B : bicat}
(HB : is_univalent_2_1 B)
(b : B)
: isaprop (cartesian_ob b).
Show proof.
use isapropdirprod.
- apply isaprop_cartesian_terminal.
exact HB.
- apply isaprop_cartesian_prod.
exact HB.
- apply isaprop_cartesian_terminal.
exact HB.
- apply isaprop_cartesian_prod.
exact HB.
3. The definitions of cartesian objects via adjunctions
Section CartesianViaAdjunction.
Context {B : bicat}
(b : B).
Section Terminal.
Context (T : bifinal_obj B).
Let f : b --> pr1 T
:= is_bifinal_1cell_property (pr2 T) b.
Definition cartesian_terminal_via_adj
: UU
:= left_adjoint f.
Definition isaprop_cartesian_terminal_via_adj
(HB : is_univalent_2_1 B)
: isaprop cartesian_terminal_via_adj.
Show proof.
End Terminal.
Section Prod.
Context (prod : has_binprod B).
Let δ : b --> pr1 (prod b b)
:= binprod_ump_1cell (pr2 (prod b b)) (id₁ b) (id₁ b).
Definition cartesian_prod_via_adj
: UU
:= left_adjoint δ.
Definition isaprop_cartesian_prod_via_adj
(HB : is_univalent_2_1 B)
: isaprop cartesian_prod_via_adj.
Show proof.
End Prod.
Section Cartesian.
Context (T : bifinal_obj B)
(prod : has_binprod B).
Definition cartesian_ob_via_adj
: UU
:= cartesian_terminal_via_adj T × cartesian_prod_via_adj prod.
Definition isaprop_cartesian_ob_via_adj
(HB : is_univalent_2_1 B)
: isaprop cartesian_ob_via_adj.
Show proof.
End CartesianViaAdjunction.
Context {B : bicat}
(b : B).
Section Terminal.
Context (T : bifinal_obj B).
Let f : b --> pr1 T
:= is_bifinal_1cell_property (pr2 T) b.
Definition cartesian_terminal_via_adj
: UU
:= left_adjoint f.
Definition isaprop_cartesian_terminal_via_adj
(HB : is_univalent_2_1 B)
: isaprop cartesian_terminal_via_adj.
Show proof.
End Terminal.
Section Prod.
Context (prod : has_binprod B).
Let δ : b --> pr1 (prod b b)
:= binprod_ump_1cell (pr2 (prod b b)) (id₁ b) (id₁ b).
Definition cartesian_prod_via_adj
: UU
:= left_adjoint δ.
Definition isaprop_cartesian_prod_via_adj
(HB : is_univalent_2_1 B)
: isaprop cartesian_prod_via_adj.
Show proof.
End Prod.
Section Cartesian.
Context (T : bifinal_obj B)
(prod : has_binprod B).
Definition cartesian_ob_via_adj
: UU
:= cartesian_terminal_via_adj T × cartesian_prod_via_adj prod.
Definition isaprop_cartesian_ob_via_adj
(HB : is_univalent_2_1 B)
: isaprop cartesian_ob_via_adj.
Show proof.
apply isapropdirprod.
- apply isaprop_cartesian_terminal_via_adj.
exact HB.
- apply isaprop_cartesian_prod_via_adj.
exact HB.
End Cartesian.- apply isaprop_cartesian_terminal_via_adj.
exact HB.
- apply isaprop_cartesian_prod_via_adj.
exact HB.
End CartesianViaAdjunction.
4. Equivalence of the two definitions of cartesian object
Section EquivalenceCartesian.
Context {B : bicat}
(T : bifinal_obj B)
(prod : has_binprod B)
(b : B).
Section ToAdj.
Context (Hb : cartesian_terminal b).
Let term : Terminal (hom (pr1 T) b) := pr1 Hb (pr1 T).
Let l : b --> pr1 T := is_bifinal_1cell_property (pr2 T) b.
Let r : pr1 T --> b := pr1 term.
Local Definition cartesian_terminal_to_cartesian_terminal_via_adj_unit
: id₁ b ==> l · r
:= TerminalArrow (_ ,, pr2 Hb _ _ l _ (pr2 term)) (id₁ b).
Let η : id₁ b ==> l · r
:= cartesian_terminal_to_cartesian_terminal_via_adj_unit.
Local Definition cartesian_terminal_to_cartesian_terminal_via_adj_counit
: r · l ==> id₁ (pr1 T)
:= is_bifinal_2cell_property (pr2 T) (pr1 T) (r · l) (id₁ (pr1 T)).
Let ε : r · l ==> id₁ (pr1 T)
:= cartesian_terminal_to_cartesian_terminal_via_adj_counit.
Definition cartesian_terminal_to_cartesian_terminal_via_adj
: cartesian_terminal_via_adj b T.
Show proof.
Section FromAdj.
Context (Hb : cartesian_terminal_via_adj b T).
Let l : b --> pr1 T := is_bifinal_1cell_property (pr2 T) b.
Let r : pr1 T --> b := left_adjoint_right_adjoint (pr1 Hb).
Let η : id₁ b ==> l · r := left_adjoint_unit (pr1 Hb).
Let ε : r · l ==> id₁ (pr1 T) := left_adjoint_counit (pr1 Hb).
Let p
: rinvunitor r • (r ◃ η) • lassociator r l r • (ε ▹ r) • lunitor r
=
id₂ r
:= internal_triangle2 (pr2 Hb).
Definition cartesian_terminal_via_adj_to_cartesian_terminal_1cell
(x : B)
: x --> b
:= is_bifinal_1cell_property (pr2 T) x · r.
Definition cartesian_terminal_via_adj_to_cartesian_terminal_2cell
(x : B)
(f : x --> b)
: f ==> cartesian_terminal_via_adj_to_cartesian_terminal_1cell x
:= rinvunitor _
• (_ ◃ η)
• lassociator _ _ _
• (is_bifinal_2cell_property (pr2 T) _ _ _ ▹ r).
Definition cartesian_terminal_via_adj_to_cartesian_terminal_eq
(x : B)
(f : x --> b)
: isaprop (f ==> cartesian_terminal_via_adj_to_cartesian_terminal_1cell x).
Show proof.
Definition cartesian_terminal_via_adj_to_cartesian_terminal_obj
(x : B)
: Terminal (hom x b).
Show proof.
Definition cartesian_terminal_via_adj_to_cartesian_terminal_preserves
{x y : B}
(f : x --> y)
: preserves_terminal (pre_comp b f).
Show proof.
Definition cartesian_terminal_via_adj_to_cartesian_terminal
: cartesian_terminal b.
Show proof.
Definition cartesian_terminal_weq_cartesian_terminal_via_adj
(HB : is_univalent_2_1 B)
: cartesian_terminal b ≃ cartesian_terminal_via_adj b T.
Show proof.
Section ToAdj.
Context (Hb : cartesian_prod b).
Let δ : b --> pr1 (prod b b)
:= binprod_ump_1cell (pr2 (prod b b)) (id₁ b) (id₁ b).
Let product
: BinProduct
(hom (pr1 (prod b b)) b)
(binprod_cone_pr1 (pr1 (prod b b)))
(binprod_cone_pr2 (pr1 (prod b b)))
:= pr1 Hb (pr1 (prod b b))
(binprod_cone_pr1 (pr1 (prod b b)))
(binprod_cone_pr2 (pr1 (prod b b))).
Let r : pr1 (prod b b) --> b
:= BinProductObject _ product.
Local Definition cartesian_prod_to_cartesian_prod_via_adj_unit
: id₁ b ==> δ · r.
Show proof.
Let η : id₁ b ==> δ · r
:= cartesian_prod_to_cartesian_prod_via_adj_unit.
Local Definition cartesian_prod_to_cartesian_prod_via_adj_counit
: r · δ ==> id₁ _.
Show proof.
Let ε : r · δ ==> id₁ _
:= cartesian_prod_to_cartesian_prod_via_adj_counit.
Local Lemma cartesian_prod_to_cartesian_prod_via_adj_triangle1
: linvunitor δ • (η ▹ δ) • rassociator δ r δ • (δ ◃ ε) • runitor δ
=
id₂ δ.
Show proof.
Local Lemma cartesian_prod_to_cartesian_prod_via_adj_triangle2
: rinvunitor r • (r ◃ η) • lassociator r δ r • (ε ▹ r) • lunitor r
=
id₂ r.
Show proof.
Definition cartesian_prod_to_cartesian_prod_via_adj
: cartesian_prod_via_adj b prod.
Show proof.
Section FromAdj.
Context (Hb : cartesian_prod_via_adj b prod).
Let δ : b --> pr1 (prod b b)
:= binprod_ump_1cell (pr2 (prod b b)) (id₁ b) (id₁ b).
Let r : pr1 (prod b b) --> b := left_adjoint_right_adjoint (pr1 Hb).
Let η : id₁ b ==> δ · r := left_adjoint_unit (pr1 Hb).
Let ε : r · δ ==> id₁ _ := left_adjoint_counit (pr1 Hb).
Let p
: rinvunitor r • (r ◃ η) • lassociator r δ r • (ε ▹ r) • lunitor r
=
id₂ r
:= internal_triangle2 (pr2 Hb).
Local Definition cartesian_prod_via_adj_to_cartesian_prod_1cell
{x : B}
(f g : x --> b)
: x --> b
:= binprod_ump_1cell (pr2 (prod b b)) f g · r.
Local Definition cartesian_prod_via_adj_to_cartesian_prod_pr1_help
: r ==> binprod_cone_pr1 (pr1 (prod b b))
:= rinvunitor _
• (r ◃ (binprod_ump_1cell_pr1 (pr2 (prod b b)) _ (id₁ b) (id₁ b))^-1)
• lassociator _ _ _
• (ε ▹ _)
• lunitor _.
Local Definition cartesian_prod_via_adj_to_cartesian_prod_pr1
{x : B}
(f g : x --> b)
: cartesian_prod_via_adj_to_cartesian_prod_1cell f g ==> f
:= (_ ◃ cartesian_prod_via_adj_to_cartesian_prod_pr1_help)
• binprod_ump_1cell_pr1 (pr2 (prod b b)) _ f g.
Local Definition cartesian_prod_via_adj_to_cartesian_prod_pr2_help
: r ==> binprod_cone_pr2 (pr1 (prod b b))
:= rinvunitor _
• (r ◃ (binprod_ump_1cell_pr2 (pr2 (prod b b)) _ (id₁ b) (id₁ b))^-1)
• lassociator _ _ _
• (ε ▹ _)
• lunitor _.
Local Definition cartesian_prod_via_adj_to_cartesian_prod_pr2
{x : B}
(f g : x --> b)
: cartesian_prod_via_adj_to_cartesian_prod_1cell f g ==> g
:= (_ ◃ cartesian_prod_via_adj_to_cartesian_prod_pr2_help)
• binprod_ump_1cell_pr2 (pr2 (prod b b)) _ f g.
Local Definition cartesian_prod_via_adj_to_cartesian_prod_2cell
{x : B}
{f g k : x --> b}
(α : k ==> f)
(β : k ==> g)
: k ==> cartesian_prod_via_adj_to_cartesian_prod_1cell f g.
Show proof.
Local Definition cartesian_prod_via_adj_to_cartesian_prod_2cell_pr1
{x : B}
{f g k : x --> b}
(α : k ==> f)
(β : k ==> g)
: cartesian_prod_via_adj_to_cartesian_prod_2cell α β
• cartesian_prod_via_adj_to_cartesian_prod_pr1 f g
=
α.
Show proof.
Local Definition cartesian_prod_via_adj_to_cartesian_prod_2cell_pr2
{x : B}
{f g k : x --> b}
(α : k ==> f)
(β : k ==> g)
: cartesian_prod_via_adj_to_cartesian_prod_2cell α β
• cartesian_prod_via_adj_to_cartesian_prod_pr2 f g
=
β.
Show proof.
Local Definition cartesian_prod_via_adj_to_cartesian_prod_eq
{x : B}
{f g k : x --> b}
(α : k ==> f)
(β : k ==> g)
(φ : ∑ (fg : k ==> cartesian_prod_via_adj_to_cartesian_prod_1cell f g),
fg • cartesian_prod_via_adj_to_cartesian_prod_pr1 f g = α
×
fg • cartesian_prod_via_adj_to_cartesian_prod_pr2 f g = β)
: φ
=
cartesian_prod_via_adj_to_cartesian_prod_2cell α β
,,
cartesian_prod_via_adj_to_cartesian_prod_2cell_pr1 α β
,,
cartesian_prod_via_adj_to_cartesian_prod_2cell_pr2 α β.
Show proof.
Local Definition cartesian_prod_via_adj_to_cartesian_prod_obj
(x : B)
: BinProducts (hom x b).
Show proof.
Local Definition help_inv2cell
{x y : B}
(f : x --> y)
(h₁ h₂ : y --> b)
: invertible_2cell
(f
· BinProductObject
(hom y b)
(cartesian_prod_via_adj_to_cartesian_prod_obj y h₁ h₂))
(BinProductObject
(hom x b)
(cartesian_prod_via_adj_to_cartesian_prod_obj x (f · h₁) (f · h₂))).
Show proof.
Definition cartesian_prod_via_adj_to_cartesian_prod_preserves
{x y : B}
(f : x --> y)
: preserves_binproduct (pre_comp b f).
Show proof.
Definition cartesian_prod_via_adj_to_cartesian_prod
: cartesian_prod b.
Show proof.
Definition cartesian_prod_weq_cartesian_prod_via_adj
(HB : is_univalent_2_1 B)
: cartesian_prod b ≃ cartesian_prod_via_adj b prod.
Show proof.
Definition cartesian_weq_cartesian_via_adj
(HB : is_univalent_2_1 B)
: cartesian_ob b ≃ cartesian_ob_via_adj b T prod.
Show proof.
Context {B : bicat}
(T : bifinal_obj B)
(prod : has_binprod B)
(b : B).
Section ToAdj.
Context (Hb : cartesian_terminal b).
Let term : Terminal (hom (pr1 T) b) := pr1 Hb (pr1 T).
Let l : b --> pr1 T := is_bifinal_1cell_property (pr2 T) b.
Let r : pr1 T --> b := pr1 term.
Local Definition cartesian_terminal_to_cartesian_terminal_via_adj_unit
: id₁ b ==> l · r
:= TerminalArrow (_ ,, pr2 Hb _ _ l _ (pr2 term)) (id₁ b).
Let η : id₁ b ==> l · r
:= cartesian_terminal_to_cartesian_terminal_via_adj_unit.
Local Definition cartesian_terminal_to_cartesian_terminal_via_adj_counit
: r · l ==> id₁ (pr1 T)
:= is_bifinal_2cell_property (pr2 T) (pr1 T) (r · l) (id₁ (pr1 T)).
Let ε : r · l ==> id₁ (pr1 T)
:= cartesian_terminal_to_cartesian_terminal_via_adj_counit.
Definition cartesian_terminal_to_cartesian_terminal_via_adj
: cartesian_terminal_via_adj b T.
Show proof.
simple refine ((_ ,, (_ ,, _)) ,, (_ ,, _)).
- exact r.
- exact η.
- exact ε.
- apply (is_bifinal_eq_property (pr2 T)).
- apply (@TerminalArrowEq _ term).
End ToAdj.- exact r.
- exact η.
- exact ε.
- apply (is_bifinal_eq_property (pr2 T)).
- apply (@TerminalArrowEq _ term).
Section FromAdj.
Context (Hb : cartesian_terminal_via_adj b T).
Let l : b --> pr1 T := is_bifinal_1cell_property (pr2 T) b.
Let r : pr1 T --> b := left_adjoint_right_adjoint (pr1 Hb).
Let η : id₁ b ==> l · r := left_adjoint_unit (pr1 Hb).
Let ε : r · l ==> id₁ (pr1 T) := left_adjoint_counit (pr1 Hb).
Let p
: rinvunitor r • (r ◃ η) • lassociator r l r • (ε ▹ r) • lunitor r
=
id₂ r
:= internal_triangle2 (pr2 Hb).
Definition cartesian_terminal_via_adj_to_cartesian_terminal_1cell
(x : B)
: x --> b
:= is_bifinal_1cell_property (pr2 T) x · r.
Definition cartesian_terminal_via_adj_to_cartesian_terminal_2cell
(x : B)
(f : x --> b)
: f ==> cartesian_terminal_via_adj_to_cartesian_terminal_1cell x
:= rinvunitor _
• (_ ◃ η)
• lassociator _ _ _
• (is_bifinal_2cell_property (pr2 T) _ _ _ ▹ r).
Definition cartesian_terminal_via_adj_to_cartesian_terminal_eq
(x : B)
(f : x --> b)
: isaprop (f ==> cartesian_terminal_via_adj_to_cartesian_terminal_1cell x).
Show proof.
use invproofirrelevance.
intros α β.
refine (!(id2_right _) @ _ @ id2_right _).
unfold cartesian_terminal_via_adj_to_cartesian_terminal_1cell.
rewrite <- lwhisker_id2.
rewrite <- p.
rewrite <- !lwhisker_vcomp.
rewrite !vassocl.
rewrite !left_unit_inv_assoc.
rewrite !vassocr.
rewrite !rinvunitor_natural.
rewrite <- !rwhisker_hcomp.
rewrite !vassocl.
apply maponpaths.
rewrite !(maponpaths (λ z, _ • z) (vassocr _ _ _)).
rewrite !lwhisker_lwhisker_rassociator.
rewrite !vassocr.
rewrite !vcomp_whisker.
rewrite !vassocl.
apply maponpaths.
rewrite !(maponpaths (λ z, _ • z) (vassocr _ _ _)).
rewrite !lwhisker_hcomp.
rewrite inverse_pentagon_4.
rewrite <- !lwhisker_hcomp, <- !rwhisker_hcomp.
rewrite !vassocr.
rewrite <- !rwhisker_rwhisker.
rewrite !vassocl.
apply maponpaths.
rewrite !vassocr.
do 4 apply maponpaths_2.
apply maponpaths.
apply (is_bifinal_eq_property (pr2 T)).
intros α β.
refine (!(id2_right _) @ _ @ id2_right _).
unfold cartesian_terminal_via_adj_to_cartesian_terminal_1cell.
rewrite <- lwhisker_id2.
rewrite <- p.
rewrite <- !lwhisker_vcomp.
rewrite !vassocl.
rewrite !left_unit_inv_assoc.
rewrite !vassocr.
rewrite !rinvunitor_natural.
rewrite <- !rwhisker_hcomp.
rewrite !vassocl.
apply maponpaths.
rewrite !(maponpaths (λ z, _ • z) (vassocr _ _ _)).
rewrite !lwhisker_lwhisker_rassociator.
rewrite !vassocr.
rewrite !vcomp_whisker.
rewrite !vassocl.
apply maponpaths.
rewrite !(maponpaths (λ z, _ • z) (vassocr _ _ _)).
rewrite !lwhisker_hcomp.
rewrite inverse_pentagon_4.
rewrite <- !lwhisker_hcomp, <- !rwhisker_hcomp.
rewrite !vassocr.
rewrite <- !rwhisker_rwhisker.
rewrite !vassocl.
apply maponpaths.
rewrite !vassocr.
do 4 apply maponpaths_2.
apply maponpaths.
apply (is_bifinal_eq_property (pr2 T)).
Definition cartesian_terminal_via_adj_to_cartesian_terminal_obj
(x : B)
: Terminal (hom x b).
Show proof.
use make_Terminal.
- exact (cartesian_terminal_via_adj_to_cartesian_terminal_1cell x).
- intro f.
use iscontraprop1.
+ exact (cartesian_terminal_via_adj_to_cartesian_terminal_eq x f).
+ exact (cartesian_terminal_via_adj_to_cartesian_terminal_2cell x f).
- exact (cartesian_terminal_via_adj_to_cartesian_terminal_1cell x).
- intro f.
use iscontraprop1.
+ exact (cartesian_terminal_via_adj_to_cartesian_terminal_eq x f).
+ exact (cartesian_terminal_via_adj_to_cartesian_terminal_2cell x f).
Definition cartesian_terminal_via_adj_to_cartesian_terminal_preserves
{x y : B}
(f : x --> y)
: preserves_terminal (pre_comp b f).
Show proof.
use preserves_terminal_if_preserves_chosen.
- apply cartesian_terminal_via_adj_to_cartesian_terminal_obj.
- use (iso_to_Terminal
(cartesian_terminal_via_adj_to_cartesian_terminal_obj x)).
use inv2cell_to_z_iso.
refine (comp_of_invertible_2cell
(rwhisker_of_invertible_2cell
_
_)
(rassociator_invertible_2cell _ _ _)).
apply (is_bifinal_invertible_2cell_property (pr2 T)).
- apply cartesian_terminal_via_adj_to_cartesian_terminal_obj.
- use (iso_to_Terminal
(cartesian_terminal_via_adj_to_cartesian_terminal_obj x)).
use inv2cell_to_z_iso.
refine (comp_of_invertible_2cell
(rwhisker_of_invertible_2cell
_
_)
(rassociator_invertible_2cell _ _ _)).
apply (is_bifinal_invertible_2cell_property (pr2 T)).
Definition cartesian_terminal_via_adj_to_cartesian_terminal
: cartesian_terminal b.
Show proof.
split.
- exact cartesian_terminal_via_adj_to_cartesian_terminal_obj.
- exact @cartesian_terminal_via_adj_to_cartesian_terminal_preserves.
End FromAdj.- exact cartesian_terminal_via_adj_to_cartesian_terminal_obj.
- exact @cartesian_terminal_via_adj_to_cartesian_terminal_preserves.
Definition cartesian_terminal_weq_cartesian_terminal_via_adj
(HB : is_univalent_2_1 B)
: cartesian_terminal b ≃ cartesian_terminal_via_adj b T.
Show proof.
use weqimplimpl.
- exact cartesian_terminal_to_cartesian_terminal_via_adj.
- exact cartesian_terminal_via_adj_to_cartesian_terminal.
- apply isaprop_cartesian_terminal.
exact HB.
- apply isaprop_cartesian_terminal_via_adj.
exact HB.
- exact cartesian_terminal_to_cartesian_terminal_via_adj.
- exact cartesian_terminal_via_adj_to_cartesian_terminal.
- apply isaprop_cartesian_terminal.
exact HB.
- apply isaprop_cartesian_terminal_via_adj.
exact HB.
Section ToAdj.
Context (Hb : cartesian_prod b).
Let δ : b --> pr1 (prod b b)
:= binprod_ump_1cell (pr2 (prod b b)) (id₁ b) (id₁ b).
Let product
: BinProduct
(hom (pr1 (prod b b)) b)
(binprod_cone_pr1 (pr1 (prod b b)))
(binprod_cone_pr2 (pr1 (prod b b)))
:= pr1 Hb (pr1 (prod b b))
(binprod_cone_pr1 (pr1 (prod b b)))
(binprod_cone_pr2 (pr1 (prod b b))).
Let r : pr1 (prod b b) --> b
:= BinProductObject _ product.
Local Definition cartesian_prod_to_cartesian_prod_via_adj_unit
: id₁ b ==> δ · r.
Show proof.
use (BinProductArrow
_
(make_BinProduct
_ _ _ _ _ _
(pr2 Hb _ _ δ _ _ _ _ _ (pr2 product)))).
- exact ((binprod_ump_1cell_pr1 (pr2 (prod b b)) _ (id₁ b) (id₁ b))^-1).
- exact ((binprod_ump_1cell_pr2 (pr2 (prod b b)) _ (id₁ b) (id₁ b))^-1).
_
(make_BinProduct
_ _ _ _ _ _
(pr2 Hb _ _ δ _ _ _ _ _ (pr2 product)))).
- exact ((binprod_ump_1cell_pr1 (pr2 (prod b b)) _ (id₁ b) (id₁ b))^-1).
- exact ((binprod_ump_1cell_pr2 (pr2 (prod b b)) _ (id₁ b) (id₁ b))^-1).
Let η : id₁ b ==> δ · r
:= cartesian_prod_to_cartesian_prod_via_adj_unit.
Local Definition cartesian_prod_to_cartesian_prod_via_adj_counit
: r · δ ==> id₁ _.
Show proof.
use (binprod_ump_2cell (pr2 (prod b b))).
- exact (rassociator _ _ _
• (r ◃ binprod_ump_1cell_pr1 (pr2 (prod b b)) _ (id₁ b) (id₁ b))
• runitor _
• BinProductPr1 _ product
• linvunitor _).
- exact (rassociator _ _ _
• (r ◃ binprod_ump_1cell_pr2 (pr2 (prod b b)) _ (id₁ b) (id₁ b))
• runitor _
• BinProductPr2 _ product
• linvunitor _).
- exact (rassociator _ _ _
• (r ◃ binprod_ump_1cell_pr1 (pr2 (prod b b)) _ (id₁ b) (id₁ b))
• runitor _
• BinProductPr1 _ product
• linvunitor _).
- exact (rassociator _ _ _
• (r ◃ binprod_ump_1cell_pr2 (pr2 (prod b b)) _ (id₁ b) (id₁ b))
• runitor _
• BinProductPr2 _ product
• linvunitor _).
Let ε : r · δ ==> id₁ _
:= cartesian_prod_to_cartesian_prod_via_adj_counit.
Local Lemma cartesian_prod_to_cartesian_prod_via_adj_triangle1
: linvunitor δ • (η ▹ δ) • rassociator δ r δ • (δ ◃ ε) • runitor δ
=
id₂ δ.
Show proof.
use (binprod_ump_2cell_unique_alt (pr2 (prod b b))).
- rewrite id2_rwhisker.
rewrite <- !rwhisker_vcomp.
rewrite <- lunitor_lwhisker.
rewrite !vassocl.
etrans.
{
do 3 apply maponpaths.
rewrite !vassocr.
rewrite <- rwhisker_lwhisker_rassociator.
rewrite !vassocl.
rewrite lwhisker_vcomp.
do 2 apply maponpaths.
etrans.
{
apply maponpaths_2.
apply binprod_ump_2cell_pr1.
}
rewrite !vassocl.
rewrite linvunitor_lunitor.
rewrite id2_right.
apply idpath.
}
rewrite <- !lwhisker_vcomp.
etrans.
{
do 2 apply maponpaths.
rewrite !vassocr.
rewrite rassociator_rassociator.
rewrite !vassocl.
apply idpath.
}
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite rwhisker_rwhisker_alt.
rewrite !vassocl.
apply maponpaths.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite lwhisker_lwhisker_rassociator.
rewrite !vassocl.
apply idpath.
}
rewrite !vassocr.
rewrite vcomp_whisker.
rewrite !vassocl.
apply maponpaths.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite runitor_triangle.
apply idpath.
}
rewrite !vassocr.
rewrite vcomp_runitor.
rewrite !vassocl.
apply maponpaths.
apply (BinProductPr1Commutes
_ _ _
(make_BinProduct
_ _ _ _ _ _
(pr2 Hb _ _ δ _ _ _ _ _ (pr2 product)))).
}
etrans.
{
rewrite !vassocr.
rewrite <- linvunitor_assoc.
rewrite lwhisker_hcomp.
rewrite <- linvunitor_natural.
rewrite !vassocl.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite runitor_lunitor_identity.
rewrite linvunitor_lunitor.
apply id2_left.
}
apply vcomp_rinv.
}
apply idpath.
- rewrite id2_rwhisker.
rewrite <- !rwhisker_vcomp.
rewrite <- lunitor_lwhisker.
rewrite !vassocl.
etrans.
{
do 3 apply maponpaths.
rewrite !vassocr.
rewrite <- rwhisker_lwhisker_rassociator.
rewrite !vassocl.
rewrite lwhisker_vcomp.
do 2 apply maponpaths.
etrans.
{
apply maponpaths_2.
apply binprod_ump_2cell_pr2.
}
rewrite !vassocl.
rewrite linvunitor_lunitor.
rewrite id2_right.
apply idpath.
}
rewrite <- !lwhisker_vcomp.
etrans.
{
do 2 apply maponpaths.
rewrite !vassocr.
rewrite rassociator_rassociator.
rewrite !vassocl.
apply idpath.
}
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite rwhisker_rwhisker_alt.
rewrite !vassocl.
apply maponpaths.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite lwhisker_lwhisker_rassociator.
rewrite !vassocl.
apply idpath.
}
rewrite !vassocr.
rewrite vcomp_whisker.
rewrite !vassocl.
apply maponpaths.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite runitor_triangle.
apply idpath.
}
rewrite !vassocr.
rewrite vcomp_runitor.
rewrite !vassocl.
apply maponpaths.
apply (BinProductPr2Commutes
_ _ _
(make_BinProduct
_ _ _ _ _ _
(pr2 Hb _ _ δ _ _ _ _ _ (pr2 product)))).
}
etrans.
{
rewrite !vassocr.
rewrite <- linvunitor_assoc.
rewrite lwhisker_hcomp.
rewrite <- linvunitor_natural.
rewrite !vassocl.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite runitor_lunitor_identity.
rewrite linvunitor_lunitor.
apply id2_left.
}
apply vcomp_rinv.
}
apply idpath.
- rewrite id2_rwhisker.
rewrite <- !rwhisker_vcomp.
rewrite <- lunitor_lwhisker.
rewrite !vassocl.
etrans.
{
do 3 apply maponpaths.
rewrite !vassocr.
rewrite <- rwhisker_lwhisker_rassociator.
rewrite !vassocl.
rewrite lwhisker_vcomp.
do 2 apply maponpaths.
etrans.
{
apply maponpaths_2.
apply binprod_ump_2cell_pr1.
}
rewrite !vassocl.
rewrite linvunitor_lunitor.
rewrite id2_right.
apply idpath.
}
rewrite <- !lwhisker_vcomp.
etrans.
{
do 2 apply maponpaths.
rewrite !vassocr.
rewrite rassociator_rassociator.
rewrite !vassocl.
apply idpath.
}
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite rwhisker_rwhisker_alt.
rewrite !vassocl.
apply maponpaths.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite lwhisker_lwhisker_rassociator.
rewrite !vassocl.
apply idpath.
}
rewrite !vassocr.
rewrite vcomp_whisker.
rewrite !vassocl.
apply maponpaths.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite runitor_triangle.
apply idpath.
}
rewrite !vassocr.
rewrite vcomp_runitor.
rewrite !vassocl.
apply maponpaths.
apply (BinProductPr1Commutes
_ _ _
(make_BinProduct
_ _ _ _ _ _
(pr2 Hb _ _ δ _ _ _ _ _ (pr2 product)))).
}
etrans.
{
rewrite !vassocr.
rewrite <- linvunitor_assoc.
rewrite lwhisker_hcomp.
rewrite <- linvunitor_natural.
rewrite !vassocl.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite runitor_lunitor_identity.
rewrite linvunitor_lunitor.
apply id2_left.
}
apply vcomp_rinv.
}
apply idpath.
- rewrite id2_rwhisker.
rewrite <- !rwhisker_vcomp.
rewrite <- lunitor_lwhisker.
rewrite !vassocl.
etrans.
{
do 3 apply maponpaths.
rewrite !vassocr.
rewrite <- rwhisker_lwhisker_rassociator.
rewrite !vassocl.
rewrite lwhisker_vcomp.
do 2 apply maponpaths.
etrans.
{
apply maponpaths_2.
apply binprod_ump_2cell_pr2.
}
rewrite !vassocl.
rewrite linvunitor_lunitor.
rewrite id2_right.
apply idpath.
}
rewrite <- !lwhisker_vcomp.
etrans.
{
do 2 apply maponpaths.
rewrite !vassocr.
rewrite rassociator_rassociator.
rewrite !vassocl.
apply idpath.
}
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite rwhisker_rwhisker_alt.
rewrite !vassocl.
apply maponpaths.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite lwhisker_lwhisker_rassociator.
rewrite !vassocl.
apply idpath.
}
rewrite !vassocr.
rewrite vcomp_whisker.
rewrite !vassocl.
apply maponpaths.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite runitor_triangle.
apply idpath.
}
rewrite !vassocr.
rewrite vcomp_runitor.
rewrite !vassocl.
apply maponpaths.
apply (BinProductPr2Commutes
_ _ _
(make_BinProduct
_ _ _ _ _ _
(pr2 Hb _ _ δ _ _ _ _ _ (pr2 product)))).
}
etrans.
{
rewrite !vassocr.
rewrite <- linvunitor_assoc.
rewrite lwhisker_hcomp.
rewrite <- linvunitor_natural.
rewrite !vassocl.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite runitor_lunitor_identity.
rewrite linvunitor_lunitor.
apply id2_left.
}
apply vcomp_rinv.
}
apply idpath.
Local Lemma cartesian_prod_to_cartesian_prod_via_adj_triangle2
: rinvunitor r • (r ◃ η) • lassociator r δ r • (ε ▹ r) • lunitor r
=
id₂ r.
Show proof.
use (BinProductArrowsEq _ _ _ (product)) ; cbn.
- rewrite !vassocl.
rewrite id2_left.
rewrite <- vcomp_lunitor.
etrans.
{
do 3 apply maponpaths.
rewrite !vassocr.
rewrite vcomp_whisker.
rewrite !vassocl.
apply idpath.
}
etrans.
{
do 2 apply maponpaths.
rewrite !vassocr.
rewrite <- lwhisker_lwhisker.
rewrite !vassocl.
apply idpath.
}
etrans.
{
apply maponpaths.
rewrite !vassocr.
do 3 apply maponpaths_2.
rewrite lwhisker_vcomp.
apply maponpaths.
apply (BinProductPr1Commutes
_ _ _
(make_BinProduct
_ _ _ _ _ _
(pr2 Hb _ _ δ _ _ _ _ _ (pr2 product)))).
}
rewrite !vassocl.
etrans.
{
do 3 apply maponpaths.
apply maponpaths_2.
apply binprod_ump_2cell_pr1.
}
rewrite !vassocl.
etrans.
{
do 2 apply maponpaths.
rewrite !vassocr.
rewrite lassociator_rassociator.
rewrite id2_left.
rewrite !vassocl.
apply idpath.
}
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite lwhisker_vcomp.
rewrite vcomp_linv.
rewrite lwhisker_id2.
rewrite id2_left.
apply idpath.
}
rewrite !vassocr.
rewrite rinvunitor_runitor.
rewrite id2_left.
rewrite !vassocl.
rewrite linvunitor_lunitor.
apply id2_right.
- rewrite !vassocl.
rewrite id2_left.
rewrite <- vcomp_lunitor.
etrans.
{
do 3 apply maponpaths.
rewrite !vassocr.
rewrite vcomp_whisker.
rewrite !vassocl.
apply idpath.
}
etrans.
{
do 2 apply maponpaths.
rewrite !vassocr.
rewrite <- lwhisker_lwhisker.
rewrite !vassocl.
apply idpath.
}
etrans.
{
apply maponpaths.
rewrite !vassocr.
do 3 apply maponpaths_2.
rewrite lwhisker_vcomp.
apply maponpaths.
apply (BinProductPr2Commutes
_ _ _
(make_BinProduct
_ _ _ _ _ _
(pr2 Hb _ _ δ _ _ _ _ _ (pr2 product)))).
}
rewrite !vassocl.
etrans.
{
do 3 apply maponpaths.
apply maponpaths_2.
apply binprod_ump_2cell_pr2.
}
rewrite !vassocl.
etrans.
{
do 2 apply maponpaths.
rewrite !vassocr.
rewrite lassociator_rassociator.
rewrite id2_left.
rewrite !vassocl.
apply idpath.
}
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite lwhisker_vcomp.
rewrite vcomp_linv.
rewrite lwhisker_id2.
rewrite id2_left.
apply idpath.
}
rewrite !vassocr.
rewrite rinvunitor_runitor.
rewrite id2_left.
rewrite !vassocl.
rewrite linvunitor_lunitor.
apply id2_right.
- rewrite !vassocl.
rewrite id2_left.
rewrite <- vcomp_lunitor.
etrans.
{
do 3 apply maponpaths.
rewrite !vassocr.
rewrite vcomp_whisker.
rewrite !vassocl.
apply idpath.
}
etrans.
{
do 2 apply maponpaths.
rewrite !vassocr.
rewrite <- lwhisker_lwhisker.
rewrite !vassocl.
apply idpath.
}
etrans.
{
apply maponpaths.
rewrite !vassocr.
do 3 apply maponpaths_2.
rewrite lwhisker_vcomp.
apply maponpaths.
apply (BinProductPr1Commutes
_ _ _
(make_BinProduct
_ _ _ _ _ _
(pr2 Hb _ _ δ _ _ _ _ _ (pr2 product)))).
}
rewrite !vassocl.
etrans.
{
do 3 apply maponpaths.
apply maponpaths_2.
apply binprod_ump_2cell_pr1.
}
rewrite !vassocl.
etrans.
{
do 2 apply maponpaths.
rewrite !vassocr.
rewrite lassociator_rassociator.
rewrite id2_left.
rewrite !vassocl.
apply idpath.
}
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite lwhisker_vcomp.
rewrite vcomp_linv.
rewrite lwhisker_id2.
rewrite id2_left.
apply idpath.
}
rewrite !vassocr.
rewrite rinvunitor_runitor.
rewrite id2_left.
rewrite !vassocl.
rewrite linvunitor_lunitor.
apply id2_right.
- rewrite !vassocl.
rewrite id2_left.
rewrite <- vcomp_lunitor.
etrans.
{
do 3 apply maponpaths.
rewrite !vassocr.
rewrite vcomp_whisker.
rewrite !vassocl.
apply idpath.
}
etrans.
{
do 2 apply maponpaths.
rewrite !vassocr.
rewrite <- lwhisker_lwhisker.
rewrite !vassocl.
apply idpath.
}
etrans.
{
apply maponpaths.
rewrite !vassocr.
do 3 apply maponpaths_2.
rewrite lwhisker_vcomp.
apply maponpaths.
apply (BinProductPr2Commutes
_ _ _
(make_BinProduct
_ _ _ _ _ _
(pr2 Hb _ _ δ _ _ _ _ _ (pr2 product)))).
}
rewrite !vassocl.
etrans.
{
do 3 apply maponpaths.
apply maponpaths_2.
apply binprod_ump_2cell_pr2.
}
rewrite !vassocl.
etrans.
{
do 2 apply maponpaths.
rewrite !vassocr.
rewrite lassociator_rassociator.
rewrite id2_left.
rewrite !vassocl.
apply idpath.
}
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite lwhisker_vcomp.
rewrite vcomp_linv.
rewrite lwhisker_id2.
rewrite id2_left.
apply idpath.
}
rewrite !vassocr.
rewrite rinvunitor_runitor.
rewrite id2_left.
rewrite !vassocl.
rewrite linvunitor_lunitor.
apply id2_right.
Definition cartesian_prod_to_cartesian_prod_via_adj
: cartesian_prod_via_adj b prod.
Show proof.
simple refine ((_ ,, (_ ,, _)) ,, (_ ,, _)).
- exact r.
- exact η.
- exact ε.
- exact cartesian_prod_to_cartesian_prod_via_adj_triangle1.
- exact cartesian_prod_to_cartesian_prod_via_adj_triangle2.
End ToAdj.- exact r.
- exact η.
- exact ε.
- exact cartesian_prod_to_cartesian_prod_via_adj_triangle1.
- exact cartesian_prod_to_cartesian_prod_via_adj_triangle2.
Section FromAdj.
Context (Hb : cartesian_prod_via_adj b prod).
Let δ : b --> pr1 (prod b b)
:= binprod_ump_1cell (pr2 (prod b b)) (id₁ b) (id₁ b).
Let r : pr1 (prod b b) --> b := left_adjoint_right_adjoint (pr1 Hb).
Let η : id₁ b ==> δ · r := left_adjoint_unit (pr1 Hb).
Let ε : r · δ ==> id₁ _ := left_adjoint_counit (pr1 Hb).
Let p
: rinvunitor r • (r ◃ η) • lassociator r δ r • (ε ▹ r) • lunitor r
=
id₂ r
:= internal_triangle2 (pr2 Hb).
Local Definition cartesian_prod_via_adj_to_cartesian_prod_1cell
{x : B}
(f g : x --> b)
: x --> b
:= binprod_ump_1cell (pr2 (prod b b)) f g · r.
Local Definition cartesian_prod_via_adj_to_cartesian_prod_pr1_help
: r ==> binprod_cone_pr1 (pr1 (prod b b))
:= rinvunitor _
• (r ◃ (binprod_ump_1cell_pr1 (pr2 (prod b b)) _ (id₁ b) (id₁ b))^-1)
• lassociator _ _ _
• (ε ▹ _)
• lunitor _.
Local Definition cartesian_prod_via_adj_to_cartesian_prod_pr1
{x : B}
(f g : x --> b)
: cartesian_prod_via_adj_to_cartesian_prod_1cell f g ==> f
:= (_ ◃ cartesian_prod_via_adj_to_cartesian_prod_pr1_help)
• binprod_ump_1cell_pr1 (pr2 (prod b b)) _ f g.
Local Definition cartesian_prod_via_adj_to_cartesian_prod_pr2_help
: r ==> binprod_cone_pr2 (pr1 (prod b b))
:= rinvunitor _
• (r ◃ (binprod_ump_1cell_pr2 (pr2 (prod b b)) _ (id₁ b) (id₁ b))^-1)
• lassociator _ _ _
• (ε ▹ _)
• lunitor _.
Local Definition cartesian_prod_via_adj_to_cartesian_prod_pr2
{x : B}
(f g : x --> b)
: cartesian_prod_via_adj_to_cartesian_prod_1cell f g ==> g
:= (_ ◃ cartesian_prod_via_adj_to_cartesian_prod_pr2_help)
• binprod_ump_1cell_pr2 (pr2 (prod b b)) _ f g.
Local Definition cartesian_prod_via_adj_to_cartesian_prod_2cell
{x : B}
{f g k : x --> b}
(α : k ==> f)
(β : k ==> g)
: k ==> cartesian_prod_via_adj_to_cartesian_prod_1cell f g.
Show proof.
refine (rinvunitor _
• (_ ◃ η)
• lassociator _ _ _
• (binprod_ump_2cell (pr2 (prod b b)) _ _ ▹ r)).
- exact (rassociator _ _ _
• (k ◃ binprod_ump_1cell_pr1 (pr2 (prod b b)) _ _ _)
• runitor _
• α
• (binprod_ump_1cell_pr1 (pr2 (prod b b)) _ _ _)^-1).
- exact (rassociator _ _ _
• (k ◃ binprod_ump_1cell_pr2 (pr2 (prod b b)) _ _ _)
• runitor _
• β
• (binprod_ump_1cell_pr2 (pr2 (prod b b)) _ _ _)^-1).
• (_ ◃ η)
• lassociator _ _ _
• (binprod_ump_2cell (pr2 (prod b b)) _ _ ▹ r)).
- exact (rassociator _ _ _
• (k ◃ binprod_ump_1cell_pr1 (pr2 (prod b b)) _ _ _)
• runitor _
• α
• (binprod_ump_1cell_pr1 (pr2 (prod b b)) _ _ _)^-1).
- exact (rassociator _ _ _
• (k ◃ binprod_ump_1cell_pr2 (pr2 (prod b b)) _ _ _)
• runitor _
• β
• (binprod_ump_1cell_pr2 (pr2 (prod b b)) _ _ _)^-1).
Local Definition cartesian_prod_via_adj_to_cartesian_prod_2cell_pr1
{x : B}
{f g k : x --> b}
(α : k ==> f)
(β : k ==> g)
: cartesian_prod_via_adj_to_cartesian_prod_2cell α β
• cartesian_prod_via_adj_to_cartesian_prod_pr1 f g
=
α.
Show proof.
unfold cartesian_prod_via_adj_to_cartesian_prod_2cell.
unfold cartesian_prod_via_adj_to_cartesian_prod_pr1.
rewrite !vassocl.
etrans.
{
do 3 apply maponpaths.
rewrite !vassocr.
apply maponpaths_2.
refine (vcomp_whisker _ _ @ _).
apply maponpaths.
apply binprod_ump_2cell_pr1.
}
rewrite !vassocl.
rewrite vcomp_linv.
rewrite id2_right.
refine (_ @ id2_left _).
rewrite !vassocr.
apply maponpaths_2.
rewrite !vassocl.
etrans.
{
do 2 apply maponpaths.
rewrite !vassocr.
rewrite <- lwhisker_lwhisker.
rewrite !vassocl.
apply maponpaths.
rewrite !vassocr.
rewrite lassociator_rassociator.
rewrite id2_left.
apply idpath.
}
use vcomp_move_R_pM ; [ is_iso | ] ; cbn.
rewrite id2_right.
refine (_ @ id2_left _).
rewrite !vassocr.
apply maponpaths_2.
rewrite !lwhisker_vcomp.
refine (_ @ lwhisker_id2 _ _).
apply maponpaths.
unfold cartesian_prod_via_adj_to_cartesian_prod_pr1_help.
rewrite <- !lwhisker_vcomp.
rewrite !vassocl.
rewrite left_unit_inv_assoc.
rewrite !vassocl.
etrans.
{
do 2 apply maponpaths.
rewrite !vassocr.
rewrite lwhisker_lwhisker_rassociator.
rewrite !vassocl.
etrans.
{
apply maponpaths.
rewrite !vassocr.
do 3 apply maponpaths_2.
rewrite lwhisker_hcomp.
rewrite inverse_pentagon_4.
rewrite <- rwhisker_hcomp.
apply idpath.
}
rewrite !vassocl.
do 3 apply maponpaths.
rewrite !vassocr.
rewrite rwhisker_lwhisker_rassociator.
rewrite !vassocl.
apply maponpaths.
rewrite !vassocr.
rewrite lunitor_lwhisker.
apply idpath.
}
rewrite !vassocr.
rewrite rinvunitor_natural.
rewrite <- rwhisker_hcomp.
rewrite !vassocl.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite vcomp_whisker.
rewrite !vassocl.
apply idpath.
}
rewrite <- lunitor_V_id_is_left_unit_V_id.
rewrite !vassocr.
rewrite lwhisker_hcomp.
rewrite <- linvunitor_natural.
rewrite !vassocl.
use vcomp_move_R_pM ; [ is_iso | ] ; cbn.
rewrite id2_right.
refine (_ @ id2_left _).
rewrite !vassocr.
apply maponpaths_2.
rewrite !vassocl.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite <- rwhisker_rwhisker.
apply idpath.
}
rewrite !vassocr.
rewrite linvunitor_assoc.
rewrite !vassocl.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite rassociator_lassociator.
rewrite id2_left.
apply idpath.
}
rewrite !rwhisker_vcomp.
refine (_ @ id2_rwhisker _ _).
apply maponpaths.
rewrite !vassocr.
exact (pr12 Hb).
unfold cartesian_prod_via_adj_to_cartesian_prod_pr1.
rewrite !vassocl.
etrans.
{
do 3 apply maponpaths.
rewrite !vassocr.
apply maponpaths_2.
refine (vcomp_whisker _ _ @ _).
apply maponpaths.
apply binprod_ump_2cell_pr1.
}
rewrite !vassocl.
rewrite vcomp_linv.
rewrite id2_right.
refine (_ @ id2_left _).
rewrite !vassocr.
apply maponpaths_2.
rewrite !vassocl.
etrans.
{
do 2 apply maponpaths.
rewrite !vassocr.
rewrite <- lwhisker_lwhisker.
rewrite !vassocl.
apply maponpaths.
rewrite !vassocr.
rewrite lassociator_rassociator.
rewrite id2_left.
apply idpath.
}
use vcomp_move_R_pM ; [ is_iso | ] ; cbn.
rewrite id2_right.
refine (_ @ id2_left _).
rewrite !vassocr.
apply maponpaths_2.
rewrite !lwhisker_vcomp.
refine (_ @ lwhisker_id2 _ _).
apply maponpaths.
unfold cartesian_prod_via_adj_to_cartesian_prod_pr1_help.
rewrite <- !lwhisker_vcomp.
rewrite !vassocl.
rewrite left_unit_inv_assoc.
rewrite !vassocl.
etrans.
{
do 2 apply maponpaths.
rewrite !vassocr.
rewrite lwhisker_lwhisker_rassociator.
rewrite !vassocl.
etrans.
{
apply maponpaths.
rewrite !vassocr.
do 3 apply maponpaths_2.
rewrite lwhisker_hcomp.
rewrite inverse_pentagon_4.
rewrite <- rwhisker_hcomp.
apply idpath.
}
rewrite !vassocl.
do 3 apply maponpaths.
rewrite !vassocr.
rewrite rwhisker_lwhisker_rassociator.
rewrite !vassocl.
apply maponpaths.
rewrite !vassocr.
rewrite lunitor_lwhisker.
apply idpath.
}
rewrite !vassocr.
rewrite rinvunitor_natural.
rewrite <- rwhisker_hcomp.
rewrite !vassocl.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite vcomp_whisker.
rewrite !vassocl.
apply idpath.
}
rewrite <- lunitor_V_id_is_left_unit_V_id.
rewrite !vassocr.
rewrite lwhisker_hcomp.
rewrite <- linvunitor_natural.
rewrite !vassocl.
use vcomp_move_R_pM ; [ is_iso | ] ; cbn.
rewrite id2_right.
refine (_ @ id2_left _).
rewrite !vassocr.
apply maponpaths_2.
rewrite !vassocl.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite <- rwhisker_rwhisker.
apply idpath.
}
rewrite !vassocr.
rewrite linvunitor_assoc.
rewrite !vassocl.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite rassociator_lassociator.
rewrite id2_left.
apply idpath.
}
rewrite !rwhisker_vcomp.
refine (_ @ id2_rwhisker _ _).
apply maponpaths.
rewrite !vassocr.
exact (pr12 Hb).
Local Definition cartesian_prod_via_adj_to_cartesian_prod_2cell_pr2
{x : B}
{f g k : x --> b}
(α : k ==> f)
(β : k ==> g)
: cartesian_prod_via_adj_to_cartesian_prod_2cell α β
• cartesian_prod_via_adj_to_cartesian_prod_pr2 f g
=
β.
Show proof.
unfold cartesian_prod_via_adj_to_cartesian_prod_2cell.
unfold cartesian_prod_via_adj_to_cartesian_prod_pr2.
rewrite !vassocl.
etrans.
{
do 3 apply maponpaths.
rewrite !vassocr.
apply maponpaths_2.
refine (vcomp_whisker _ _ @ _).
apply maponpaths.
apply binprod_ump_2cell_pr2.
}
rewrite !vassocl.
rewrite vcomp_linv.
rewrite id2_right.
refine (_ @ id2_left _).
rewrite !vassocr.
apply maponpaths_2.
rewrite !vassocl.
etrans.
{
do 2 apply maponpaths.
rewrite !vassocr.
rewrite <- lwhisker_lwhisker.
rewrite !vassocl.
apply maponpaths.
rewrite !vassocr.
rewrite lassociator_rassociator.
rewrite id2_left.
apply idpath.
}
use vcomp_move_R_pM ; [ is_iso | ] ; cbn.
rewrite id2_right.
refine (_ @ id2_left _).
rewrite !vassocr.
apply maponpaths_2.
rewrite !lwhisker_vcomp.
refine (_ @ lwhisker_id2 _ _).
apply maponpaths.
unfold cartesian_prod_via_adj_to_cartesian_prod_pr2_help.
rewrite <- !lwhisker_vcomp.
rewrite !vassocl.
rewrite left_unit_inv_assoc.
rewrite !vassocl.
etrans.
{
do 2 apply maponpaths.
rewrite !vassocr.
rewrite lwhisker_lwhisker_rassociator.
rewrite !vassocl.
etrans.
{
apply maponpaths.
rewrite !vassocr.
do 3 apply maponpaths_2.
rewrite lwhisker_hcomp.
rewrite inverse_pentagon_4.
rewrite <- rwhisker_hcomp.
apply idpath.
}
rewrite !vassocl.
do 3 apply maponpaths.
rewrite !vassocr.
rewrite rwhisker_lwhisker_rassociator.
rewrite !vassocl.
apply maponpaths.
rewrite !vassocr.
rewrite lunitor_lwhisker.
apply idpath.
}
rewrite !vassocr.
rewrite rinvunitor_natural.
rewrite <- rwhisker_hcomp.
rewrite !vassocl.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite vcomp_whisker.
rewrite !vassocl.
apply idpath.
}
rewrite <- lunitor_V_id_is_left_unit_V_id.
rewrite !vassocr.
rewrite lwhisker_hcomp.
rewrite <- linvunitor_natural.
rewrite !vassocl.
use vcomp_move_R_pM ; [ is_iso | ] ; cbn.
rewrite id2_right.
refine (_ @ id2_left _).
rewrite !vassocr.
apply maponpaths_2.
rewrite !vassocl.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite <- rwhisker_rwhisker.
apply idpath.
}
rewrite !vassocr.
rewrite linvunitor_assoc.
rewrite !vassocl.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite rassociator_lassociator.
rewrite id2_left.
apply idpath.
}
rewrite !rwhisker_vcomp.
refine (_ @ id2_rwhisker _ _).
apply maponpaths.
rewrite !vassocr.
exact (pr12 Hb).
unfold cartesian_prod_via_adj_to_cartesian_prod_pr2.
rewrite !vassocl.
etrans.
{
do 3 apply maponpaths.
rewrite !vassocr.
apply maponpaths_2.
refine (vcomp_whisker _ _ @ _).
apply maponpaths.
apply binprod_ump_2cell_pr2.
}
rewrite !vassocl.
rewrite vcomp_linv.
rewrite id2_right.
refine (_ @ id2_left _).
rewrite !vassocr.
apply maponpaths_2.
rewrite !vassocl.
etrans.
{
do 2 apply maponpaths.
rewrite !vassocr.
rewrite <- lwhisker_lwhisker.
rewrite !vassocl.
apply maponpaths.
rewrite !vassocr.
rewrite lassociator_rassociator.
rewrite id2_left.
apply idpath.
}
use vcomp_move_R_pM ; [ is_iso | ] ; cbn.
rewrite id2_right.
refine (_ @ id2_left _).
rewrite !vassocr.
apply maponpaths_2.
rewrite !lwhisker_vcomp.
refine (_ @ lwhisker_id2 _ _).
apply maponpaths.
unfold cartesian_prod_via_adj_to_cartesian_prod_pr2_help.
rewrite <- !lwhisker_vcomp.
rewrite !vassocl.
rewrite left_unit_inv_assoc.
rewrite !vassocl.
etrans.
{
do 2 apply maponpaths.
rewrite !vassocr.
rewrite lwhisker_lwhisker_rassociator.
rewrite !vassocl.
etrans.
{
apply maponpaths.
rewrite !vassocr.
do 3 apply maponpaths_2.
rewrite lwhisker_hcomp.
rewrite inverse_pentagon_4.
rewrite <- rwhisker_hcomp.
apply idpath.
}
rewrite !vassocl.
do 3 apply maponpaths.
rewrite !vassocr.
rewrite rwhisker_lwhisker_rassociator.
rewrite !vassocl.
apply maponpaths.
rewrite !vassocr.
rewrite lunitor_lwhisker.
apply idpath.
}
rewrite !vassocr.
rewrite rinvunitor_natural.
rewrite <- rwhisker_hcomp.
rewrite !vassocl.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite vcomp_whisker.
rewrite !vassocl.
apply idpath.
}
rewrite <- lunitor_V_id_is_left_unit_V_id.
rewrite !vassocr.
rewrite lwhisker_hcomp.
rewrite <- linvunitor_natural.
rewrite !vassocl.
use vcomp_move_R_pM ; [ is_iso | ] ; cbn.
rewrite id2_right.
refine (_ @ id2_left _).
rewrite !vassocr.
apply maponpaths_2.
rewrite !vassocl.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite <- rwhisker_rwhisker.
apply idpath.
}
rewrite !vassocr.
rewrite linvunitor_assoc.
rewrite !vassocl.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite rassociator_lassociator.
rewrite id2_left.
apply idpath.
}
rewrite !rwhisker_vcomp.
refine (_ @ id2_rwhisker _ _).
apply maponpaths.
rewrite !vassocr.
exact (pr12 Hb).
Local Definition cartesian_prod_via_adj_to_cartesian_prod_eq
{x : B}
{f g k : x --> b}
(α : k ==> f)
(β : k ==> g)
(φ : ∑ (fg : k ==> cartesian_prod_via_adj_to_cartesian_prod_1cell f g),
fg • cartesian_prod_via_adj_to_cartesian_prod_pr1 f g = α
×
fg • cartesian_prod_via_adj_to_cartesian_prod_pr2 f g = β)
: φ
=
cartesian_prod_via_adj_to_cartesian_prod_2cell α β
,,
cartesian_prod_via_adj_to_cartesian_prod_2cell_pr1 α β
,,
cartesian_prod_via_adj_to_cartesian_prod_2cell_pr2 α β.
Show proof.
use subtypePath.
{
intro.
apply isapropdirprod ; apply cellset_property.
}
cbn.
refine (!(id2_right _) @ _).
unfold cartesian_prod_via_adj_to_cartesian_prod_1cell.
rewrite <- lwhisker_id2.
rewrite <- p.
rewrite <- !lwhisker_vcomp.
rewrite !vassocl.
rewrite !left_unit_inv_assoc.
rewrite !vassocr.
rewrite !rinvunitor_natural.
rewrite <- !rwhisker_hcomp.
unfold cartesian_prod_via_adj_to_cartesian_prod_2cell.
rewrite !vassocl.
apply maponpaths.
rewrite !(maponpaths (λ z, _ • z) (vassocr _ _ _)).
rewrite !lwhisker_lwhisker_rassociator.
rewrite !vassocr.
rewrite !vcomp_whisker.
rewrite !vassocl.
apply maponpaths.
rewrite !(maponpaths (λ z, _ • z) (vassocr _ _ _)).
rewrite !lwhisker_hcomp.
rewrite inverse_pentagon_4.
rewrite <- !lwhisker_hcomp, <- !rwhisker_hcomp.
rewrite !vassocr.
rewrite <- !rwhisker_rwhisker.
rewrite !vassocl.
apply maponpaths.
rewrite !(maponpaths (λ z, _ • (_ • z)) (vassocr _ _ _)).
rewrite rwhisker_lwhisker_rassociator.
rewrite !vassocl.
rewrite lunitor_lwhisker.
rewrite !rwhisker_vcomp.
apply maponpaths.
use (binprod_ump_2cell_unique_alt (pr2 (prod b b))).
- rewrite binprod_ump_2cell_pr1.
rewrite <- !rwhisker_vcomp.
use vcomp_move_L_pM ; [ is_iso | ] ; cbn.
rewrite !vassocr.
rewrite rwhisker_rwhisker.
rewrite !vassocl.
use vcomp_move_L_pM ; [ is_iso ; apply property_from_invertible_2cell | ] ; cbn.
rewrite !vassocr.
rewrite <- vcomp_whisker.
rewrite !vassocl.
use vcomp_move_L_pM ; [ is_iso | ] ; cbn.
rewrite !vassocr.
rewrite rwhisker_hcomp.
rewrite <- rinvunitor_natural.
rewrite !vassocl.
use vcomp_move_L_Mp ; [ is_iso | ] ; cbn.
refine (_ @ pr12 φ).
unfold cartesian_prod_via_adj_to_cartesian_prod_pr1 ; cbn.
rewrite !vassocl.
apply maponpaths.
rewrite !vassocr.
apply maponpaths_2.
unfold cartesian_prod_via_adj_to_cartesian_prod_pr1_help.
rewrite !vassocl.
rewrite <- rinvunitor_triangle.
rewrite <- !lwhisker_vcomp.
rewrite !vassocl.
apply maponpaths.
rewrite !vassocr.
rewrite <- lwhisker_lwhisker.
rewrite !vassocl.
apply maponpaths.
rewrite !vassocr.
rewrite <- lassociator_lassociator.
rewrite !vassocl.
apply maponpaths.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite rwhisker_vcomp.
rewrite lassociator_rassociator.
rewrite id2_rwhisker.
rewrite id2_left.
apply idpath.
}
rewrite !vassocr.
rewrite <- rwhisker_lwhisker.
rewrite !vassocl.
apply maponpaths.
apply runitor_rwhisker.
- rewrite binprod_ump_2cell_pr2.
rewrite <- !rwhisker_vcomp.
use vcomp_move_L_pM ; [ is_iso | ] ; cbn.
rewrite !vassocr.
rewrite rwhisker_rwhisker.
rewrite !vassocl.
use vcomp_move_L_pM ; [ is_iso ; apply property_from_invertible_2cell | ] ; cbn.
rewrite !vassocr.
rewrite <- vcomp_whisker.
rewrite !vassocl.
use vcomp_move_L_pM ; [ is_iso | ] ; cbn.
rewrite !vassocr.
rewrite rwhisker_hcomp.
rewrite <- rinvunitor_natural.
rewrite !vassocl.
use vcomp_move_L_Mp ; [ is_iso | ] ; cbn.
refine (_ @ pr22 φ).
unfold cartesian_prod_via_adj_to_cartesian_prod_pr2 ; cbn.
rewrite !vassocl.
apply maponpaths.
rewrite !vassocr.
apply maponpaths_2.
unfold cartesian_prod_via_adj_to_cartesian_prod_pr2_help.
rewrite !vassocl.
rewrite <- rinvunitor_triangle.
rewrite <- !lwhisker_vcomp.
rewrite !vassocl.
apply maponpaths.
rewrite !vassocr.
rewrite <- lwhisker_lwhisker.
rewrite !vassocl.
apply maponpaths.
rewrite !vassocr.
rewrite <- lassociator_lassociator.
rewrite !vassocl.
apply maponpaths.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite rwhisker_vcomp.
rewrite lassociator_rassociator.
rewrite id2_rwhisker.
rewrite id2_left.
apply idpath.
}
rewrite !vassocr.
rewrite <- rwhisker_lwhisker.
rewrite !vassocl.
apply maponpaths.
apply runitor_rwhisker.
{
intro.
apply isapropdirprod ; apply cellset_property.
}
cbn.
refine (!(id2_right _) @ _).
unfold cartesian_prod_via_adj_to_cartesian_prod_1cell.
rewrite <- lwhisker_id2.
rewrite <- p.
rewrite <- !lwhisker_vcomp.
rewrite !vassocl.
rewrite !left_unit_inv_assoc.
rewrite !vassocr.
rewrite !rinvunitor_natural.
rewrite <- !rwhisker_hcomp.
unfold cartesian_prod_via_adj_to_cartesian_prod_2cell.
rewrite !vassocl.
apply maponpaths.
rewrite !(maponpaths (λ z, _ • z) (vassocr _ _ _)).
rewrite !lwhisker_lwhisker_rassociator.
rewrite !vassocr.
rewrite !vcomp_whisker.
rewrite !vassocl.
apply maponpaths.
rewrite !(maponpaths (λ z, _ • z) (vassocr _ _ _)).
rewrite !lwhisker_hcomp.
rewrite inverse_pentagon_4.
rewrite <- !lwhisker_hcomp, <- !rwhisker_hcomp.
rewrite !vassocr.
rewrite <- !rwhisker_rwhisker.
rewrite !vassocl.
apply maponpaths.
rewrite !(maponpaths (λ z, _ • (_ • z)) (vassocr _ _ _)).
rewrite rwhisker_lwhisker_rassociator.
rewrite !vassocl.
rewrite lunitor_lwhisker.
rewrite !rwhisker_vcomp.
apply maponpaths.
use (binprod_ump_2cell_unique_alt (pr2 (prod b b))).
- rewrite binprod_ump_2cell_pr1.
rewrite <- !rwhisker_vcomp.
use vcomp_move_L_pM ; [ is_iso | ] ; cbn.
rewrite !vassocr.
rewrite rwhisker_rwhisker.
rewrite !vassocl.
use vcomp_move_L_pM ; [ is_iso ; apply property_from_invertible_2cell | ] ; cbn.
rewrite !vassocr.
rewrite <- vcomp_whisker.
rewrite !vassocl.
use vcomp_move_L_pM ; [ is_iso | ] ; cbn.
rewrite !vassocr.
rewrite rwhisker_hcomp.
rewrite <- rinvunitor_natural.
rewrite !vassocl.
use vcomp_move_L_Mp ; [ is_iso | ] ; cbn.
refine (_ @ pr12 φ).
unfold cartesian_prod_via_adj_to_cartesian_prod_pr1 ; cbn.
rewrite !vassocl.
apply maponpaths.
rewrite !vassocr.
apply maponpaths_2.
unfold cartesian_prod_via_adj_to_cartesian_prod_pr1_help.
rewrite !vassocl.
rewrite <- rinvunitor_triangle.
rewrite <- !lwhisker_vcomp.
rewrite !vassocl.
apply maponpaths.
rewrite !vassocr.
rewrite <- lwhisker_lwhisker.
rewrite !vassocl.
apply maponpaths.
rewrite !vassocr.
rewrite <- lassociator_lassociator.
rewrite !vassocl.
apply maponpaths.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite rwhisker_vcomp.
rewrite lassociator_rassociator.
rewrite id2_rwhisker.
rewrite id2_left.
apply idpath.
}
rewrite !vassocr.
rewrite <- rwhisker_lwhisker.
rewrite !vassocl.
apply maponpaths.
apply runitor_rwhisker.
- rewrite binprod_ump_2cell_pr2.
rewrite <- !rwhisker_vcomp.
use vcomp_move_L_pM ; [ is_iso | ] ; cbn.
rewrite !vassocr.
rewrite rwhisker_rwhisker.
rewrite !vassocl.
use vcomp_move_L_pM ; [ is_iso ; apply property_from_invertible_2cell | ] ; cbn.
rewrite !vassocr.
rewrite <- vcomp_whisker.
rewrite !vassocl.
use vcomp_move_L_pM ; [ is_iso | ] ; cbn.
rewrite !vassocr.
rewrite rwhisker_hcomp.
rewrite <- rinvunitor_natural.
rewrite !vassocl.
use vcomp_move_L_Mp ; [ is_iso | ] ; cbn.
refine (_ @ pr22 φ).
unfold cartesian_prod_via_adj_to_cartesian_prod_pr2 ; cbn.
rewrite !vassocl.
apply maponpaths.
rewrite !vassocr.
apply maponpaths_2.
unfold cartesian_prod_via_adj_to_cartesian_prod_pr2_help.
rewrite !vassocl.
rewrite <- rinvunitor_triangle.
rewrite <- !lwhisker_vcomp.
rewrite !vassocl.
apply maponpaths.
rewrite !vassocr.
rewrite <- lwhisker_lwhisker.
rewrite !vassocl.
apply maponpaths.
rewrite !vassocr.
rewrite <- lassociator_lassociator.
rewrite !vassocl.
apply maponpaths.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite rwhisker_vcomp.
rewrite lassociator_rassociator.
rewrite id2_rwhisker.
rewrite id2_left.
apply idpath.
}
rewrite !vassocr.
rewrite <- rwhisker_lwhisker.
rewrite !vassocl.
apply maponpaths.
apply runitor_rwhisker.
Local Definition cartesian_prod_via_adj_to_cartesian_prod_obj
(x : B)
: BinProducts (hom x b).
Show proof.
intros f g.
use make_BinProduct.
- exact (cartesian_prod_via_adj_to_cartesian_prod_1cell f g).
- exact (cartesian_prod_via_adj_to_cartesian_prod_pr1 f g).
- exact (cartesian_prod_via_adj_to_cartesian_prod_pr2 f g).
- intros k α β.
use make_iscontr.
+ simple refine (_ ,, (_ ,, _)).
* exact (cartesian_prod_via_adj_to_cartesian_prod_2cell α β).
* exact (cartesian_prod_via_adj_to_cartesian_prod_2cell_pr1 α β).
* exact (cartesian_prod_via_adj_to_cartesian_prod_2cell_pr2 α β).
+ apply cartesian_prod_via_adj_to_cartesian_prod_eq.
use make_BinProduct.
- exact (cartesian_prod_via_adj_to_cartesian_prod_1cell f g).
- exact (cartesian_prod_via_adj_to_cartesian_prod_pr1 f g).
- exact (cartesian_prod_via_adj_to_cartesian_prod_pr2 f g).
- intros k α β.
use make_iscontr.
+ simple refine (_ ,, (_ ,, _)).
* exact (cartesian_prod_via_adj_to_cartesian_prod_2cell α β).
* exact (cartesian_prod_via_adj_to_cartesian_prod_2cell_pr1 α β).
* exact (cartesian_prod_via_adj_to_cartesian_prod_2cell_pr2 α β).
+ apply cartesian_prod_via_adj_to_cartesian_prod_eq.
Local Definition help_inv2cell
{x y : B}
(f : x --> y)
(h₁ h₂ : y --> b)
: invertible_2cell
(f
· BinProductObject
(hom y b)
(cartesian_prod_via_adj_to_cartesian_prod_obj y h₁ h₂))
(BinProductObject
(hom x b)
(cartesian_prod_via_adj_to_cartesian_prod_obj x (f · h₁) (f · h₂))).
Show proof.
refine (comp_of_invertible_2cell
(lassociator_invertible_2cell _ _ _)
(rwhisker_of_invertible_2cell
_
_)).
use make_invertible_2cell.
- use (binprod_ump_2cell (pr2 (prod b b))).
+ exact (rassociator _ _ _
• (_ ◃ binprod_ump_1cell_pr1 (pr2 (prod b b)) _ h₁ h₂)
• (binprod_ump_1cell_pr1 (pr2 (prod b b)) _ _ _)^-1).
+ exact (rassociator _ _ _
• (_ ◃ binprod_ump_1cell_pr2 (pr2 (prod b b)) _ h₁ h₂)
• (binprod_ump_1cell_pr2 (pr2 (prod b b)) _ _ _)^-1).
- use binprod_ump_2cell_invertible.
+ is_iso.
apply property_from_invertible_2cell.
+ is_iso.
apply property_from_invertible_2cell.
(lassociator_invertible_2cell _ _ _)
(rwhisker_of_invertible_2cell
_
_)).
use make_invertible_2cell.
- use (binprod_ump_2cell (pr2 (prod b b))).
+ exact (rassociator _ _ _
• (_ ◃ binprod_ump_1cell_pr1 (pr2 (prod b b)) _ h₁ h₂)
• (binprod_ump_1cell_pr1 (pr2 (prod b b)) _ _ _)^-1).
+ exact (rassociator _ _ _
• (_ ◃ binprod_ump_1cell_pr2 (pr2 (prod b b)) _ h₁ h₂)
• (binprod_ump_1cell_pr2 (pr2 (prod b b)) _ _ _)^-1).
- use binprod_ump_2cell_invertible.
+ is_iso.
apply property_from_invertible_2cell.
+ is_iso.
apply property_from_invertible_2cell.
Definition cartesian_prod_via_adj_to_cartesian_prod_preserves
{x y : B}
(f : x --> y)
: preserves_binproduct (pre_comp b f).
Show proof.
use preserves_binproduct_if_preserves_chosen.
- apply cartesian_prod_via_adj_to_cartesian_prod_obj.
- intros h₁ h₂.
use (isBinProduct_eq_arrow
_ _
(pr2 (iso_to_BinProduct
_
(cartesian_prod_via_adj_to_cartesian_prod_obj x (f · h₁) (f · h₂))
(z_iso_to_iso
(inv2cell_to_z_iso
(help_inv2cell f h₁ h₂)))))).
+ cbn.
unfold cartesian_prod_via_adj_to_cartesian_prod_pr1.
rewrite !vassocl.
etrans.
{
apply maponpaths.
rewrite !vassocr.
etrans.
{
apply maponpaths_2.
apply vcomp_whisker.
}
rewrite !vassocl.
etrans.
{
apply maponpaths.
apply maponpaths_2.
apply binprod_ump_2cell_pr1.
}
rewrite !vassocl.
rewrite vcomp_linv.
rewrite id2_right.
apply idpath.
}
rewrite !vassocr.
etrans.
{
do 2 apply maponpaths_2.
refine (!_).
apply lwhisker_lwhisker.
}
rewrite !vassocl.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite lassociator_rassociator.
apply id2_left.
}
apply lwhisker_vcomp.
+ cbn.
unfold cartesian_prod_via_adj_to_cartesian_prod_pr2.
rewrite !vassocl.
etrans.
{
apply maponpaths.
rewrite !vassocr.
etrans.
{
apply maponpaths_2.
apply vcomp_whisker.
}
rewrite !vassocl.
etrans.
{
apply maponpaths.
apply maponpaths_2.
apply binprod_ump_2cell_pr2.
}
rewrite !vassocl.
rewrite vcomp_linv.
rewrite id2_right.
apply idpath.
}
rewrite !vassocr.
etrans.
{
do 2 apply maponpaths_2.
refine (!_).
apply lwhisker_lwhisker.
}
rewrite !vassocl.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite lassociator_rassociator.
apply id2_left.
}
apply lwhisker_vcomp.
- apply cartesian_prod_via_adj_to_cartesian_prod_obj.
- intros h₁ h₂.
use (isBinProduct_eq_arrow
_ _
(pr2 (iso_to_BinProduct
_
(cartesian_prod_via_adj_to_cartesian_prod_obj x (f · h₁) (f · h₂))
(z_iso_to_iso
(inv2cell_to_z_iso
(help_inv2cell f h₁ h₂)))))).
+ cbn.
unfold cartesian_prod_via_adj_to_cartesian_prod_pr1.
rewrite !vassocl.
etrans.
{
apply maponpaths.
rewrite !vassocr.
etrans.
{
apply maponpaths_2.
apply vcomp_whisker.
}
rewrite !vassocl.
etrans.
{
apply maponpaths.
apply maponpaths_2.
apply binprod_ump_2cell_pr1.
}
rewrite !vassocl.
rewrite vcomp_linv.
rewrite id2_right.
apply idpath.
}
rewrite !vassocr.
etrans.
{
do 2 apply maponpaths_2.
refine (!_).
apply lwhisker_lwhisker.
}
rewrite !vassocl.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite lassociator_rassociator.
apply id2_left.
}
apply lwhisker_vcomp.
+ cbn.
unfold cartesian_prod_via_adj_to_cartesian_prod_pr2.
rewrite !vassocl.
etrans.
{
apply maponpaths.
rewrite !vassocr.
etrans.
{
apply maponpaths_2.
apply vcomp_whisker.
}
rewrite !vassocl.
etrans.
{
apply maponpaths.
apply maponpaths_2.
apply binprod_ump_2cell_pr2.
}
rewrite !vassocl.
rewrite vcomp_linv.
rewrite id2_right.
apply idpath.
}
rewrite !vassocr.
etrans.
{
do 2 apply maponpaths_2.
refine (!_).
apply lwhisker_lwhisker.
}
rewrite !vassocl.
etrans.
{
apply maponpaths.
rewrite !vassocr.
rewrite lassociator_rassociator.
apply id2_left.
}
apply lwhisker_vcomp.
Definition cartesian_prod_via_adj_to_cartesian_prod
: cartesian_prod b.
Show proof.
split.
- exact cartesian_prod_via_adj_to_cartesian_prod_obj.
- exact @cartesian_prod_via_adj_to_cartesian_prod_preserves.
End FromAdj.- exact cartesian_prod_via_adj_to_cartesian_prod_obj.
- exact @cartesian_prod_via_adj_to_cartesian_prod_preserves.
Definition cartesian_prod_weq_cartesian_prod_via_adj
(HB : is_univalent_2_1 B)
: cartesian_prod b ≃ cartesian_prod_via_adj b prod.
Show proof.
use weqimplimpl.
- exact cartesian_prod_to_cartesian_prod_via_adj.
- exact cartesian_prod_via_adj_to_cartesian_prod.
- apply isaprop_cartesian_prod.
exact HB.
- apply isaprop_cartesian_prod_via_adj.
exact HB.
- exact cartesian_prod_to_cartesian_prod_via_adj.
- exact cartesian_prod_via_adj_to_cartesian_prod.
- apply isaprop_cartesian_prod.
exact HB.
- apply isaprop_cartesian_prod_via_adj.
exact HB.
Definition cartesian_weq_cartesian_via_adj
(HB : is_univalent_2_1 B)
: cartesian_ob b ≃ cartesian_ob_via_adj b T prod.
Show proof.
use weqdirprodf.
- exact (cartesian_terminal_weq_cartesian_terminal_via_adj HB).
- exact (cartesian_prod_weq_cartesian_prod_via_adj HB).
End EquivalenceCartesian.- exact (cartesian_terminal_weq_cartesian_terminal_via_adj HB).
- exact (cartesian_prod_weq_cartesian_prod_via_adj HB).