From 096421b750c3412fcc01d24233472ae7ba132706 Mon Sep 17 00:00:00 2001 From: Niels Date: Mon, 14 Feb 2022 19:24:12 +0100 Subject: [PATCH] Street (op)fibs in Cat --- UniMath/Bicategories/DisplayMapBicat.v | 321 ++++ .../Examples/MorphismsInBicatOfUnivCats.v | 1667 +++++++++++++++++ .../Morphisms/InternalStreetOpFibration.v | 31 + .../Properties/ClosedUnderPullback.v | 100 +- UniMath/CONTENTS.md | 1 + UniMath/CategoryTheory/.package/files | 1 + .../DisplayedCats/StreetFibration.v | 166 ++ .../DisplayedCats/StreetOpFibration.v | 488 +++++ 8 files changed, 2726 insertions(+), 49 deletions(-) create mode 100644 UniMath/CategoryTheory/DisplayedCats/StreetOpFibration.v diff --git a/UniMath/Bicategories/DisplayMapBicat.v b/UniMath/Bicategories/DisplayMapBicat.v index 26017a9d69..1a2eb6cc79 100644 --- a/UniMath/Bicategories/DisplayMapBicat.v +++ b/UniMath/Bicategories/DisplayMapBicat.v @@ -25,6 +25,8 @@ Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Morphisms.FullyFaithful. Require Import UniMath.Bicategories.Morphisms.Adjunctions. +Require Import UniMath.Bicategories.Morphisms.FullyFaithful. +Require Import UniMath.Bicategories.Morphisms.DiscreteMorphisms. Require Import UniMath.Bicategories.Morphisms.InternalStreetFibration. Require Import UniMath.Bicategories.Morphisms.InternalStreetOpFibration. Require Import UniMath.Bicategories.Morphisms.Properties.ClosedUnderPullback. @@ -299,6 +301,62 @@ Proof. + exact (pr2 HD₂ _ _ _ _ p₁ p₂ fe). Defined. +Definition faithful_subbicat + (B : bicat) + : arrow_subbicat B + := full_arrow_subbicat (λ _ _ f, faithful_1cell f). + +Definition faithful_subbicat_props + (B : bicat) + : arrow_subbicat_props (faithful_subbicat B). +Proof. + use full_arrow_subbicat_props. + intros. + apply isaprop_faithful_1cell. +Defined. + +Definition fully_faithful_subbicat + (B : bicat) + : arrow_subbicat B + := full_arrow_subbicat (λ _ _ f, fully_faithful_1cell f). + +Definition fully_faithful_subbicat_props + (B : bicat) + : arrow_subbicat_props (fully_faithful_subbicat B). +Proof. + use full_arrow_subbicat_props. + intros. + apply isaprop_fully_faithful_1cell. +Defined. + +Definition conservative_subbicat + (B : bicat) + : arrow_subbicat B + := full_arrow_subbicat (λ _ _ f, conservative_1cell f). + +Definition conservative_subbicat_props + (B : bicat) + : arrow_subbicat_props (conservative_subbicat B). +Proof. + use full_arrow_subbicat_props. + intros. + apply isaprop_conservative_1cell. +Defined. + +Definition discrete_subbicat + (B : bicat) + : arrow_subbicat B + := full_arrow_subbicat (λ _ _ f, discrete_1cell f). + +Definition discrete_subbicat_props + (B : bicat) + : arrow_subbicat_props (discrete_subbicat B). +Proof. + use full_arrow_subbicat_props. + intros. + apply isaprop_discrete_1cell. +Defined. + Definition sfib_subbicat (B : bicat) : arrow_subbicat B. @@ -355,6 +413,40 @@ Proof. apply isaprop_mor_preserves_opcartesian. Defined. +Definition discrete_sfib_subbicat + (B : bicat) + : arrow_subbicat B + := intersection_arrow_subbicat + (sfib_subbicat B) + (discrete_subbicat B). + +Definition discrete_sfib_subbicat_props + (B : bicat) + (HB_2_1 : is_univalent_2_1 B) + : arrow_subbicat_props (discrete_sfib_subbicat B). +Proof. + use intersection_arrow_subbicat_props. + - exact (sfib_subbicat_props _ HB_2_1). + - exact (discrete_subbicat_props B). +Defined. + +Definition discrete_sopfib_subbicat + (B : bicat) + : arrow_subbicat B + := intersection_arrow_subbicat + (sopfib_subbicat B) + (discrete_subbicat B). + +Definition discrete_sopfib_subbicat_props + (B : bicat) + (HB_2_1 : is_univalent_2_1 B) + : arrow_subbicat_props (discrete_sopfib_subbicat B). +Proof. + use intersection_arrow_subbicat_props. + - exact (sopfib_subbicat_props _ HB_2_1). + - exact (discrete_subbicat_props B). +Defined. + (** 3. Display map bicategories *) @@ -584,6 +676,31 @@ Defined. (** 4. Examples of display map bicategories *) +Definition full_disp_map_bicat + {B : bicat_with_pb} + (P₀ : ∏ (x y : B), x --> y → UU) + (closed_pb : ∏ (pb x y z : B) + (f : x --> z) + (g : y --> z) + (p₁ : pb --> x) + (p₂ : pb --> y) + (γ : invertible_2cell (p₁ · f) (p₂ · g)), + P₀ x z f + → + has_pb_ump (make_pb_cone pb p₁ p₂ γ) + → + P₀ pb y p₂) + : disp_map_bicat B. +Proof. + use make_disp_map_bicat_with_pb. + - exact (full_arrow_subbicat P₀). + - exact (λ pb x y z f g p₁ p₂ γ H₁ H₂, + closed_pb pb x y z f g p₁ p₂ γ H₁ H₂ + ,, + tt). + - exact (λ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _, tt). +Defined. + Definition intersection_disp_map_bicat {B : bicat} (D₁ D₂ : disp_map_bicat B) @@ -611,6 +728,46 @@ Proof. (pr2 Hf) (pr2 Hp₁) (pr2 Hcp₁)). Defined. +Definition faithful_disp_map_bicat + (B : bicat_with_pb) + : disp_map_bicat B. +Proof. + use full_disp_map_bicat. + - exact (λ _ _ f, faithful_1cell f). + - intros pb x y z f g p₁ p₂ γ Hf Hpb. + exact (pb_of_faithful_1cell Hpb Hf). +Defined. + +Definition fully_faithful_disp_map_bicat + (B : bicat_with_pb) + : disp_map_bicat B. +Proof. + use full_disp_map_bicat. + - exact (λ _ _ f, fully_faithful_1cell f). + - intros pb x y z f g p₁ p₂ γ Hf Hpb. + exact (pb_of_fully_faithful_1cell Hpb Hf). +Defined. + +Definition conservative_disp_map_bicat + (B : bicat_with_pb) + : disp_map_bicat B. +Proof. + use full_disp_map_bicat. + - exact (λ _ _ f, conservative_1cell f). + - intros pb x y z f g p₁ p₂ γ Hf Hpb. + exact (pb_of_conservative_1cell Hpb Hf). +Defined. + +Definition discrete_disp_map_bicat + (B : bicat_with_pb) + : disp_map_bicat B. +Proof. + use full_disp_map_bicat. + - exact (λ _ _ f, discrete_1cell f). + - intros pb x y z f g p₁ p₂ γ Hf Hpb. + exact (pb_of_discrete_1cell Hpb Hf). +Defined. + Definition sfib_disp_map_bicat (B : bicat_with_pb) : disp_map_bicat B. @@ -641,6 +798,20 @@ Proof. exact H₃. Defined. +Definition discrete_sfib_disp_map_bicat + (B : bicat_with_pb) + : disp_map_bicat B + := intersection_disp_map_bicat + (sfib_disp_map_bicat B) + (discrete_disp_map_bicat B). + +Definition discrete_sopfib_disp_map_bicat + (B : bicat_with_pb) + : disp_map_bicat B + := intersection_disp_map_bicat + (sopfib_disp_map_bicat B) + (discrete_disp_map_bicat B). + (** 5. Properties of display map bicategories *) @@ -660,6 +831,128 @@ Definition is_contravariant_disp_map_bicat × pred_mor_is_mor_preserves_cartesian D. +Definition intersection_is_covariant + {B : bicat} + {D₁ D₂ : disp_map_bicat B} + (HD₁ : is_covariant_disp_map_bicat D₁) + (HD₂ : is_covariant_disp_map_bicat D₂) + : is_covariant_disp_map_bicat (intersection_disp_map_bicat D₁ D₂). +Proof. + split. + - intros x y f Hf. + apply HD₁. + apply Hf. + - intros e₁ e₂ b₁ b₂ p₁ p₂ fe. + split. + + intro H. + apply HD₁. + apply H. + + intro H. + split. + * apply HD₁. + apply H. + * apply HD₂. + apply H. +Defined. + +Definition intersection_with_full_is_covariant + {B : bicat_with_pb} + (P₀ : ∏ (x y : B), x --> y → UU) + (closed_pb : ∏ (pb x y z : B) + (f : x --> z) + (g : y --> z) + (p₁ : pb --> x) + (p₂ : pb --> y) + (γ : invertible_2cell (p₁ · f) (p₂ · g)), + P₀ x z f + → + has_pb_ump (make_pb_cone pb p₁ p₂ γ) + → + P₀ pb y p₂) + {D : disp_map_bicat B} + (HD : is_covariant_disp_map_bicat D) + : is_covariant_disp_map_bicat + (intersection_disp_map_bicat + D + (full_disp_map_bicat P₀ closed_pb)). +Proof. + split. + - intros x y f Hf. + apply HD. + apply Hf. + - intros e₁ e₂ b₁ b₂ p₁ p₂ fe. + split. + + intro H. + apply HD. + apply H. + + intro H. + split. + * apply HD. + apply H. + * exact tt. +Defined. + +Definition intersection_is_contravariant + {B : bicat} + {D₁ D₂ : disp_map_bicat B} + (HD₁ : is_contravariant_disp_map_bicat D₁) + (HD₂ : is_contravariant_disp_map_bicat D₂) + : is_contravariant_disp_map_bicat (intersection_disp_map_bicat D₁ D₂). +Proof. + split. + - intros x y f Hf. + apply HD₁. + apply Hf. + - intros e₁ e₂ b₁ b₂ p₁ p₂ fe. + split. + + intro H. + apply HD₁. + apply H. + + intro H. + split. + * apply HD₁. + apply H. + * apply HD₂. + apply H. +Defined. + +Definition intersection_with_full_is_contravariant + {B : bicat_with_pb} + (P₀ : ∏ (x y : B), x --> y → UU) + (closed_pb : ∏ (pb x y z : B) + (f : x --> z) + (g : y --> z) + (p₁ : pb --> x) + (p₂ : pb --> y) + (γ : invertible_2cell (p₁ · f) (p₂ · g)), + P₀ x z f + → + has_pb_ump (make_pb_cone pb p₁ p₂ γ) + → + P₀ pb y p₂) + {D : disp_map_bicat B} + (HD : is_contravariant_disp_map_bicat D) + : is_contravariant_disp_map_bicat + (intersection_disp_map_bicat + D + (full_disp_map_bicat P₀ closed_pb)). +Proof. + split. + - intros x y f Hf. + apply HD. + apply Hf. + - intros e₁ e₂ b₁ b₂ p₁ p₂ fe. + split. + + intro H. + apply HD. + apply H. + + intro H. + split. + * apply HD. + apply H. + * exact tt. +Defined. + Definition sopfib_disp_map_bicat_is_covariant (B : bicat_with_pb) : is_covariant_disp_map_bicat (sopfib_disp_map_bicat B). @@ -685,3 +978,31 @@ Proof. + exact (λ H, H). + exact (λ H, H). Defined. + +Definition discrete_sopfib_disp_map_bicat_is_covariant + (B : bicat_with_pb) + : is_covariant_disp_map_bicat (discrete_sopfib_disp_map_bicat B). +Proof. + use intersection_with_full_is_covariant. + split. + - intros ? ? ? H. + exact H. + - intros ? ? ? ? ? ? ?. + split. + + exact (λ H, H). + + exact (λ H, H). +Defined. + +Definition discrete_sfib_disp_map_bicat_is_covariant + (B : bicat_with_pb) + : is_contravariant_disp_map_bicat (discrete_sfib_disp_map_bicat B). +Proof. + use intersection_with_full_is_contravariant. + split. + - intros ? ? ? H. + exact H. + - intros ? ? ? ? ? ? ?. + split. + + exact (λ H, H). + + exact (λ H, H). +Defined. diff --git a/UniMath/Bicategories/Morphisms/Examples/MorphismsInBicatOfUnivCats.v b/UniMath/Bicategories/Morphisms/Examples/MorphismsInBicatOfUnivCats.v index 843d55bd1a..04e32298db 100644 --- a/UniMath/Bicategories/Morphisms/Examples/MorphismsInBicatOfUnivCats.v +++ b/UniMath/Bicategories/Morphisms/Examples/MorphismsInBicatOfUnivCats.v @@ -5,6 +5,8 @@ 1. Faithful 1-cells 2. Fully faithful 1-cells 3. Conservative 1-cells + 4. Internal Street Fibrations + 5. Internal Street Opfibrations *) Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. @@ -15,16 +17,21 @@ Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.categories.StandardCategories. +Require Import UniMath.CategoryTheory.DisplayedCats.StreetFibration. +Require Import UniMath.CategoryTheory.DisplayedCats.StreetOpFibration. Require Import UniMath.Bicategories.Core.Bicat. Import Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.BicategoryLaws. +Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Morphisms.FullyFaithful. Require Import UniMath.Bicategories.Morphisms.DiscreteMorphisms. +Require Import UniMath.Bicategories.Morphisms.InternalStreetFibration. +Require Import UniMath.Bicategories.Morphisms.InternalStreetOpFibration. Local Open Scope cat. @@ -256,3 +263,1663 @@ Proof. - apply isaprop_conservative. - apply isaprop_conservative_1cell. Defined. + +(** + 4. Internal Street Fibrations + *) +Section InternalSFibToStreetFib. + Context {C₁ C₂ : bicat_of_univ_cats} + {F : C₁ --> C₂} + (HF : internal_sfib F). + + Section InternalSFibToStreetFibFactor. + Context {G₁ G₂ : (unit_category : bicat_of_univ_cats) --> C₁} + {α : G₁ ==> G₂} + (Hα : is_cartesian_2cell_sfib F α) + {z : pr1 C₁} + {g : z --> pr1 G₂ tt} + {h : pr1 F z --> pr1 F (pr1 G₁ tt)} + (q : # (pr1 F) g = h · # (pr1 F) (pr1 α tt)). + + Let Φ : unit_category ⟶ pr1 C₁ + := functor_from_unit z. + + Local Definition internal_sfib_is_cartesian_sfib_factor_nat_trans_1 + : Φ ⟹ pr1 G₂. + Proof. + use make_nat_trans. + - intro x ; induction x. + exact g. + - abstract + (intros x y f ; cbn ; + induction x ; induction y ; + cbn ; + assert (p : f = identity _) ; [ apply isapropunit | ] ; + rewrite p ; + refine (id_left _ @ !(id_right _) @ _) ; + apply maponpaths ; + refine (!_) ; + apply functor_id). + Defined. + + Let ζ := internal_sfib_is_cartesian_sfib_factor_nat_trans_1. + + Local Definition internal_sfib_is_cartesian_sfib_factor_nat_trans_2 + : Φ ∙ F ⟹ G₁ ∙ F. + Proof. + use make_nat_trans. + - intros x ; induction x. + exact h. + - abstract + (intros x y f ; cbn ; + induction x ; induction y ; + cbn ; + assert (p : f = identity _) ; [ apply isapropunit | ] ; + rewrite p ; + rewrite (functor_id G₁) ; + rewrite !(functor_id F) ; + rewrite id_left, id_right ; + apply idpath). + Defined. + + Let ξ := internal_sfib_is_cartesian_sfib_factor_nat_trans_2. + + Local Lemma internal_sfib_is_cartesian_sfib_factor_eq + : post_whisker ζ F + = + nat_trans_comp _ _ _ ξ (post_whisker α F). + Proof. + use nat_trans_eq. + { + apply homset_property. + } + intro x ; induction x. + exact q. + Qed. + + Let p := internal_sfib_is_cartesian_sfib_factor_eq. + + Definition internal_sfib_is_cartesian_sfib_factor + : z --> pr1 G₁ tt + := pr1 (is_cartesian_2cell_sfib_factor _ Hα ζ ξ p) tt. + + Definition internal_sfib_is_cartesian_sfib_factor_over + : # (pr1 F) internal_sfib_is_cartesian_sfib_factor = h. + Proof. + exact (nat_trans_eq_pointwise + (is_cartesian_2cell_sfib_factor_over _ Hα p) + tt). + Qed. + + Definition internal_sfib_is_cartesian_sfib_factor_comm + : internal_sfib_is_cartesian_sfib_factor · pr1 α tt = g. + Proof. + exact (nat_trans_eq_pointwise + (is_cartesian_2cell_sfib_factor_comm _ Hα p) + tt). + Qed. + + Local Definition internal_sfib_is_cartesian_sfib_factor_unique_help + (k : z --> pr1 G₁ tt) + : Φ ⟹ pr1 G₁. + Proof. + use make_nat_trans. + - intro x ; induction x. + exact k. + - abstract + (intros x y f ; + induction x ; induction y ; cbn ; + assert (r : f = identity _) ; [ apply isapropunit | ] ; + rewrite r ; + rewrite !(functor_id G₁) ; + rewrite id_left, id_right ; + apply idpath). + Defined. + + Definition internal_sfib_is_cartesian_sfib_factor_unique + : isaprop (∑ φ, # (pr1 F) φ = h × φ · pr1 α tt = g). + Proof. + use invproofirrelevance. + intros φ₁ φ₂. + use subtypePath. + { + intro. + apply isapropdirprod ; apply homset_property. + } + refine (nat_trans_eq_pointwise + (is_cartesian_2cell_sfib_factor_unique + _ Hα + Φ ζ ξ p + (internal_sfib_is_cartesian_sfib_factor_unique_help (pr1 φ₁)) + (internal_sfib_is_cartesian_sfib_factor_unique_help (pr1 φ₂)) + _ _ _ _) + tt) ; + (use nat_trans_eq ; [ apply homset_property | ]) ; + intro x ; induction x ; cbn. + - exact (pr12 φ₁). + - exact (pr12 φ₂). + - exact (pr22 φ₁). + - exact (pr22 φ₂). + Qed. + End InternalSFibToStreetFibFactor. + + Definition internal_sfib_is_cartesian_sfib + {G₁ G₂ : (unit_category : bicat_of_univ_cats) --> C₁} + {α : G₁ ==> G₂} + (Hα : is_cartesian_2cell_sfib F α) + : is_cartesian_sfib F (pr1 α tt). + Proof. + intros z g h q. + use iscontraprop1. + - exact (internal_sfib_is_cartesian_sfib_factor_unique Hα q). + - simple refine (_ ,, _ ,, _). + + exact (internal_sfib_is_cartesian_sfib_factor Hα q). + + exact (internal_sfib_is_cartesian_sfib_factor_over Hα q). + + exact (internal_sfib_is_cartesian_sfib_factor_comm Hα q). + Defined. + + Section Cleaving. + Context {e : pr1 C₁} + {b : pr1 C₂} + (f : b --> pr1 F e). + + Definition internal_sfib_is_street_fib_nat_trans + : functor_from_unit b ⟹ functor_from_unit e ∙ F. + Proof. + use make_nat_trans. + - exact (λ _, f). + - abstract + (intros z₁ z₂ g ; cbn ; + rewrite id_left, functor_id, id_right ; + apply idpath). + Defined. + + Let ℓ := pr1 HF _ _ _ internal_sfib_is_street_fib_nat_trans. + + Definition internal_sfib_is_street_fib_lift_ob + : pr1 C₁ + := pr1 (pr1 ℓ) tt. + + Definition internal_sfib_is_street_fib_lift_mor + : internal_sfib_is_street_fib_lift_ob --> e + := pr1 (pr12 ℓ) tt. + + Definition internal_sfib_is_street_fib_lift_iso + : iso (pr1 F internal_sfib_is_street_fib_lift_ob) b + := nat_iso_pointwise_iso (invertible_2cell_to_nat_iso _ _ (pr122 ℓ)) tt. + + Definition internal_sfib_is_street_fib_lift_over + : # (pr1 F) internal_sfib_is_street_fib_lift_mor + = + internal_sfib_is_street_fib_lift_iso · f + := nat_trans_eq_pointwise (pr2 (pr222 ℓ)) tt. + + Definition internal_sfib_is_street_fib_lift_cartesian + : is_cartesian_sfib F internal_sfib_is_street_fib_lift_mor + := internal_sfib_is_cartesian_sfib (pr1 (pr222 ℓ)). + End Cleaving. + + Definition internal_sfib_is_street_fib + : street_fib F. + Proof. + intros e b f. + simple refine (_ ,, (_ ,, _) ,, _ ,, _) ; cbn. + - exact (internal_sfib_is_street_fib_lift_ob f). + - exact (internal_sfib_is_street_fib_lift_mor f). + - exact (internal_sfib_is_street_fib_lift_iso f). + - exact (internal_sfib_is_street_fib_lift_over f). + - exact (internal_sfib_is_street_fib_lift_cartesian f). + Defined. +End InternalSFibToStreetFib. + +Section StreetFibToInternalSFib. + Context {C₁ C₂ : bicat_of_univ_cats} + {F : C₁ --> C₂} + (HF : street_fib F). + + Section IsCartesian. + Context {C₀ : bicat_of_univ_cats} + {G₁ G₂ : C₀ --> C₁} + (α : G₁ ==> G₂) + (Hα : ∏ (x : pr1 C₀), is_cartesian_sfib F (pr1 α x)). + + Section Factorization. + Context {H : C₀ --> C₁} + {β : H ==> G₂} + {δp : H · F ==> G₁ · F} + (q : β ▹ F = δp • (α ▹ F)). + + Definition pointwise_cartesian_is_cartesian_factor_data + : nat_trans_data (pr1 H) (pr1 G₁) + := λ x, + cartesian_factorization_sfib + _ + (Hα x) + (pr1 β x) + (pr1 δp x) + (nat_trans_eq_pointwise q x). + + Definition pointwise_cartesian_is_cartesian_factor_laws + : is_nat_trans _ _ pointwise_cartesian_is_cartesian_factor_data. + Proof. + intros x y f ; unfold pointwise_cartesian_is_cartesian_factor_data ; cbn. + pose (cartesian_factorization_sfib_commute + F + (Hα x) (pr1 β x) (pr1 δp x) + (nat_trans_eq_pointwise q x)) + as p. + pose (cartesian_factorization_sfib_commute + F + (Hα y) (pr1 β y) (pr1 δp y) + (nat_trans_eq_pointwise q y)) + as p'. + use (cartesian_factorization_sfib_unique + _ + (Hα y) + (pr1 β x · # (pr1 G₂) f) + (pr1 δp x · # (pr1 F) (# (pr1 G₁) f))). + - rewrite functor_comp. + pose (r := nat_trans_eq_pointwise q x) ; cbn in r. + etrans. + { + apply maponpaths_2. + exact r. + } + clear r. + rewrite !assoc'. + apply maponpaths. + refine (!(functor_comp _ _ _) @ _ @ functor_comp _ _ _). + apply maponpaths. + exact (!(nat_trans_ax α _ _ f)). + - rewrite functor_comp. + rewrite cartesian_factorization_sfib_over. + exact (nat_trans_ax δp _ _ f). + - rewrite !functor_comp. + rewrite cartesian_factorization_sfib_over. + apply idpath. + - rewrite !assoc'. + etrans. + { + apply maponpaths. + exact p'. + } + exact (nat_trans_ax β _ _ f). + - rewrite !assoc'. + etrans. + { + apply maponpaths. + exact (nat_trans_ax α _ _ f). + } + rewrite assoc. + apply maponpaths_2. + exact p. + Qed. + + Definition pointwise_cartesian_is_cartesian_factor + : H ==> G₁. + Proof. + use make_nat_trans. + - exact pointwise_cartesian_is_cartesian_factor_data. + - exact pointwise_cartesian_is_cartesian_factor_laws. + Defined. + + Definition pointwise_cartesian_is_cartesian_over + : pointwise_cartesian_is_cartesian_factor ▹ F = δp. + Proof. + use nat_trans_eq. + { + apply homset_property. + } + intro x ; cbn. + apply cartesian_factorization_sfib_over. + Qed. + + Definition pointwise_cartesian_is_cartesian_comm + : pointwise_cartesian_is_cartesian_factor • α = β. + Proof. + use nat_trans_eq. + { + apply homset_property. + } + intro x ; cbn. + apply cartesian_factorization_sfib_commute. + Qed. + + Definition pointwise_cartesian_is_cartesian_unique + : isaprop (∑ (δ : H ==> G₁), δ ▹ F = δp × δ • α = β). + Proof. + use invproofirrelevance. + intros δ₁ δ₂. + use subtypePath. + { + intro. + apply isapropdirprod ; apply cellset_property. + } + use nat_trans_eq. + { + apply homset_property. + } + intro x. + use (cartesian_factorization_sfib_unique + _ (Hα x) + (pr1 β x) + (pr1 δp x)). + - exact (nat_trans_eq_pointwise q x). + - exact (nat_trans_eq_pointwise (pr12 δ₁) x). + - exact (nat_trans_eq_pointwise (pr12 δ₂) x). + - exact (nat_trans_eq_pointwise (pr22 δ₁) x). + - exact (nat_trans_eq_pointwise (pr22 δ₂) x). + Qed. + End Factorization. + + Definition pointwise_cartesian_is_cartesian + : is_cartesian_2cell_sfib F α. + Proof. + intros H β δp q. + use iscontraprop1. + - exact (pointwise_cartesian_is_cartesian_unique q). + - simple refine (_ ,, _ ,, _). + + exact (pointwise_cartesian_is_cartesian_factor q). + + exact (pointwise_cartesian_is_cartesian_over q). + + exact (pointwise_cartesian_is_cartesian_comm q). + Defined. + End IsCartesian. + + Section Cleaving. + Context {C₀ : bicat_of_univ_cats} + {G₁ : C₀ --> C₂} + {G₂ : C₀ --> C₁} + (α : G₁ ==> G₂ · F). + + Definition street_fib_is_internal_sfib_cleaving_lift_data + : functor_data (pr1 C₀) (pr1 C₁). + Proof. + use make_functor_data. + - exact (λ x, pr1 (HF (pr1 G₂ x) (pr1 G₁ x) (pr1 α x))). + - intros x y f ; cbn. + use (cartesian_factorization_sfib + _ + (pr222 (HF (pr1 G₂ y) (pr1 G₁ y) (pr1 α y)))). + + exact (pr112 (HF (pr1 G₂ x) (pr1 G₁ x) (pr1 α x)) · # (pr1 G₂) f). + + exact (pr212 (HF (pr1 G₂ x) (pr1 G₁ x) (pr1 α x)) + · # (pr1 G₁) f + · inv_from_iso (pr212 (HF (pr1 G₂ y) (pr1 G₁ y) (pr1 α y)))). + + abstract + (rewrite functor_comp ; + rewrite (pr122 (HF (pr1 G₂ x) (pr1 G₁ x) (pr1 α x))) ; + rewrite !assoc' ; + apply maponpaths ; + refine (!(nat_trans_ax α _ _ f) @ _) ; + apply maponpaths ; + refine (!_) ; + use iso_inv_on_right ; + rewrite (pr122 (HF (pr1 G₂ y) (pr1 G₁ y) (pr1 α y))) ; + apply idpath). + Defined. + + Definition street_fib_is_internal_sfib_cleaving_lift_is_functor + : is_functor street_fib_is_internal_sfib_cleaving_lift_data. + Proof. + split. + - intro x ; cbn. + use (cartesian_factorization_sfib_unique + _ + (pr222 (HF (pr1 G₂ x) (pr1 G₁ x) (pr1 α x)))). + + exact (pr112 (HF (pr1 G₂ x) (pr1 G₁ x) (pr1 α x))). + + apply identity. + + rewrite id_left. + apply idpath. + + rewrite cartesian_factorization_sfib_over. + refine (!_). + use iso_inv_on_left. + rewrite id_left. + rewrite (functor_id G₁). + rewrite id_right. + apply idpath. + + apply functor_id. + + rewrite cartesian_factorization_sfib_commute. + rewrite (functor_id G₂). + apply id_right. + + apply id_left. + - intros x y z f g ; cbn. + use (cartesian_factorization_sfib_unique + _ + (pr222 (HF (pr1 G₂ z) (pr1 G₁ z) (pr1 α z)))). + + exact (pr112 (HF (pr1 G₂ x) (pr1 G₁ x) (pr1 α x)) · # (pr1 G₂) (f · g)). + + exact (pr212 (HF (pr1 G₂ x) (pr1 G₁ x) (pr1 α x)) + · # (pr1 G₁) (f · g) + · inv_from_iso (pr212 (HF (pr1 G₂ z) (pr1 G₁ z) (pr1 α z)))). + + rewrite functor_comp. + etrans. + { + apply maponpaths_2. + exact (pr122 (HF (pr1 G₂ x) (pr1 G₁ x) (pr1 α x))). + } + rewrite !assoc'. + apply maponpaths. + refine (!(nat_trans_ax α _ _ (f · g)) @ _). + apply maponpaths. + refine (!_). + use iso_inv_on_right. + exact (pr122 (HF (pr1 G₂ z) (pr1 G₁ z) (pr1 α z))). + + apply cartesian_factorization_sfib_over. + + rewrite functor_comp. + rewrite !cartesian_factorization_sfib_over. + rewrite !assoc'. + apply maponpaths. + rewrite !assoc. + apply maponpaths_2. + rewrite (functor_comp G₁). + rewrite !assoc'. + apply maponpaths. + rewrite !assoc. + rewrite iso_after_iso_inv. + apply id_left. + + apply cartesian_factorization_sfib_commute. + + rewrite !assoc'. + rewrite cartesian_factorization_sfib_commute. + rewrite !assoc. + rewrite cartesian_factorization_sfib_commute. + rewrite !assoc'. + rewrite (functor_comp G₂). + apply idpath. + Qed. + + Definition street_fib_is_internal_sfib_cleaving_lift + : C₀ --> C₁. + Proof. + use make_functor. + - exact street_fib_is_internal_sfib_cleaving_lift_data. + - exact street_fib_is_internal_sfib_cleaving_lift_is_functor. + Defined. + + Definition street_fib_is_internal_sfib_cleaving_lift_mor_data + : nat_trans_data + street_fib_is_internal_sfib_cleaving_lift_data + (pr1 G₂) + := λ x, pr112 (HF (pr1 G₂ x) (pr1 G₁ x) (pr1 α x)). + + Definition street_fib_is_internal_sfib_cleaving_lift_mor_is_nat_trans + : is_nat_trans _ _ street_fib_is_internal_sfib_cleaving_lift_mor_data. + Proof. + intros x y f ; cbn. + apply cartesian_factorization_sfib_commute. + Qed. + + Definition street_fib_is_internal_sfib_cleaving_lift_mor + : street_fib_is_internal_sfib_cleaving_lift ==> G₂. + Proof. + use make_nat_trans. + - exact street_fib_is_internal_sfib_cleaving_lift_mor_data. + - exact street_fib_is_internal_sfib_cleaving_lift_mor_is_nat_trans. + Defined. + + Definition street_fib_is_internal_sfib_cleaving_lift_over_nat_trans_data + : nat_trans_data (street_fib_is_internal_sfib_cleaving_lift ∙ F) (pr1 G₁) + := λ x, pr212 (HF (pr1 G₂ x) (pr1 G₁ x) (pr1 α x)). + + Definition street_fib_is_internal_sfib_cleaving_lift_over_is_nat_trans + : is_nat_trans + _ _ + street_fib_is_internal_sfib_cleaving_lift_over_nat_trans_data. + Proof. + intros x y f ; cbn. + unfold street_fib_is_internal_sfib_cleaving_lift_over_nat_trans_data. + rewrite cartesian_factorization_sfib_over. + rewrite !assoc'. + rewrite iso_after_iso_inv. + rewrite id_right. + apply idpath. + Qed. + + Definition street_fib_is_internal_sfib_cleaving_lift_over_nat_trans + : street_fib_is_internal_sfib_cleaving_lift ∙ F ⟹ pr1 G₁. + Proof. + use make_nat_trans. + - exact street_fib_is_internal_sfib_cleaving_lift_over_nat_trans_data. + - exact street_fib_is_internal_sfib_cleaving_lift_over_is_nat_trans. + Defined. + + Definition street_fib_is_internal_sfib_cleaving_lift_cartesian + : is_cartesian_2cell_sfib + F + street_fib_is_internal_sfib_cleaving_lift_mor. + Proof. + use pointwise_cartesian_is_cartesian. + intro x. + exact (pr222 (HF (pr1 G₂ x) (pr1 G₁ x) (pr1 α x))). + Defined. + + Definition street_fib_is_internal_sfib_cleaving_lift_over + : invertible_2cell + (street_fib_is_internal_sfib_cleaving_lift · F) + G₁. + Proof. + use nat_iso_to_invertible_2cell. + use make_nat_iso. + - exact street_fib_is_internal_sfib_cleaving_lift_over_nat_trans. + - intro x. + apply iso_is_iso. + Defined. + End Cleaving. + + Definition street_fib_is_internal_sfib_cleaving + : internal_sfib_cleaving F. + Proof. + intros C₀ G₁ G₂ α. + simple refine (_ ,, _ ,, _ ,, _ ,, _). + - exact (street_fib_is_internal_sfib_cleaving_lift α). + - exact (street_fib_is_internal_sfib_cleaving_lift_mor α). + - exact (street_fib_is_internal_sfib_cleaving_lift_over α). + - exact (street_fib_is_internal_sfib_cleaving_lift_cartesian α). + - abstract + (use nat_trans_eq ; [ apply homset_property | ] ; + intro x ; cbn ; + exact (pr122 (HF (pr1 G₂ x) (pr1 G₁ x) (pr1 α x)))). + Defined. + + Section IsCartesian. + Context {C₀ : bicat_of_univ_cats} + {G₁ G₂ : C₀ --> C₁} + (α : G₁ ==> G₂) + (Hα : is_cartesian_2cell_sfib F α). + + Definition pointwise_lift_functor_data + : functor_data (pr1 C₀) (pr1 C₁). + Proof. + use make_functor_data. + - exact (λ x, pr1 (HF (pr1 G₂ x) (pr1 F (pr1 G₁ x)) (# (pr1 F) (pr1 α x)))). + - intros x y f ; cbn. + use (cartesian_factorization_sfib + _ + (pr222 (HF (pr1 G₂ y) (pr1 F (pr1 G₁ y)) (# (pr1 F) (pr1 α y))))). + + exact (pr112 (HF (pr1 G₂ x) (pr1 F (pr1 G₁ x)) (# (pr1 F) (pr1 α x))) + · # (pr1 G₂) f). + + exact (pr212 (HF (pr1 G₂ x) (pr1 F (pr1 G₁ x)) (# (pr1 F) (pr1 α x))) + · # (pr1 F) (# (pr1 G₁) f) + · inv_from_iso + (pr212 (HF (pr1 G₂ y) (pr1 F (pr1 G₁ y)) (# (pr1 F) (pr1 α y))))). + + abstract + (rewrite functor_comp ; + rewrite (pr122 (HF (pr1 G₂ x) (pr1 F (pr1 G₁ x)) (# (pr1 F) (pr1 α x)))) ; + rewrite !assoc' ; + apply maponpaths ; + rewrite <- (functor_comp F) ; + etrans ; + [ apply maponpaths ; + exact (!(nat_trans_ax α _ _ f)) + | ] ; + rewrite functor_comp ; + apply maponpaths ; + refine (!_) ; + use iso_inv_on_right ; + rewrite (pr122 (HF (pr1 G₂ y) (pr1 F (pr1 G₁ y)) (# (pr1 F) (pr1 α y)))) ; + apply idpath). + Defined. + + Definition pointwise_lift_functor_is_functor + : is_functor pointwise_lift_functor_data. + Proof. + split. + - intro x ; cbn. + use (cartesian_factorization_sfib_unique + _ + (pr222 (HF (pr1 G₂ x) (pr1 F (pr1 G₁ x)) (# (pr1 F) (pr1 α x))))). + + exact (pr112 (HF (pr1 G₂ x) (pr1 F (pr1 G₁ x)) (# (pr1 F) (pr1 α x)))). + + apply identity. + + rewrite id_left. + apply idpath. + + rewrite cartesian_factorization_sfib_over. + refine (!_). + use iso_inv_on_left. + rewrite id_left. + rewrite (functor_id G₁). + rewrite (functor_id F). + apply id_right. + + apply functor_id. + + rewrite cartesian_factorization_sfib_commute. + rewrite (functor_id G₂). + apply id_right. + + apply id_left. + - intros x y z f g ; cbn. + use (cartesian_factorization_sfib_unique + _ + (pr222 (HF (pr1 G₂ z) (pr1 F (pr1 G₁ z)) (# (pr1 F) (pr1 α z))))). + + exact (pr112 (HF (pr1 G₂ x) (pr1 F (pr1 G₁ x)) (# (pr1 F) (pr1 α x))) + · # (pr1 G₂) (f · g)). + + exact (pr212 (HF (pr1 G₂ x) (pr1 F (pr1 G₁ x)) (# (pr1 F) (pr1 α x))) + · # (pr1 F) (# (pr1 G₁) (f · g)) + · inv_from_iso + (pr212 (HF (pr1 G₂ z) (pr1 F (pr1 G₁ z)) (# (pr1 F) (pr1 α z))))). + + rewrite functor_comp. + rewrite (pr122 (HF (pr1 G₂ x) (pr1 F (pr1 G₁ x)) (# (pr1 F) (pr1 α x)))). + rewrite !assoc'. + apply maponpaths. + rewrite <- (functor_comp F). + etrans. + { + apply maponpaths. + exact (!(nat_trans_ax α _ _ (f · g))). + } + rewrite functor_comp. + apply maponpaths. + refine (!_). + use iso_inv_on_right. + rewrite (pr122 (HF (pr1 G₂ z) (pr1 F (pr1 G₁ z)) (# (pr1 F) (pr1 α z)))). + apply idpath. + + apply cartesian_factorization_sfib_over. + + rewrite functor_comp. + rewrite !cartesian_factorization_sfib_over. + rewrite (functor_comp G₁). + rewrite (functor_comp F). + rewrite !assoc'. + do 2 apply maponpaths. + rewrite !assoc. + apply maponpaths_2. + rewrite !assoc'. + use iso_inv_on_right. + apply idpath. + + apply cartesian_factorization_sfib_commute. + + rewrite !assoc'. + rewrite cartesian_factorization_sfib_commute. + rewrite !assoc. + rewrite cartesian_factorization_sfib_commute. + rewrite !assoc'. + rewrite (functor_comp G₂). + apply idpath. + Qed. + + Definition pointwise_lift_functor + : C₀ --> C₁. + Proof. + use make_functor. + - exact pointwise_lift_functor_data. + - exact pointwise_lift_functor_is_functor. + Defined. + + Definition pointwise_lift_nat_trans_data + : nat_trans_data pointwise_lift_functor_data (pr1 G₂) + := λ x, pr112 (HF (pr1 G₂ x) (pr1 F (pr1 G₁ x)) (# (pr1 F) (pr1 α x))). + + Definition pointwise_lift_is_nat_trans + : is_nat_trans _ _ pointwise_lift_nat_trans_data. + Proof. + intros x y f ; cbn. + unfold pointwise_lift_nat_trans_data. + apply cartesian_factorization_sfib_commute. + Qed. + + Definition pointwise_lift_nat_trans + : pointwise_lift_functor ==> G₂. + Proof. + use make_nat_trans. + - exact pointwise_lift_nat_trans_data. + - exact pointwise_lift_is_nat_trans. + Defined. + + Definition pointwise_lift_nat_trans_is_cartesian_2cell + : is_cartesian_2cell_sfib F pointwise_lift_nat_trans. + Proof. + use pointwise_cartesian_is_cartesian. + intro x. + exact (pr222 (HF (pr1 G₂ x) (pr1 F (pr1 G₁ x)) (# (pr1 F) (pr1 α x)))). + Defined. + + Definition is_cartesian_2cell_sfib_pointwise_cartesian_over_data + : nat_trans_data (G₁ ∙ F) (pointwise_lift_functor ∙ F). + Proof. + intro x. + pose (i := pr212 (HF (pr1 G₂ x) (pr1 F (pr1 G₁ x)) (# (pr1 F) (pr1 α x)))). + exact (iso_inv_from_iso i). + Defined. + + Definition is_cartesian_2cell_sfib_pointwise_cartesian_over_laws + : is_nat_trans + _ _ + is_cartesian_2cell_sfib_pointwise_cartesian_over_data. + Proof. + intros x y f ; cbn. + refine (!_). + use iso_inv_on_right. + rewrite !assoc. + use iso_inv_on_left. + rewrite cartesian_factorization_sfib_over. + rewrite !assoc'. + apply maponpaths. + rewrite iso_after_iso_inv. + rewrite id_right. + apply idpath. + Qed. + + Definition is_cartesian_2cell_sfib_pointwise_cartesian_over + : G₁ ∙ F ⟹ pointwise_lift_functor ∙ F. + Proof. + use make_nat_trans. + - exact is_cartesian_2cell_sfib_pointwise_cartesian_over_data. + - exact is_cartesian_2cell_sfib_pointwise_cartesian_over_laws. + Defined. + + Definition is_cartesian_2cell_sfib_pointwise_cartesian_inv2cell + : invertible_2cell (G₁ · F) (pointwise_lift_functor · F). + Proof. + use nat_iso_to_invertible_2cell. + use make_nat_iso. + - exact is_cartesian_2cell_sfib_pointwise_cartesian_over. + - intro. + apply iso_is_iso. + Defined. + + Definition is_cartesian_2cell_sfib_pointwise_cartesian_eq + : α ▹ F + = + is_cartesian_2cell_sfib_pointwise_cartesian_inv2cell + • (pointwise_lift_nat_trans ▹ F). + Proof. + use nat_trans_eq. + { + apply homset_property. + } + intro x. + simpl. + unfold pointwise_lift_nat_trans_data. + refine (!_). + etrans. + { + apply maponpaths. + exact (pr122 (HF (pr1 G₂ x) (pr1 F (pr1 G₁ x)) (# (pr1 F) (pr1 α x)))). + } + rewrite !assoc. + etrans. + { + apply maponpaths_2. + apply iso_after_iso_inv. + } + apply id_left. + Qed. + + Definition is_cartesian_2cell_sfib_pointwise_cartesian + (x : pr1 C₀) + : is_cartesian_sfib F (pr1 α x). + Proof. + pose (i := invertible_between_cartesians + Hα + pointwise_lift_nat_trans_is_cartesian_2cell + is_cartesian_2cell_sfib_pointwise_cartesian_inv2cell + is_cartesian_2cell_sfib_pointwise_cartesian_eq). + use is_cartesian_sfib_eq. + - exact (nat_iso_pointwise_iso (invertible_2cell_to_nat_iso _ _ i) x + · pr1 pointwise_lift_nat_trans x). + - exact (cartesian_factorization_sfib_commute _ _ _ _ _). + - use comp_is_cartesian_sfib. + + apply iso_is_cartesian_sfib. + apply iso_is_iso. + + exact (pr222 (HF (pr1 G₂ x) (pr1 F (pr1 G₁ x)) (# (pr1 F) (pr1 α x)))). + Defined. + End IsCartesian. + + Definition street_fib_is_internal_sfib_lwhisker_is_cartesian + : lwhisker_is_cartesian F. + Proof. + intros C₀ C₀' G H₁ H₂ α Hα. + use pointwise_cartesian_is_cartesian. + intro x ; cbn. + apply is_cartesian_2cell_sfib_pointwise_cartesian. + exact Hα. + Defined. + + Definition street_fib_is_internal_sfib + : internal_sfib F. + Proof. + split. + - exact street_fib_is_internal_sfib_cleaving. + - exact street_fib_is_internal_sfib_lwhisker_is_cartesian. + Defined. +End StreetFibToInternalSFib. + +Definition internal_sfib_weq_street_fib + {C₁ C₂ : bicat_of_univ_cats} + (F : C₁ --> C₂) + : internal_sfib F ≃ street_fib F. +Proof. + use weqimplimpl. + - exact internal_sfib_is_street_fib. + - exact street_fib_is_internal_sfib. + - apply isaprop_internal_sfib. + exact univalent_cat_is_univalent_2_1. + - apply isaprop_street_fib. + apply C₁. +Defined. + +(** + 5. Internal Street Opfibrations + *) +Section InternalSOpFibToStreetOpFib. + Context {C₁ C₂ : bicat_of_univ_cats} + {F : C₁ --> C₂} + (HF : internal_sopfib F). + + Section InternalSOpFibToStreetOpFibFactor. + Context {G₁ G₂ : (unit_category : bicat_of_univ_cats) --> C₁} + {α : G₁ ==> G₂} + (Hα : is_opcartesian_2cell_sopfib F α) + {z : pr1 C₁} + {g : pr1 G₁ tt --> z} + {h : pr1 F (pr1 G₂ tt) --> pr1 F z} + (q : # (pr1 F) g = # (pr1 F) (pr1 α tt) · h). + + Let Φ : unit_category ⟶ pr1 C₁ + := functor_from_unit z. + + Local Definition internal_sopfib_is_opcartesian_sopfib_factor_nat_trans_1 + : pr1 G₁ ⟹ Φ. + Proof. + use make_nat_trans. + - intro x ; induction x. + exact g. + - abstract + (intros x y f ; cbn ; + induction x ; induction y ; + cbn ; + assert (p : f = identity _) ; [ apply isapropunit | ] ; + rewrite p ; + rewrite (functor_id G₁) ; + rewrite id_left, id_right ; + apply idpath). + Defined. + + Let ζ := internal_sopfib_is_opcartesian_sopfib_factor_nat_trans_1. + + Local Definition internal_sopfib_is_opcartesian_sopfib_factor_nat_trans_2 + : G₂ · F ==> Φ ∙ F. + Proof. + use make_nat_trans. + - intros x ; induction x. + exact h. + - abstract + (intros x y f ; cbn ; + induction x ; induction y ; + cbn ; + assert (p : f = identity _) ; [ apply isapropunit | ] ; + rewrite p ; + rewrite (functor_id G₂) ; + rewrite !(functor_id F) ; + rewrite id_left, id_right ; + apply idpath). + Defined. + + Let ξ := internal_sopfib_is_opcartesian_sopfib_factor_nat_trans_2. + + Local Lemma internal_sopfib_is_opcartesian_sopfib_factor_eq + : post_whisker ζ F + = + nat_trans_comp _ _ _ (post_whisker α F) ξ. + Proof. + use nat_trans_eq. + { + apply homset_property. + } + intro x ; induction x. + exact q. + Qed. + + Let p := internal_sopfib_is_opcartesian_sopfib_factor_eq. + + Definition internal_sopfib_is_opcartesian_sopfib_factor + : pr1 G₂ tt --> z + := pr1 (is_opcartesian_2cell_sopfib_factor _ Hα ζ ξ p) tt. + + Definition internal_sopfib_is_opcartesian_sopfib_factor_over + : # (pr1 F) internal_sopfib_is_opcartesian_sopfib_factor = h. + Proof. + exact (nat_trans_eq_pointwise + (is_opcartesian_2cell_sopfib_factor_over _ Hα _ _ p) + tt). + Qed. + + Definition internal_sopfib_is_opcartesian_sopfib_factor_comm + : pr1 α tt · internal_sopfib_is_opcartesian_sopfib_factor = g. + Proof. + exact (nat_trans_eq_pointwise + (is_opcartesian_2cell_sopfib_factor_comm _ Hα _ _ p) + tt). + Qed. + + Local Definition internal_sopfib_is_opcartesian_sopfib_factor_unique_help + (k : pr1 G₂ tt --> z) + : pr1 G₂ ⟹ Φ. + Proof. + use make_nat_trans. + - intro x ; induction x. + exact k. + - abstract + (intros x y f ; + induction x ; induction y ; cbn ; + assert (r : f = identity _) ; [ apply isapropunit | ] ; + rewrite r ; + rewrite !(functor_id G₂) ; + rewrite id_left, id_right ; + apply idpath). + Defined. + + Definition internal_sopfib_is_opcartesian_sopfib_factor_unique + : isaprop (∑ φ, # (pr1 F) φ = h × pr1 α tt · φ = g). + Proof. + use invproofirrelevance. + intros φ₁ φ₂. + use subtypePath. + { + intro. + apply isapropdirprod ; apply homset_property. + } + refine (nat_trans_eq_pointwise + (is_opcartesian_2cell_sopfib_factor_unique + _ Hα + Φ ζ ξ p + (internal_sopfib_is_opcartesian_sopfib_factor_unique_help (pr1 φ₁)) + (internal_sopfib_is_opcartesian_sopfib_factor_unique_help (pr1 φ₂)) + _ _ _ _) + tt) ; + (use nat_trans_eq ; [ apply homset_property | ]) ; + intro x ; induction x ; cbn. + - exact (pr12 φ₁). + - exact (pr12 φ₂). + - exact (pr22 φ₁). + - exact (pr22 φ₂). + Qed. + End InternalSOpFibToStreetOpFibFactor. + + Definition internal_sopfib_is_opcartesian_sopfib + {G₁ G₂ : (unit_category : bicat_of_univ_cats) --> C₁} + {α : G₁ ==> G₂} + (Hα : is_opcartesian_2cell_sopfib F α) + : is_opcartesian_sopfib F (pr1 α tt). + Proof. + intros z g h q. + use iscontraprop1. + - exact (internal_sopfib_is_opcartesian_sopfib_factor_unique Hα q). + - simple refine (_ ,, _ ,, _). + + exact (internal_sopfib_is_opcartesian_sopfib_factor Hα q). + + exact (internal_sopfib_is_opcartesian_sopfib_factor_over Hα q). + + exact (internal_sopfib_is_opcartesian_sopfib_factor_comm Hα q). + Defined. + + Section OpCleaving. + Context {e : pr1 C₁} + {b : pr1 C₂} + (f : pr1 F e --> b). + + Definition internal_sopfib_is_street_opfib_nat_trans + : functor_from_unit e ∙ F ⟹ functor_from_unit b. + Proof. + use make_nat_trans. + - exact (λ _, f). + - abstract + (intros z₁ z₂ g ; cbn ; + rewrite functor_id, id_left, id_right ; + apply idpath). + Defined. + + Let ℓ := pr1 HF _ _ _ internal_sopfib_is_street_opfib_nat_trans. + + Definition internal_sopfib_is_street_opfib_lift_ob + : pr1 C₁ + := pr1 (pr1 ℓ) tt. + + Definition internal_sopfib_is_street_opfib_lift_mor + : e --> internal_sopfib_is_street_opfib_lift_ob + := pr1 (pr12 ℓ) tt. + + Definition internal_sopfib_is_street_opfib_lift_iso + : iso b (pr1 F internal_sopfib_is_street_opfib_lift_ob) + := nat_iso_pointwise_iso (invertible_2cell_to_nat_iso _ _ (pr122 ℓ)) tt. + + Definition internal_sopfib_is_street_opfib_lift_over + : # (pr1 F) internal_sopfib_is_street_opfib_lift_mor + = + f · internal_sopfib_is_street_opfib_lift_iso + := nat_trans_eq_pointwise (pr2 (pr222 ℓ)) tt. + + Definition internal_sopfib_is_street_opfib_lift_cartesian + : is_opcartesian_sopfib F internal_sopfib_is_street_opfib_lift_mor + := internal_sopfib_is_opcartesian_sopfib (pr1 (pr222 ℓ)). + End OpCleaving. + + Definition internal_sopfib_is_street_opfib + : street_opfib F. + Proof. + intros e b f. + simple refine (_ ,, (_ ,, _) ,, _ ,, _) ; cbn. + - exact (internal_sopfib_is_street_opfib_lift_ob f). + - exact (internal_sopfib_is_street_opfib_lift_mor f). + - exact (internal_sopfib_is_street_opfib_lift_iso f). + - exact (internal_sopfib_is_street_opfib_lift_over f). + - exact (internal_sopfib_is_street_opfib_lift_cartesian f). + Defined. +End InternalSOpFibToStreetOpFib. + +Section StreetOpFibToInternalSOpFib. + Context {C₁ C₂ : bicat_of_univ_cats} + {F : C₁ --> C₂} + (HF : street_opfib F). + + Section IsOpCartesian. + Context {C₀ : bicat_of_univ_cats} + {G₁ G₂ : C₀ --> C₁} + (α : G₁ ==> G₂) + (Hα : ∏ (x : pr1 C₀), is_opcartesian_sopfib F (pr1 α x)). + + Section Factorization. + Context {H : C₀ --> C₁} + {β : G₁ ==> H} + {δp : G₂ · F ==> H · F} + (q : β ▹ F = (α ▹ F) • δp). + + Definition pointwise_opcartesian_is_opcartesian_factor_data + : nat_trans_data (pr1 G₂) (pr1 H) + := λ x, + opcartesian_factorization_sopfib + _ + (Hα x) + (pr1 β x) + (pr1 δp x) + (nat_trans_eq_pointwise q x). + + Definition pointwise_opcartesian_is_opcartesian_factor_laws + : is_nat_trans _ _ pointwise_opcartesian_is_opcartesian_factor_data. + Proof. + intros x y f ; unfold pointwise_opcartesian_is_opcartesian_factor_data ; cbn. + pose (opcartesian_factorization_sopfib_commute + F + (Hα x) (pr1 β x) (pr1 δp x) + (nat_trans_eq_pointwise q x)) + as p. + pose (opcartesian_factorization_sopfib_commute + F + (Hα y) (pr1 β y) (pr1 δp y) + (nat_trans_eq_pointwise q y)) + as p'. + use (opcartesian_factorization_sopfib_unique + _ + (Hα x) + (pr1 β x · # (pr1 H) f) + (pr1 δp x · # (pr1 F) (# (pr1 H) f))). + - rewrite functor_comp. + pose (r := nat_trans_eq_pointwise q x) ; cbn in r. + etrans. + { + apply maponpaths_2. + exact r. + } + clear r. + rewrite !assoc'. + apply idpath. + - rewrite functor_comp. + rewrite opcartesian_factorization_sopfib_over. + exact (nat_trans_ax δp _ _ f). + - rewrite !functor_comp. + rewrite opcartesian_factorization_sopfib_over. + apply idpath. + - rewrite !assoc. + etrans. + { + apply maponpaths_2. + exact (!(nat_trans_ax α _ _ f)). + } + rewrite !assoc'. + etrans. + { + apply maponpaths. + exact p'. + } + exact (nat_trans_ax β _ _ f). + - rewrite !assoc. + apply maponpaths_2. + exact p. + Qed. + + Definition pointwise_opcartesian_is_opcartesian_factor + : G₂ ==> H. + Proof. + use make_nat_trans. + - exact pointwise_opcartesian_is_opcartesian_factor_data. + - exact pointwise_opcartesian_is_opcartesian_factor_laws. + Defined. + + Definition pointwise_opcartesian_is_opcartesian_over + : pointwise_opcartesian_is_opcartesian_factor ▹ F = δp. + Proof. + use nat_trans_eq. + { + apply homset_property. + } + intro x ; cbn. + apply opcartesian_factorization_sopfib_over. + Qed. + + Definition pointwise_opcartesian_is_opcartesian_comm + : α • pointwise_opcartesian_is_opcartesian_factor = β. + Proof. + use nat_trans_eq. + { + apply homset_property. + } + intro x ; cbn. + apply opcartesian_factorization_sopfib_commute. + Qed. + + Definition pointwise_opcartesian_is_opcartesian_unique + : isaprop (∑ (δ : G₂ ==> H), δ ▹ F = δp × α • δ = β). + Proof. + use invproofirrelevance. + intros δ₁ δ₂. + use subtypePath. + { + intro. + apply isapropdirprod ; apply cellset_property. + } + use nat_trans_eq. + { + apply homset_property. + } + intro x. + use (opcartesian_factorization_sopfib_unique + _ (Hα x) + (pr1 β x) + (pr1 δp x)). + - exact (nat_trans_eq_pointwise q x). + - exact (nat_trans_eq_pointwise (pr12 δ₁) x). + - exact (nat_trans_eq_pointwise (pr12 δ₂) x). + - exact (nat_trans_eq_pointwise (pr22 δ₁) x). + - exact (nat_trans_eq_pointwise (pr22 δ₂) x). + Qed. + End Factorization. + + Definition pointwise_opcartesian_is_opcartesian + : is_opcartesian_2cell_sopfib F α. + Proof. + intros H β δp q. + use iscontraprop1. + - exact (pointwise_opcartesian_is_opcartesian_unique q). + - simple refine (_ ,, _ ,, _). + + exact (pointwise_opcartesian_is_opcartesian_factor q). + + exact (pointwise_opcartesian_is_opcartesian_over q). + + exact (pointwise_opcartesian_is_opcartesian_comm q). + Defined. + End IsOpCartesian. + + Section OpCleaving. + Context {C₀ : bicat_of_univ_cats} + {G₁ : C₀ --> C₁} + {G₂ : C₀ --> C₂} + (α : G₁ · F ==> G₂). + + Definition street_opfib_is_internal_sopfib_opcleaving_lift_data + : functor_data (pr1 C₀) (pr1 C₁). + Proof. + use make_functor_data. + - exact (λ x, pr1 (HF _ _ (pr1 α x))). + - intros x y f ; cbn. + use (opcartesian_factorization_sopfib + _ + (pr222 (HF _ _ (pr1 α x)))). + + exact (# (pr1 G₁) f · pr112 (HF _ _ (pr1 α y))). + + exact (inv_from_iso (pr212 (HF _ _ (pr1 α x))) + · # (pr1 G₂) f + · pr212 (HF _ _ (pr1 α y))). + + abstract + (rewrite functor_comp ; + rewrite (pr122 (HF _ _ (pr1 α x))) ; + refine (maponpaths (λ z, _ · z) (pr122 (HF _ _ (pr1 α y))) @ _) ; + rewrite !assoc ; + apply maponpaths_2 ; + refine (nat_trans_ax α _ _ f @ _) ; + rewrite !assoc' ; + apply maponpaths ; + rewrite !assoc ; + rewrite iso_inv_after_iso ; + rewrite id_left ; + apply idpath). + Defined. + + Definition street_opfib_is_internal_sopfib_opcleaving_lift_is_functor + : is_functor street_opfib_is_internal_sopfib_opcleaving_lift_data. + Proof. + split. + - intro x ; cbn. + use (opcartesian_factorization_sopfib_unique + _ + (pr222 (HF _ _ (pr1 α x)))). + + exact (pr112 (HF _ _ (pr1 α x))). + + apply identity. + + rewrite id_right. + apply idpath. + + rewrite opcartesian_factorization_sopfib_over. + refine (!_). + rewrite (functor_id G₂). + rewrite id_right. + rewrite iso_after_iso_inv. + apply idpath. + + apply functor_id. + + rewrite opcartesian_factorization_sopfib_commute. + rewrite (functor_id G₁). + apply id_left. + + apply id_right. + - intros x y z f g ; cbn. + use (opcartesian_factorization_sopfib_unique + _ + (pr222 (HF _ _ (pr1 α x)))). + + exact (# (pr1 G₁) (f · g) · pr112 (HF _ _ (pr1 α z))). + + exact (inv_from_iso (pr212 (HF _ _ (pr1 α x))) + · # (pr1 G₂) (f · g) + · pr212 (HF _ _ (pr1 α z))). + + rewrite functor_comp. + etrans. + { + apply maponpaths. + exact (pr122 (HF _ _ (pr1 α z))). + } + rewrite !assoc. + apply maponpaths_2. + refine (nat_trans_ax α _ _ (f · g) @ _). + apply maponpaths_2. + use iso_inv_on_left. + exact (pr122 (HF _ _ (pr1 α x))). + + apply opcartesian_factorization_sopfib_over. + + rewrite functor_comp. + rewrite !opcartesian_factorization_sopfib_over. + rewrite !assoc'. + apply maponpaths. + rewrite !assoc. + apply maponpaths_2. + rewrite (functor_comp G₂). + rewrite !assoc'. + apply maponpaths. + rewrite !assoc. + rewrite iso_inv_after_iso. + apply id_left. + + apply opcartesian_factorization_sopfib_commute. + + rewrite !assoc. + rewrite opcartesian_factorization_sopfib_commute. + rewrite !assoc'. + rewrite opcartesian_factorization_sopfib_commute. + rewrite !assoc. + rewrite (functor_comp G₁). + apply idpath. + Qed. + + Definition street_opfib_is_internal_sopfib_opcleaving_lift + : C₀ --> C₁. + Proof. + use make_functor. + - exact street_opfib_is_internal_sopfib_opcleaving_lift_data. + - exact street_opfib_is_internal_sopfib_opcleaving_lift_is_functor. + Defined. + + Definition street_opfib_is_internal_sopfib_opcleaving_lift_mor_data + : nat_trans_data + (pr1 G₁) + street_opfib_is_internal_sopfib_opcleaving_lift_data + := λ x, pr112 (HF _ _ (pr1 α x)). + + Definition street_opfib_is_internal_sopfib_opcleaving_lift_mor_is_nat_trans + : is_nat_trans _ _ street_opfib_is_internal_sopfib_opcleaving_lift_mor_data. + Proof. + intros x y f ; cbn. + refine (!_). + apply opcartesian_factorization_sopfib_commute. + Qed. + + Definition street_opfib_is_internal_sopfib_opcleaving_lift_mor + : G₁ ==> street_opfib_is_internal_sopfib_opcleaving_lift. + Proof. + use make_nat_trans. + - exact street_opfib_is_internal_sopfib_opcleaving_lift_mor_data. + - exact street_opfib_is_internal_sopfib_opcleaving_lift_mor_is_nat_trans. + Defined. + + Definition street_opfib_is_internal_sopfib_opcleaving_lift_over_nat_trans_data + : nat_trans_data (pr1 G₂) (street_opfib_is_internal_sopfib_opcleaving_lift ∙ F) + := λ x, pr212 (HF _ _ (pr1 α x)). + + Definition street_opfib_is_internal_sopfib_opcleaving_lift_over_is_nat_trans + : is_nat_trans + _ _ + street_opfib_is_internal_sopfib_opcleaving_lift_over_nat_trans_data. + Proof. + intros x y f ; cbn. + unfold street_opfib_is_internal_sopfib_opcleaving_lift_over_nat_trans_data. + rewrite opcartesian_factorization_sopfib_over. + rewrite !assoc. + rewrite iso_inv_after_iso. + rewrite id_left. + apply idpath. + Qed. + + Definition street_opfib_is_internal_sopfib_opcleaving_lift_over_nat_trans + : pr1 G₂ ⟹ street_opfib_is_internal_sopfib_opcleaving_lift ∙ F. + Proof. + use make_nat_trans. + - exact street_opfib_is_internal_sopfib_opcleaving_lift_over_nat_trans_data. + - exact street_opfib_is_internal_sopfib_opcleaving_lift_over_is_nat_trans. + Defined. + + Definition street_opfib_is_internal_sopfib_opcleaving_lift_opcartesian + : is_opcartesian_2cell_sopfib + F + street_opfib_is_internal_sopfib_opcleaving_lift_mor. + Proof. + use pointwise_opcartesian_is_opcartesian. + intro x. + exact (pr222 (HF _ _ (pr1 α x))). + Defined. + + Definition street_opfib_is_internal_sopfib_opcleaving_lift_over + : invertible_2cell + G₂ + (street_opfib_is_internal_sopfib_opcleaving_lift · F). + Proof. + use nat_iso_to_invertible_2cell. + use make_nat_iso. + - exact street_opfib_is_internal_sopfib_opcleaving_lift_over_nat_trans. + - intro x. + apply iso_is_iso. + Defined. + End OpCleaving. + + Definition street_opfib_is_internal_sopfib_opcleaving + : internal_sopfib_opcleaving F. + Proof. + intros C₀ G₁ G₂ α. + simple refine (_ ,, _ ,, _ ,, _ ,, _). + - exact (street_opfib_is_internal_sopfib_opcleaving_lift α). + - exact (street_opfib_is_internal_sopfib_opcleaving_lift_mor α). + - exact (street_opfib_is_internal_sopfib_opcleaving_lift_over α). + - exact (street_opfib_is_internal_sopfib_opcleaving_lift_opcartesian α). + - abstract + (use nat_trans_eq ; [ apply homset_property | ] ; + intro x ; cbn ; + exact (pr122 (HF _ _ (pr1 α x)))). + Defined. + + Section IsOpCartesian. + Context {C₀ : bicat_of_univ_cats} + {G₁ G₂ : C₀ --> C₁} + (α : G₁ ==> G₂) + (Hα : is_opcartesian_2cell_sopfib F α). + + Definition pointwise_oplift_functor_data + : functor_data (pr1 C₀) (pr1 C₁). + Proof. + use make_functor_data. + - exact (λ x, pr1 (HF _ _ (# (pr1 F) (pr1 α x)))). + - intros x y f ; cbn. + use (opcartesian_factorization_sopfib + _ + (pr222 (HF _ _ (# (pr1 F) (pr1 α x))))). + + exact (# (pr1 G₁) f · pr112 (HF _ _ (# (pr1 F) (pr1 α y)))). + + exact (inv_from_iso (pr212 (HF _ _ (# (pr1 F) (pr1 α x)))) + · # (pr1 F) (# (pr1 G₂) f) + · pr212 (HF _ _ (# (pr1 F) (pr1 α y)))). + + abstract + (rewrite functor_comp ; + rewrite (pr122 (HF _ _ (# (pr1 F) (pr1 α x)))) ; + rewrite !assoc ; + etrans ; + [ apply maponpaths ; + exact (pr122 (HF _ _ (# (pr1 F) (pr1 α y)))) + | ] ; + rewrite !assoc ; + apply maponpaths_2 ; + rewrite <- !functor_comp ; + etrans ; + [ apply maponpaths ; + exact (nat_trans_ax α _ _ f) + | ] ; + rewrite functor_comp ; + rewrite !assoc' ; + apply maponpaths ; + rewrite !assoc ; + rewrite iso_inv_after_iso ; + rewrite id_left ; + apply idpath). + Defined. + + Definition pointwise_oplift_functor_is_functor + : is_functor pointwise_oplift_functor_data. + Proof. + split. + - intro x ; cbn. + use (opcartesian_factorization_sopfib_unique + _ + (pr222 (HF _ _ (# (pr1 F) (pr1 α x))))). + + exact (pr112 (HF _ _ (# (pr1 F) (pr1 α x)))). + + apply identity. + + rewrite id_right. + apply idpath. + + rewrite opcartesian_factorization_sopfib_over. + rewrite !assoc'. + use iso_inv_on_right. + rewrite id_right. + rewrite (functor_id G₂). + rewrite (functor_id F). + apply id_left. + + apply functor_id. + + rewrite opcartesian_factorization_sopfib_commute. + rewrite (functor_id G₁). + apply id_left. + + apply id_right. + - intros x y z f g ; cbn. + use (opcartesian_factorization_sopfib_unique + _ + (pr222 (HF _ _ (# (pr1 F) (pr1 α x))))). + + exact (# (pr1 G₁) (f · g) + · pr112 (HF _ _ (# (pr1 F) (pr1 α z)))). + + exact (inv_from_iso + (pr212 (HF _ _ (# (pr1 F) (pr1 α x)))) + · # (pr1 F) (# (pr1 G₂) (f · g)) + · pr212 (HF _ _ (# (pr1 F) (pr1 α z)))). + + rewrite functor_comp. + rewrite (pr122 (HF _ _ (# (pr1 F) (pr1 α x)))). + etrans. + { + apply maponpaths. + exact (pr122 (HF _ _ (# (pr1 F) (pr1 α z)))). + } + rewrite !assoc. + rewrite <- (functor_comp F). + etrans. + { + apply maponpaths_2. + apply maponpaths. + exact (nat_trans_ax α _ _ (f · g)). + } + rewrite functor_comp. + rewrite !assoc'. + apply maponpaths. + rewrite !assoc. + apply maponpaths_2. + rewrite iso_inv_after_iso. + rewrite id_left. + apply idpath. + + apply opcartesian_factorization_sopfib_over. + + rewrite functor_comp. + rewrite !opcartesian_factorization_sopfib_over. + rewrite (functor_comp G₂). + rewrite (functor_comp F). + rewrite !assoc'. + do 2 apply maponpaths. + rewrite !assoc. + apply maponpaths_2. + rewrite iso_inv_after_iso. + apply id_left. + + apply opcartesian_factorization_sopfib_commute. + + rewrite !assoc. + rewrite opcartesian_factorization_sopfib_commute. + rewrite !assoc'. + rewrite opcartesian_factorization_sopfib_commute. + rewrite !assoc. + rewrite (functor_comp G₁). + apply idpath. + Qed. + + Definition pointwise_oplift_functor + : C₀ --> C₁. + Proof. + use make_functor. + - exact pointwise_oplift_functor_data. + - exact pointwise_oplift_functor_is_functor. + Defined. + + Definition pointwise_oplift_nat_trans_data + : nat_trans_data (pr1 G₁) pointwise_oplift_functor_data + := λ x, pr112 (HF _ _ (# (pr1 F) (pr1 α x))). + + Definition pointwise_oplift_is_nat_trans + : is_nat_trans _ _ pointwise_oplift_nat_trans_data. + Proof. + intros x y f ; cbn. + unfold pointwise_oplift_nat_trans_data. + refine (!_). + apply opcartesian_factorization_sopfib_commute. + Qed. + + Definition pointwise_oplift_nat_trans + : G₁ ==> pointwise_oplift_functor. + Proof. + use make_nat_trans. + - exact pointwise_oplift_nat_trans_data. + - exact pointwise_oplift_is_nat_trans. + Defined. + + Definition pointwise_oplift_nat_trans_is_opcartesian_2cell + : is_opcartesian_2cell_sopfib F pointwise_oplift_nat_trans. + Proof. + use pointwise_opcartesian_is_opcartesian. + intro x. + exact (pr222 (HF _ _ (# (pr1 F) (pr1 α x)))). + Defined. + + Definition is_opcartesian_2cell_sopfib_pointwise_opcartesian_over_data + : nat_trans_data (pointwise_oplift_functor ∙ F) (G₂ ∙ F). + Proof. + intro x. + pose (i := pr212 (HF _ _ (# (pr1 F) (pr1 α x)))). + exact (iso_inv_from_iso i). + Defined. + + Definition is_opcartesian_2cell_sopfib_pointwise_opcartesian_over_laws + : is_nat_trans + _ _ + is_opcartesian_2cell_sopfib_pointwise_opcartesian_over_data. + Proof. + intros x y f ; cbn. + refine (!_). + use iso_inv_on_right. + rewrite !assoc. + use iso_inv_on_left. + rewrite opcartesian_factorization_sopfib_over. + rewrite !assoc. + apply maponpaths_2. + rewrite iso_inv_after_iso. + rewrite id_left. + apply idpath. + Qed. + + Definition is_opcartesian_2cell_sopfib_pointwise_opcartesian_over + : pointwise_oplift_functor ∙ F ⟹ G₂ ∙ F. + Proof. + use make_nat_trans. + - exact is_opcartesian_2cell_sopfib_pointwise_opcartesian_over_data. + - exact is_opcartesian_2cell_sopfib_pointwise_opcartesian_over_laws. + Defined. + + Definition is_opcartesian_2cell_sopfib_pointwise_opcartesian_inv2cell + : invertible_2cell (pointwise_oplift_functor · F) (G₂ · F). + Proof. + use nat_iso_to_invertible_2cell. + use make_nat_iso. + - exact is_opcartesian_2cell_sopfib_pointwise_opcartesian_over. + - intro. + apply iso_is_iso. + Defined. + + Definition is_opcartesian_2cell_sopfib_pointwise_opcartesian_eq + : α ▹ F + = + (pointwise_oplift_nat_trans ▹ F) + • is_opcartesian_2cell_sopfib_pointwise_opcartesian_inv2cell. + Proof. + use nat_trans_eq. + { + apply homset_property. + } + intro x. + cbn. + unfold pointwise_oplift_nat_trans_data. + refine (!_). + etrans. + { + apply maponpaths_2. + exact (pr122 (HF _ _ (# (pr1 F) (pr1 α x)))). + } + rewrite !assoc'. + etrans. + { + apply maponpaths. + apply iso_inv_after_iso. + } + apply id_right. + Qed. + + Definition is_opcartesian_2cell_sfib_pointwise_opcartesian + (x : pr1 C₀) + : is_opcartesian_sopfib F (pr1 α x). + Proof. + pose (i := invertible_between_opcartesians + Hα + pointwise_oplift_nat_trans_is_opcartesian_2cell + is_opcartesian_2cell_sopfib_pointwise_opcartesian_inv2cell + is_opcartesian_2cell_sopfib_pointwise_opcartesian_eq). + use is_opcartesian_sopfib_eq. + - exact (pr1 pointwise_oplift_nat_trans x + · nat_iso_pointwise_iso (invertible_2cell_to_nat_iso _ _ i) x). + - exact (opcartesian_factorization_sopfib_commute _ _ _ _ _). + - use comp_is_opcartesian_sopfib. + + exact (pr222 (HF _ _ (# (pr1 F) (pr1 α x)))). + + apply iso_is_opcartesian_sopfib. + apply iso_is_iso. + Qed. + End IsOpCartesian. + + Definition street_opfib_is_internal_sopfib_lwhisker_is_opcartesian + : lwhisker_is_opcartesian F. + Proof. + intros C₀ C₀' G H₁ H₂ α Hα. + use pointwise_opcartesian_is_opcartesian. + intro x ; cbn. + apply is_opcartesian_2cell_sfib_pointwise_opcartesian. + exact Hα. + Defined. + + Definition street_opfib_is_internal_sopfib + : internal_sopfib F. + Proof. + split. + - exact street_opfib_is_internal_sopfib_opcleaving. + - exact street_opfib_is_internal_sopfib_lwhisker_is_opcartesian. + Defined. +End StreetOpFibToInternalSOpFib. + +Definition internal_sopfib_weq_street_opfib + {C₁ C₂ : bicat_of_univ_cats} + (F : C₁ --> C₂) + : internal_sopfib F ≃ street_opfib F. +Proof. + use weqimplimpl. + - exact internal_sopfib_is_street_opfib. + - exact street_opfib_is_internal_sopfib. + - apply isaprop_internal_sopfib. + exact univalent_cat_is_univalent_2_1. + - apply isaprop_street_opfib. + apply C₁. +Defined. diff --git a/UniMath/Bicategories/Morphisms/InternalStreetOpFibration.v b/UniMath/Bicategories/Morphisms/InternalStreetOpFibration.v index f70f669204..6fb22fba74 100644 --- a/UniMath/Bicategories/Morphisms/InternalStreetOpFibration.v +++ b/UniMath/Bicategories/Morphisms/InternalStreetOpFibration.v @@ -508,6 +508,37 @@ Proof. - exact q. Defined. +Definition invertible_between_opcartesians + {B : bicat} + {x e b : B} + {p : e --> b} + {g₀ g₁ g₂ : x --> e} + {α : g₀ ==> g₁} + (Hα : is_opcartesian_2cell_sopfib p α) + {β : g₀ ==> g₂} + (Hβ : is_opcartesian_2cell_sopfib p β) + (δ : invertible_2cell (g₂ · p) (g₁ · p)) + (q : α ▹ p = (β ▹ p) • pr1 δ) + : invertible_2cell g₂ g₁. +Proof. + use (make_invertible_2cell + (bicat_is_invertible_2cell_to_op2_bicat_is_invertible_2cell + _ + (@invertible_between_cartesians + (op2_bicat B) + x e b + p + _ _ _ + α + (is_opcartesian_to_is_cartesian_sfib Hα) + β + (is_opcartesian_to_is_cartesian_sfib Hβ) + _ + _))). + - exact (bicat_invertible_2cell_is_op2_bicat_invertible_2cell _ _ δ). + - exact q. +Defined. + (** 4. Morphisms of internal Street opfibrations *) diff --git a/UniMath/Bicategories/Morphisms/Properties/ClosedUnderPullback.v b/UniMath/Bicategories/Morphisms/Properties/ClosedUnderPullback.v index d4247b1a7f..6bb377ce97 100644 --- a/UniMath/Bicategories/Morphisms/Properties/ClosedUnderPullback.v +++ b/UniMath/Bicategories/Morphisms/Properties/ClosedUnderPullback.v @@ -38,8 +38,8 @@ Definition pb_of_faithful_1cell {γ : invertible_2cell (p₁ · f) (p₂ · g)} (pb := make_pb_cone x₁ p₁ p₂ γ) (H : has_pb_ump pb) - (Hg : faithful_1cell g) - : faithful_1cell p₁. + (Hf : faithful_1cell f) + : faithful_1cell p₂. Proof. intros z h₁ h₂ α β p. use (pb_ump_eq @@ -65,19 +65,19 @@ Proof. apply idpath. - apply idpath. - apply idpath. - - exact (!p). - cbn. - use (faithful_1cell_eq_cell Hg). + use (faithful_1cell_eq_cell Hf). use (vcomp_lcancel (lassociator _ _ _)) ; [ is_iso | ]. rewrite !rwhisker_rwhisker. apply maponpaths_2. - use (vcomp_lcancel (_ ◃ γ)) ; [ is_iso ; apply property_from_invertible_2cell | ]. - rewrite <- !vcomp_whisker. - apply maponpaths_2. + use (vcomp_rcancel (_ ◃ γ)) ; [ is_iso ; apply property_from_invertible_2cell | ]. + rewrite !vcomp_whisker. + apply maponpaths. use (vcomp_rcancel (lassociator _ _ _)) ; [ is_iso | ]. rewrite <- !rwhisker_rwhisker. do 2 apply maponpaths. exact (!p). + - exact (!p). Qed. (** @@ -93,81 +93,81 @@ Section PbOfFullyFaithful. {γ : invertible_2cell (p₁ · f) (p₂ · g)} (pb := make_pb_cone x₁ p₁ p₂ γ) (H : has_pb_ump pb) - (Hg : fully_faithful_1cell g). + (Hf : fully_faithful_1cell f). Section Fullness. Context {z : B} {h₁ h₂ : z --> x₁} - (αf : h₁ · p₁ ==> h₂ · p₁). + (αf : h₁ · p₂ ==> h₂ · p₂). - Let ψ : h₁ · p₂ · g ==> h₂ · p₂ · g + Let ψ : h₁ · p₁ · f ==> h₂ · p₁ · f := rassociator _ _ _ - • (_ ◃ γ^-1) + • (_ ◃ γ) • lassociator _ _ _ • (αf ▹ _) • rassociator _ _ _ - • (_ ◃ γ) + • (_ ◃ γ^-1) • lassociator _ _ _. - Let ζ : h₁ · p₂ ==> h₂ · p₂ - := fully_faithful_1cell_inv_map Hg ψ. + Let ζ : h₁ · p₁ ==> h₂ · p₁ + := fully_faithful_1cell_inv_map Hf ψ. Local Lemma pb_of_fully_faithful_1cell_2cell_help_eq : (h₁ ◃ γ) • lassociator h₁ p₂ g - • (ζ ▹ g) + • (αf ▹ g) • rassociator h₂ p₂ g = lassociator h₁ p₁ f - • (αf ▹ f) + • (ζ ▹ f) • rassociator h₂ p₁ f • (h₂ ◃ γ). Proof. unfold ζ. rewrite fully_faithful_1cell_inv_map_eq. unfold ψ. + rewrite !vassocr. + rewrite lassociator_rassociator. + rewrite id2_left. rewrite !vassocl. + do 3 apply maponpaths. + refine (!(id2_right _) @ _). + apply maponpaths. + refine (!_). etrans. { apply maponpaths. rewrite !vassocr. rewrite lassociator_rassociator. - rewrite id2_left. - rewrite !vassocl. - apply idpath. + apply id2_left. } - rewrite !vassocr. rewrite lwhisker_vcomp. - rewrite vcomp_rinv. + rewrite vcomp_linv. rewrite lwhisker_id2. - rewrite id2_left. - rewrite !vassocl. - rewrite lassociator_rassociator. - rewrite id2_right. apply idpath. Qed. Definition pb_of_fully_faithful_1cell_2cell : h₁ ==> h₂. Proof. - use (pb_ump_cell H h₁ h₂ αf). + use (pb_ump_cell H h₁ h₂ _ αf). - exact ζ. - exact pb_of_fully_faithful_1cell_2cell_help_eq. Defined. Definition pb_of_fully_faithful_1cell_2cell_eq - : pb_of_fully_faithful_1cell_2cell ▹ p₁ = αf. + : pb_of_fully_faithful_1cell_2cell ▹ p₂ = αf. Proof. unfold pb_of_fully_faithful_1cell_2cell. - apply (pb_ump_cell_pr1 H). + apply (pb_ump_cell_pr2 H). Qed. End Fullness. Definition pb_of_fully_faithful_1cell - : fully_faithful_1cell p₁. + : fully_faithful_1cell p₂. Proof. use make_fully_faithful. - - exact (pb_of_faithful_1cell H (pr1 Hg)). + - exact (pb_of_faithful_1cell H (pr1 Hf)). - intros z h₁ h₂ αf. exact (pb_of_fully_faithful_1cell_2cell αf ,, @@ -188,25 +188,25 @@ Section PbOfConservative. {γ : invertible_2cell (p₁ · f) (p₂ · g)} (pb := make_pb_cone x₁ p₁ p₂ γ) (H : has_pb_ump pb) - (Hg : conservative_1cell g). + (Hf : conservative_1cell f). Section ReflectIso. Context {z : B} {h₁ h₂ : z --> x₁} {α : h₁ ==> h₂} - (Hα : is_invertible_2cell (α ▹ p₁)). + (Hα : is_invertible_2cell (α ▹ p₂)). Definition pb_reflect_iso_help - : is_invertible_2cell (α ▹ p₂). + : is_invertible_2cell (α ▹ p₁). Proof. - apply (Hg z (h₁ · p₂) (h₂ · p₂) (α ▹ p₂)). + apply (Hf z (h₁ · p₁) (h₂ · p₁) (α ▹ p₁)). use eq_is_invertible_2cell. - exact (rassociator _ _ _ - • (_ ◃ γ^-1) + • (_ ◃ γ) • lassociator _ _ _ - • ((α ▹ p₁) ▹ f) + • ((α ▹ p₂) ▹ g) • rassociator _ _ _ - • (_ ◃ γ) + • (_ ◃ γ^-1) • lassociator _ _ _). - abstract (rewrite !vassocl ; @@ -214,21 +214,23 @@ Section PbOfConservative. rewrite rwhisker_rwhisker ; rewrite !vassocr ; apply maponpaths_2 ; + use vcomp_move_R_Mp ; [ is_iso | ] ; cbn ; + rewrite vcomp_whisker ; rewrite !vassocl ; - use vcomp_move_R_pM ; [ is_iso | ] ; cbn ; - rewrite <- vcomp_whisker ; + apply maponpaths ; rewrite !vassocr ; - apply maponpaths_2 ; - rewrite !rwhisker_rwhisker ; + rewrite rwhisker_rwhisker ; rewrite !vassocl ; rewrite lassociator_rassociator ; apply id2_right). - use is_invertible_2cell_vcomp ; [ | is_iso ]. use is_invertible_2cell_vcomp ; [ | is_iso ; apply property_from_invertible_2cell ]. use is_invertible_2cell_vcomp ; [ | is_iso ]. - use is_invertible_2cell_vcomp ; [ is_iso | ]. - apply is_invertible_2cell_rwhisker. - exact Hα. + use is_invertible_2cell_vcomp. + + is_iso. + apply property_from_invertible_2cell . + + apply is_invertible_2cell_rwhisker. + exact Hα. Defined. Local Lemma pb_reflect_iso_eq @@ -270,8 +272,8 @@ Section PbOfConservative. (is_invertible_2cell_pb_ump_cell H pb_reflect_iso_eq - Hα - pb_reflect_iso_help)). + pb_reflect_iso_help + Hα)). use (pb_ump_eq H h₁ h₂ (α ▹ p₁) (α ▹ p₂)). - apply pb_reflect_iso_eq. - apply pb_ump_cell_pr1. @@ -282,7 +284,7 @@ Section PbOfConservative. End ReflectIso. Definition pb_of_conservative_1cell - : conservative_1cell p₁. + : conservative_1cell p₂. Proof. intros z h₁ h₂ α Hα. exact (pb_reflect_iso Hα). @@ -302,8 +304,8 @@ Definition pb_of_discrete_1cell {γ : invertible_2cell (p₁ · f) (p₂ · g)} (pb := make_pb_cone x₁ p₁ p₂ γ) (H : has_pb_ump pb) - (Hg : discrete_1cell g) - : discrete_1cell p₁. + (Hg : discrete_1cell f) + : discrete_1cell p₂. Proof. split. - exact (pb_of_faithful_1cell H (pr1 Hg)). diff --git a/UniMath/CONTENTS.md b/UniMath/CONTENTS.md index 2b02b29fea..443680f887 100644 --- a/UniMath/CONTENTS.md +++ b/UniMath/CONTENTS.md @@ -324,6 +324,7 @@ The packages and files are listed here in logical order: each file depends only - [DisplayedCats/Adjunctions.v](CategoryTheory/DisplayedCats/Adjunctions.v) - [DisplayedCats/ComprehensionC.v](CategoryTheory/DisplayedCats/ComprehensionC.v) - [DisplayedCats/StreetFibration.v](CategoryTheory/DisplayedCats/StreetFibration.v) + - [DisplayedCats/StreetOpFibration.v](CategoryTheory/DisplayedCats/StreetOpFibration.v) - [categories/Universal_Algebra/Algebras.v](CategoryTheory/categories/Universal_Algebra/Algebras.v) - [categories/Universal_Algebra/EqAlgebras.v](CategoryTheory/categories/Universal_Algebra/EqAlgebras.v) - [Monoidal/MonoidalCategories.v](CategoryTheory/Monoidal/MonoidalCategories.v) diff --git a/UniMath/CategoryTheory/.package/files b/UniMath/CategoryTheory/.package/files index 757aa01098..84fe10c3b1 100644 --- a/UniMath/CategoryTheory/.package/files +++ b/UniMath/CategoryTheory/.package/files @@ -206,6 +206,7 @@ DisplayedCats/FunctorCategory.v DisplayedCats/Adjunctions.v DisplayedCats/ComprehensionC.v DisplayedCats/StreetFibration.v +DisplayedCats/StreetOpFibration.v categories/Universal_Algebra/Algebras.v categories/Universal_Algebra/EqAlgebras.v diff --git a/UniMath/CategoryTheory/DisplayedCats/StreetFibration.v b/UniMath/CategoryTheory/DisplayedCats/StreetFibration.v index f87781351d..2cd194b853 100644 --- a/UniMath/CategoryTheory/DisplayedCats/StreetFibration.v +++ b/UniMath/CategoryTheory/DisplayedCats/StreetFibration.v @@ -678,3 +678,169 @@ Proof. rewrite iso_after_iso_inv. apply id_right. Qed. + +(** + Lemmas on cartesian cells for Street fibrations + *) +Definition is_cartesian_sfib_eq + {C₁ C₂ : category} + (F : C₁ ⟶ C₂) + {x₁ x₂ : C₁} + {f₁ f₂ : x₁ --> x₂} + (p : f₁ = f₂) + (Hf₁ : is_cartesian_sfib F f₁) + : is_cartesian_sfib F f₂. +Proof. + induction p. + exact Hf₁. +Defined. + +Definition iso_is_cartesian_sfib + {C₁ C₂ : category} + (F : C₁ ⟶ C₂) + {x₁ x₂ : C₁} + (i : x₁ --> x₂) + (Hi : is_iso i) + : is_cartesian_sfib F i. +Proof. + pose (i_iso := make_iso _ Hi). + intros w g h p. + use iscontraprop1. + - abstract + (use invproofirrelevance ; + intros φ₁ φ₂ ; + use subtypePath ; [ intro ; apply isapropdirprod ; apply homset_property | ] ; + refine (!(id_right _) @ _ @ id_right _) ; + rewrite <- (iso_inv_after_iso i_iso) ; + cbn ; + rewrite !assoc ; + rewrite (pr22 φ₁), (pr22 φ₂) ; + apply idpath). + - simple refine (_ ,, _ ,, _). + + exact (g · inv_from_iso i_iso). + + abstract + (rewrite functor_comp ; + rewrite p ; + rewrite !assoc' ; + rewrite <- functor_comp ; + etrans ; + [ do 2 apply maponpaths ; + exact (iso_inv_after_iso i_iso) + | ] ; + rewrite functor_id ; + apply id_right). + + abstract + (cbn ; + rewrite !assoc' ; + refine (_ @ id_right _) ; + apply maponpaths ; + apply iso_after_iso_inv). +Defined. + +Section CompositionCartesian. + Context {C₁ C₂ : category} + (F : C₁ ⟶ C₂) + {x₁ x₂ x₃ : C₁} + {f : x₁ --> x₂} + (Hf : is_cartesian_sfib F f) + {g : x₂ --> x₃} + (Hg : is_cartesian_sfib F g). + + Section Factorization. + Context {w : C₁} + {h₁ : w --> x₃} + {h₂ : F w --> F x₁} + (p : # F h₁ = h₂ · # F (f · g)). + + Definition comp_is_cartesian_sfib_factor_help + : w --> x₂. + Proof. + use (cartesian_factorization_sfib + _ Hg + h₁ (h₂ · #F f)). + abstract + (refine (p @ _) ; + rewrite functor_comp ; + rewrite assoc ; + apply idpath). + Defined. + + Definition comp_is_cartesian_sfib_factor + : w --> x₁. + Proof. + use (cartesian_factorization_sfib _ Hf). + - exact comp_is_cartesian_sfib_factor_help. + - exact h₂. + - apply cartesian_factorization_sfib_over. + Defined. + + Definition comp_is_cartesian_sfib_factor_over + : # F comp_is_cartesian_sfib_factor = h₂. + Proof. + apply cartesian_factorization_sfib_over. + Qed. + + Definition comp_is_cartesian_sfib_factor_comm + : comp_is_cartesian_sfib_factor · (f · g) = h₁. + Proof. + unfold comp_is_cartesian_sfib_factor, comp_is_cartesian_sfib_factor_help. + rewrite !assoc. + rewrite !cartesian_factorization_sfib_commute. + apply idpath. + Qed. + + Definition comp_is_cartesian_sfib_factor_unique + : isaprop (∑ φ, # F φ = h₂ × φ · (f · g) = h₁). + Proof. + use invproofirrelevance. + intros φ₁ φ₂. + use subtypePath. + { + intro. + apply isapropdirprod ; apply homset_property. + } + use (cartesian_factorization_sfib_unique + _ Hf + comp_is_cartesian_sfib_factor_help h₂). + - apply cartesian_factorization_sfib_over. + - exact (pr12 φ₁). + - exact (pr12 φ₂). + - use (cartesian_factorization_sfib_unique _ Hg h₁ (h₂ · #F f)). + + rewrite p. + rewrite functor_comp. + rewrite !assoc. + apply idpath. + + rewrite functor_comp. + rewrite (pr12 φ₁). + apply idpath. + + apply cartesian_factorization_sfib_over. + + rewrite assoc'. + apply (pr22 φ₁). + + apply cartesian_factorization_sfib_commute. + - use (cartesian_factorization_sfib_unique _ Hg h₁ (h₂ · #F f)). + + rewrite p. + rewrite functor_comp. + rewrite !assoc. + apply idpath. + + rewrite functor_comp. + rewrite (pr12 φ₂). + apply idpath. + + apply cartesian_factorization_sfib_over. + + rewrite assoc'. + apply (pr22 φ₂). + + apply cartesian_factorization_sfib_commute. + Qed. + End Factorization. + + Definition comp_is_cartesian_sfib + : is_cartesian_sfib F (f · g). + Proof. + intros w h₁ h₂ p. + use iscontraprop1. + - exact (comp_is_cartesian_sfib_factor_unique p). + - simple refine (_ ,, _ ,, _). + + exact (comp_is_cartesian_sfib_factor p). + + exact (comp_is_cartesian_sfib_factor_over p). + + exact (comp_is_cartesian_sfib_factor_comm p). + Defined. +End CompositionCartesian. diff --git a/UniMath/CategoryTheory/DisplayedCats/StreetOpFibration.v b/UniMath/CategoryTheory/DisplayedCats/StreetOpFibration.v new file mode 100644 index 0000000000..4c2b4c8cea --- /dev/null +++ b/UniMath/CategoryTheory/DisplayedCats/StreetOpFibration.v @@ -0,0 +1,488 @@ +Require Import UniMath.Foundations.All. +Require Import UniMath.MoreFoundations.All. +Require Import UniMath.CategoryTheory.Core.Categories. +Require Import UniMath.CategoryTheory.Core.Isos. +Require Import UniMath.CategoryTheory.Core.Univalence. +Require Import UniMath.CategoryTheory.Core.Functors. +Require Import UniMath.CategoryTheory.Core.NaturalTransformations. +Require Import UniMath.CategoryTheory.DisplayedCats.Core. +Require Import UniMath.CategoryTheory.DisplayedCats.Total. +Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. + +Local Open Scope cat. + +Lemma idtoiso_functor_precompose' + {C₁ C₂ : category} + (F : C₁ ⟶ C₂) + {y : C₂} + {x₁ x₂ : C₁} + (p : x₁ = x₂) + (f : y --> F x₁) + : f · idtoiso (maponpaths (λ z, F z) p) + = + transportf (λ z, y --> F z) p f. +Proof. + induction p. + cbn. + apply id_right. +Qed. + +Definition transportf_functor_isotoid' + {C₁ C₂ : category} + (HC₁ : is_univalent C₁) + (F : C₁ ⟶ C₂) + {y : C₂} + {x₁ x₂ : C₁} + (i : iso x₁ x₂) + (f : y --> F x₁) + : transportf + (λ z, y --> F z) + (isotoid _ HC₁ i) + f + = + f · #F i. +Proof. + rewrite <- idtoiso_functor_precompose'. + rewrite maponpaths_idtoiso. + rewrite idtoiso_isotoid. + apply idpath. +Qed. + + +(** +The definition of a Street opfibration of categories + *) +Section StreetOpFibration. + Context {E B : category} + (F : E ⟶ B). + + Definition is_opcartesian_sopfib + {e₁ e₂ : E} + (f : e₁--> e₂) + : UU + := ∏ (e₃ : E) + (g : e₁ --> e₃) + (h : F e₂ --> F e₃) + (p : #F g = #F f · h), + ∃! (φ : e₂ --> e₃), + #F φ = h + × + f · φ = g. + + Definition isaprop_is_opcartesian_sopfib + {e₁ e₂ : E} + (f : e₁--> e₂) + : isaprop (is_opcartesian_sopfib f). + Proof. + do 4 (apply impred ; intro). + apply isapropiscontr. + Qed. + + Definition opcartesian_factorization_sopfib + {e₁ e₂ : E} + {f : e₁--> e₂} + (Hf : is_opcartesian_sopfib f) + {e₃ : E} + (g : e₁ --> e₃) + (h : F e₂ --> F e₃) + (p : #F g = #F f · h) + : e₂ --> e₃ + := pr11 (Hf e₃ g h p). + + Definition opcartesian_factorization_sopfib_over + {e₁ e₂ : E} + {f : e₁--> e₂} + (Hf : is_opcartesian_sopfib f) + {e₃ : E} + (g : e₁ --> e₃) + (h : F e₂ --> F e₃) + (p : #F g = #F f · h) + : #F (opcartesian_factorization_sopfib Hf g h p) = h + := pr121 (Hf e₃ g h p). + + Definition opcartesian_factorization_sopfib_commute + {e₁ e₂ : E} + {f : e₁--> e₂} + (Hf : is_opcartesian_sopfib f) + {e₃ : E} + (g : e₁ --> e₃) + (h : F e₂ --> F e₃) + (p : #F g = #F f · h) + : f · opcartesian_factorization_sopfib Hf g h p = g + := pr221 (Hf e₃ g h p). + + Definition opcartesian_factorization_sopfib_unique + {e₁ e₂ : E} + {f : e₁--> e₂} + (Hf : is_opcartesian_sopfib f) + {e₃ : E} + (g : e₁ --> e₃) + (h : F e₂ --> F e₃) + (p : #F g = #F f · h) + (φ₁ φ₂ : e₂ --> e₃) + (p₁ : #F φ₁ = h) + (p₂ : #F φ₂ = h) + (q₁ : f · φ₁ = g) + (q₂ : f · φ₂ = g) + : φ₁ = φ₂. + Proof. + exact (maponpaths + pr1 + (proofirrelevance + _ + (isapropifcontr (Hf e₃ g h p)) + (φ₁ ,, p₁ ,, q₁) + (φ₂ ,, p₂ ,, q₂))). + Defined. + + Definition street_opfib + : UU + := ∏ (e : E) + (b : B) + (f : F e --> b), + ∑ (bb : E) + (ff_i : e --> bb × iso b (F bb)), + # F (pr1 ff_i) = f · pr2 ff_i + × + is_opcartesian_sopfib (pr1 ff_i). +End StreetOpFibration. + +(** + *) +Definition lift_unique_sopfib_map + {E B : category} + (F : E ⟶ B) + {e : E} + {b : B} + (f : F e --> b) + (bb₁ bb₂ : E) + (ff₁ : e --> bb₁) + (β₁ : iso b (F bb₁)) + (ff₂ : e --> bb₂) + (β₂ : iso b (F bb₂)) + (over₁ : # F (ff₁) = f · β₁) + (over₂ : # F (ff₂) = f · β₂) + (cart₁ : is_opcartesian_sopfib F ff₁) + (cart₂ : is_opcartesian_sopfib F ff₂) + : bb₁ --> bb₂. +Proof. + use (opcartesian_factorization_sopfib F cart₁ ff₂ (inv_from_iso β₁ · β₂) _). + abstract + (rewrite over₁, over₂ ; + rewrite !assoc' ; + apply maponpaths ; + rewrite !assoc ; + rewrite iso_inv_after_iso ; + rewrite id_left ; + apply idpath). +Defined. + +Section UniqueLifts. + Context {E B : category} + (F : E ⟶ B) + {e : E} + {b : B} + (f : F e --> b) + (bb₁ bb₂ : E) + (ff₁ : e --> bb₁) + (β₁ : iso b (F bb₁)) + (ff₂ : e --> bb₂) + (β₂ : iso b (F bb₂)) + (over₁ : # F (ff₁) = f · β₁) + (over₂ : # F (ff₂) = f · β₂) + (cart₁ : is_opcartesian_sopfib F ff₁) + (cart₂ : is_opcartesian_sopfib F ff₂). + + Let ζ : bb₁ --> bb₂ + := lift_unique_sopfib_map F f bb₁ bb₂ ff₁ β₁ ff₂ β₂ over₁ over₂ cart₁ cart₂. + Let ζinv : bb₂ --> bb₁ + := lift_unique_sopfib_map F f bb₂ bb₁ ff₂ β₂ ff₁ β₁ over₂ over₁ cart₂ cart₁. + + Local Lemma lift_unique_sopfib_inv₁ + : ζ · ζinv = identity bb₁. + Proof. + unfold ζ, ζinv, lift_unique_sopfib_map. + use (opcartesian_factorization_sopfib_unique + F + cart₁ + ff₁ + (identity _)). + - rewrite id_right. + apply idpath. + - rewrite functor_comp. + rewrite !opcartesian_factorization_sopfib_over. + rewrite !assoc'. + rewrite !(maponpaths (λ z, _ · z) (assoc _ _ _)). + rewrite iso_inv_after_iso. + rewrite id_left. + rewrite iso_after_iso_inv. + apply idpath. + - apply functor_id. + - rewrite !assoc. + rewrite !opcartesian_factorization_sopfib_commute. + apply idpath. + - apply id_right. + Qed. + + Local Lemma lift_unique_sopfib_inv₂ + : ζinv · ζ = identity bb₂. + Proof. + unfold ζ, ζinv, lift_unique_sopfib_map. + use (opcartesian_factorization_sopfib_unique + F + cart₂ + ff₂ + (identity _)). + - rewrite id_right. + apply idpath. + - rewrite functor_comp. + rewrite !opcartesian_factorization_sopfib_over. + rewrite !assoc'. + rewrite !(maponpaths (λ z, _ · z) (assoc _ _ _)). + rewrite iso_inv_after_iso. + rewrite id_left. + rewrite iso_after_iso_inv. + apply idpath. + - apply functor_id. + - rewrite !assoc. + rewrite !opcartesian_factorization_sopfib_commute. + apply idpath. + - apply id_right. + Qed. + + Definition lift_unique_sopfib + : iso bb₁ bb₂. + Proof. + use make_iso. + - exact ζ. + - use is_iso_qinv. + + exact ζinv. + + split. + * exact lift_unique_sopfib_inv₁. + * exact lift_unique_sopfib_inv₂. + Defined. +End UniqueLifts. + +(** The type of Street opfibrations is a proposition *) +Definition isaprop_street_opfib + {B E : category} + (HE : is_univalent E) + (F : E ⟶ B) + : isaprop (street_opfib F). +Proof. + use impred ; intro e. + use impred ; intro b. + use impred ; intro f. + use invproofirrelevance. + intros φ₁ φ₂. + use total2_paths_f. + - apply (isotoid _ HE). + exact (lift_unique_sopfib + F f + (pr1 φ₁) (pr1 φ₂) + (pr112 φ₁) (pr212 φ₁) + (pr112 φ₂) (pr212 φ₂) + (pr122 φ₁) (pr122 φ₂) + (pr222 φ₁) (pr222 φ₂)). + - use subtypePath. + { + intro. + apply isapropdirprod ; + [ apply homset_property + | apply isaprop_is_opcartesian_sopfib ]. + } + rewrite pr1_transportf. + use dirprod_paths. + + etrans. + { + apply (@pr1_transportf E (λ x, e --> x) (λ x _, iso _ (F x))). + } + rewrite transportf_isotoid'. + apply opcartesian_factorization_sopfib_commute. + + rewrite pr2_transportf. + use subtypePath. + { + intro. + apply isaprop_is_iso. + } + unfold iso. + rewrite pr1_transportf. + rewrite transportf_functor_isotoid'. + etrans. + { + apply maponpaths. + apply opcartesian_factorization_sopfib_over. + } + rewrite !assoc. + etrans. + { + apply maponpaths_2. + apply iso_inv_after_iso. + } + apply id_left. +Qed. + +(** + Lemmas on opcartesian cells for Street fibrations + *) +Definition is_opcartesian_sopfib_eq + {C₁ C₂ : category} + (F : C₁ ⟶ C₂) + {x₁ x₂ : C₁} + {f₁ f₂ : x₁ --> x₂} + (p : f₁ = f₂) + (Hf₁ : is_opcartesian_sopfib F f₁) + : is_opcartesian_sopfib F f₂. +Proof. + induction p. + exact Hf₁. +Defined. + +Definition iso_is_opcartesian_sopfib + {C₁ C₂ : category} + (F : C₁ ⟶ C₂) + {x₁ x₂ : C₁} + (i : x₁ --> x₂) + (Hi : is_iso i) + : is_opcartesian_sopfib F i. +Proof. + pose (i_iso := make_iso _ Hi). + intros w g h p. + use iscontraprop1. + - abstract + (use invproofirrelevance ; + intros φ₁ φ₂ ; + use subtypePath ; [ intro ; apply isapropdirprod ; apply homset_property | ] ; + refine (!(id_left _) @ _ @ id_left _) ; + rewrite <- (iso_after_iso_inv i_iso) ; + cbn ; + rewrite !assoc' ; + rewrite (pr22 φ₁), (pr22 φ₂) ; + apply idpath). + - simple refine (_ ,, _ ,, _). + + exact (inv_from_iso i_iso · g). + + abstract + (rewrite functor_comp ; + rewrite p ; + rewrite !assoc ; + rewrite <- functor_comp ; + etrans ; + [ apply maponpaths_2 ; + apply maponpaths ; + exact (iso_after_iso_inv i_iso) + | ] ; + rewrite functor_id ; + apply id_left). + + abstract + (cbn ; + rewrite !assoc ; + refine (_ @ id_left _) ; + apply maponpaths_2 ; + exact (iso_inv_after_iso i_iso)). +Defined. + +Section CompositionOpCartesian. + Context {C₁ C₂ : category} + (F : C₁ ⟶ C₂) + {x₁ x₂ x₃ : C₁} + {f : x₁ --> x₂} + (Hf : is_opcartesian_sopfib F f) + {g : x₂ --> x₃} + (Hg : is_opcartesian_sopfib F g). + + Section Factorization. + Context {w : C₁} + {h₁ : x₁ --> w} + {h₂ : F x₃ --> F w} + (p : # F h₁ = # F (f · g) · h₂). + + Definition comp_is_opcartesian_sopfib_factor_help + : x₂ --> w. + Proof. + use (opcartesian_factorization_sopfib _ Hf h₁ (#F g · h₂)). + abstract + (refine (p @ _) ; + rewrite functor_comp ; + rewrite !assoc ; + apply idpath). + Defined. + + Definition comp_is_opcartesian_sopfib_factor + : x₃ --> w. + Proof. + use (opcartesian_factorization_sopfib _ Hg). + - exact comp_is_opcartesian_sopfib_factor_help. + - exact h₂. + - apply opcartesian_factorization_sopfib_over. + Defined. + + Definition comp_is_opcartesian_sopfib_factor_over + : # F comp_is_opcartesian_sopfib_factor = h₂. + Proof. + apply opcartesian_factorization_sopfib_over. + Qed. + + Definition comp_is_opcartesian_sopfib_factor_comm + : f · g · comp_is_opcartesian_sopfib_factor = h₁. + Proof. + unfold comp_is_opcartesian_sopfib_factor, comp_is_opcartesian_sopfib_factor_help. + rewrite !assoc'. + rewrite !opcartesian_factorization_sopfib_commute. + apply idpath. + Qed. + + Definition comp_is_opcartesian_sopfib_factor_unique + : isaprop (∑ φ, # F φ = h₂ × f · g · φ = h₁). + Proof. + use invproofirrelevance. + intros φ₁ φ₂. + use subtypePath. + { + intro. + apply isapropdirprod ; apply homset_property. + } + use (opcartesian_factorization_sopfib_unique + _ Hg + comp_is_opcartesian_sopfib_factor_help h₂). + - apply opcartesian_factorization_sopfib_over. + - exact (pr12 φ₁). + - exact (pr12 φ₂). + - use (opcartesian_factorization_sopfib_unique _ Hf h₁ (#F g · h₂)). + + rewrite p. + rewrite functor_comp. + rewrite !assoc. + apply idpath. + + rewrite functor_comp. + rewrite (pr12 φ₁). + apply idpath. + + apply opcartesian_factorization_sopfib_over. + + rewrite assoc. + apply (pr22 φ₁). + + apply opcartesian_factorization_sopfib_commute. + - use (opcartesian_factorization_sopfib_unique _ Hf h₁ (#F g · h₂)). + + rewrite p. + rewrite functor_comp. + rewrite !assoc. + apply idpath. + + rewrite functor_comp. + rewrite (pr12 φ₂). + apply idpath. + + apply opcartesian_factorization_sopfib_over. + + rewrite assoc. + apply (pr22 φ₂). + + apply opcartesian_factorization_sopfib_commute. + Qed. + End Factorization. + + Definition comp_is_opcartesian_sopfib + : is_opcartesian_sopfib F (f · g). + Proof. + intros w h₁ h₂ p. + use iscontraprop1. + - exact (comp_is_opcartesian_sopfib_factor_unique p). + - simple refine (_ ,, _ ,, _). + + exact (comp_is_opcartesian_sopfib_factor p). + + exact (comp_is_opcartesian_sopfib_factor_over p). + + exact (comp_is_opcartesian_sopfib_factor_comm p). + Defined. +End CompositionOpCartesian.