Merge pull request #171 from UniMath/revert-169-AKLV/direct-surjective

Revert "Another proof that reluniv_functor_with_ess_surj issurjective (assuming R is essentially surjective)"

Author: benediktahrens

TypeTheory/ALV2/RelUnivTransfer.v

@@ -28,7 +28,6 @@ Require Import TypeTheory.ALV1.Transport_along_Equivs.
 Require Import TypeTheory.ALV2.RelUniv_Cat_Simple.
 Require Import TypeTheory.ALV2.RelUniv_Cat.
 Require Import UniMath.CategoryTheory.catiso.
-Require Import UniMath.CategoryTheory.Equivalences.Core.
 
 Set Automatic Introduction.
 
@@ -333,293 +332,6 @@ Section RelUniv_Transfer.
       - apply reluniv_functor_with_ess_surj_is_faithful, S_faithful.
     Defined.
 
-  Section Surjective_if_R_split_ess_surj.
-    Context (R_ses : split_ess_surj R)
-            (D'_univ : is_univalent D')
-            (invS : functor D' D)
-            (eta : iso (C:=[D, D, pr2 D]) (functor_identity D) (S ∙ invS))
-            (eps : iso (C:=[D', D', pr2 D']) (invS ∙ S) (functor_identity D'))
-            (S_ff : fully_faithful S).
-
-    Let E := ((S,, (invS,, (pr1 eta, pr1 eps)))
-                ,, ((λ d,  (pr2 (Constructions.pointwise_iso_from_nat_iso eta d )))
-                    , (λ d', (pr2 (Constructions.pointwise_iso_from_nat_iso eps d')))))
-            : equivalence_of_precats D D'.
-
-    Let AE := adjointificiation E.
-    Let η' := pr1 (pr121 AE) : nat_trans (functor_identity _) (S ∙ invS).
-    Let ε' := pr2 (pr121 AE) : nat_trans (invS ∙ S) (functor_identity _).
-    Let η := functor_iso_from_pointwise_iso
-                _ _ _ _ _ η' (pr12 (adjointificiation E))
-            : iso (C:=[D, D, pr2 D]) (functor_identity D) (S ∙ invS).
-    Let ε := functor_iso_from_pointwise_iso
-                _ _ _ _ _ ε' (pr22 (adjointificiation E))
-            : iso (C:=[D', D', pr2 D']) (invS ∙ S) (functor_identity D').
-
-    Let ηx := Constructions.pointwise_iso_from_nat_iso (iso_inv_from_iso η).
-    Let αx := Constructions.pointwise_iso_from_nat_iso (α,,α_is_iso).
-
-  Section Helpers.
-
-    Context (u' : reluniv_cat J').
-
-    Let p' := pr1  u' : mor_total D'.
-    Let Ũ' := pr21 p' : D'.
-    Let U' := pr11 p' : D'.
-    Let pf' := pr2 p' : D' ⟦ Ũ', U' ⟧.
-
-    Let U := invS U'.
-    Let Ũ := invS Ũ'.
-    Let pf := # invS pf'.
-    Local Definition p := functor_on_mor_total invS p' : mor_total D.
-
-    Context (X : C) (f : D ⟦ J X, U ⟧).
-
-    Let X' := R X : C'.
-    Let f' := inv_from_iso (αx X) ;; # S f ;; pr11 ε U'
-              : D' ⟦ J' X' , U' ⟧.
-    Let pb' := pr2 u' X' f' : fpullback J' p' f'.
-    Let Xf' := pr11 pb'.
-
-    Local Definition Xf := pr1 (R_ses Xf') : C.
-    Let RXf_Xf'_iso := pr2 (R_ses Xf') : iso (R Xf) Xf'.
-
-    Let pp' := pr121 pb' : C' ⟦ Xf', X' ⟧.
-    Local Definition pp : C ⟦ Xf, X ⟧.
-    Proof.
-      use (invweq (weq_from_fully_faithful ff_J _ _)).
-      use (pr11 η _ ;; _ ;; pr1 (inv_from_iso η) _).
-      use (# invS _).
-      apply (pr1 α Xf ;; # J' (RXf_Xf'_iso ;; pp') ;; inv_from_iso (αx X)).
-    Defined.
-
-    Let Q' := pr221 pb' : D' ⟦ J' Xf', Ũ' ⟧.
-    Local Definition Q
-      := pr11 η _ ;; # invS (pr1 α Xf ;; # J' RXf_Xf'_iso ;; Q')
-         : D ⟦ J Xf, invS Ũ' ⟧.
-
-    Let pb'_commutes := pr12 pb' : # J' pp' ;; f' = Q' ;; p'.
-    Let pb'_isPullback := pr22 pb'.
-
-    Local Definition pb_commutes_and_is_pullback
-      : commutes_and_is_pullback f p (# J pp) Q.
-    Proof.
-      Check @commutes_and_is_pullback_transfer_iso.
-      use (@commutes_and_is_pullback_transfer_iso
-               _ _ _ _ _
-               _ _ _ _
-               _ _ _ (J Xf)
-               f p (# J pp) Q
-               _ _ _ _
-               _ _ _ _
-               (functor_on_square _ _ invS pb'_commutes)
-            ).
-      - apply identity_iso.
-      - eapply iso_comp.
-        apply functor_on_iso, iso_inv_from_iso, αx.
-        apply ηx.
-      - apply identity_iso.
-      - eapply iso_comp. apply functor_on_iso, functor_on_iso.
-        apply iso_inv_from_iso, RXf_Xf'_iso.
-        eapply iso_comp. apply functor_on_iso, iso_inv_from_iso, αx.
-        apply ηx.
-      - unfold f', iso_comp.
-
-        etrans. apply id_right.
-        etrans. apply functor_comp.
-        etrans. apply maponpaths_2, functor_comp.
-        etrans. apply assoc'.
-        apply pathsinv0.
-        etrans. apply assoc'.
-        apply maponpaths.
-
-        etrans. apply pathsinv0.
-        apply (nat_trans_ax (inv_from_iso η)).
-        apply maponpaths.
-
-        apply pathsinv0.
-        etrans. apply pathsinv0, id_left.
-        etrans. apply maponpaths_2, pathsinv0.
-        apply (maponpaths (λ k, pr1 k (invS U'))
-                          (iso_after_iso_inv η)).
-
-        etrans. apply assoc'.
-        etrans. apply maponpaths.
-        set (AE_tr2 := pr2 (pr221 AE) U'
-                       : pr11 η (invS U') ;; # invS (pr11 ε U')
-                         = identity _).
-        apply AE_tr2.
-        apply id_right.
-
-      - etrans. apply id_right.
-        apply pathsinv0, id_left.
-
-      - apply pathsinv0.
-        etrans. apply maponpaths.
-        apply (homotweqinvweq (weq_from_fully_faithful ff_J _ _)). (*  *)
-
-        etrans. apply maponpaths, assoc'.
-        etrans. apply maponpaths, maponpaths, maponpaths_2.
-        apply (functor_comp invS).
-        etrans. apply maponpaths, maponpaths, assoc'.
-        etrans. apply assoc.
-        etrans. apply assoc.
-        apply maponpaths_2.
-
-        unfold iso_comp, functor_on_iso. simpl.
-        etrans. apply maponpaths_2, maponpaths_2, maponpaths, maponpaths.
-        apply id_right.
-        etrans. apply maponpaths_2, assoc'.
-        etrans. apply maponpaths_2, maponpaths, assoc'.
-        etrans. apply maponpaths_2, maponpaths, maponpaths.
-        apply iso_after_iso_inv.
-
-        etrans. apply maponpaths_2, maponpaths, id_right.
-        etrans. apply maponpaths, functor_comp.
-        etrans. apply assoc.
-        etrans. apply maponpaths_2, assoc'.
-        etrans. apply maponpaths_2, maponpaths.
-        apply pathsinv0, functor_comp.
-        etrans. apply maponpaths_2, maponpaths, maponpaths.
-        apply iso_after_iso_inv.
-
-        etrans. apply maponpaths_2, pathsinv0, functor_comp.
-        etrans. apply pathsinv0, functor_comp.
-        apply maponpaths.
-
-        etrans. apply maponpaths_2, id_right.
-        etrans. apply pathsinv0, functor_comp.
-        apply maponpaths.
-        
-        etrans. apply assoc.
-        etrans. apply maponpaths_2, iso_after_iso_inv.
-        apply id_left.
-
-      - etrans. apply id_right.
-        apply pathsinv0.
-
-        unfold Q, iso_comp, functor_on_iso. simpl.
-
-        etrans. apply maponpaths_2, maponpaths, maponpaths.
-        apply id_right.
-
-        etrans. apply assoc.
-        etrans. apply maponpaths_2, assoc'.
-        etrans. apply maponpaths_2, maponpaths, assoc'.
-        etrans. apply maponpaths_2, maponpaths, maponpaths.
-        apply iso_after_iso_inv.
-
-        etrans. apply maponpaths_2, maponpaths.
-        apply id_right.
-
-        etrans. apply maponpaths, functor_comp.
-        etrans. apply assoc.
-        etrans. apply maponpaths_2, assoc'.
-        etrans. apply maponpaths_2, maponpaths, maponpaths, functor_comp.
-        etrans. apply maponpaths_2, maponpaths, assoc.
-        etrans. apply maponpaths_2, maponpaths, maponpaths_2.
-        apply pathsinv0, functor_comp.
-        etrans. apply maponpaths_2, maponpaths, maponpaths_2.
-        apply maponpaths, iso_after_iso_inv.
-
-        etrans. apply maponpaths_2, maponpaths.
-        apply pathsinv0, functor_comp.
-        etrans. apply maponpaths_2, maponpaths.
-        apply maponpaths, id_left.
-
-        etrans. apply maponpaths_2, pathsinv0, functor_comp.
-        etrans. apply pathsinv0, functor_comp.
-        apply maponpaths.
-
-        etrans. apply maponpaths_2, pathsinv0, functor_comp.
-        etrans. apply maponpaths_2, maponpaths, iso_after_iso_inv.
-        etrans. apply maponpaths_2, functor_id.
-        apply id_left.
-
-     - use (isPullback_image_square _ _ invS).
-       + apply homset_property.
-       + apply (right_adj_equiv_is_ff _ _ S AE).
-       + apply (right_adj_equiv_is_ess_sur _ _ S AE).
-       + apply pb'_isPullback.
-    Defined.
-
-  End Helpers.
-
-    Definition inv_reluniv_with_ess_surj
-      : reluniv_cat J' → reluniv_cat J.
-    Proof.
-      intros u'.
-      use tpair.
-      + apply (p u').
-      + intros X f.
-        use tpair.
-        * use tpair.
-          -- apply (Xf u' X f).
-          -- use make_dirprod.
-             ++ apply pp.
-             ++ apply Q.
-        * apply pb_commutes_and_is_pullback.
-    Defined.
-
-    Definition reluniv_functor_with_ess_surj_after_inv_iso
-               (u' : reluniv_cat J')
-      : iso u'
-            (reluniv_functor_with_ess_surj (inv_reluniv_with_ess_surj u')).
-    Proof.
-      set (εx := Constructions.pointwise_iso_from_nat_iso ε).
-      set (εx' := Constructions.pointwise_iso_from_nat_iso
-                   (iso_inv_from_iso ε)).
-      use z_iso_to_iso.
-      use make_z_iso.
-      - use tpair.
-        + use make_dirprod.
-          * cbn. apply (εx' (pr211 u')).
-          * cbn. apply (εx' (pr111 u')).
-        + unfold is_gen_reluniv_mor.
-          etrans. apply pathsinv0.
-          apply (nat_trans_ax (pr1 (iso_inv_from_iso ε))).
-          apply idpath.
-      - use tpair.
-        + use make_dirprod.
-          * cbn. apply (εx (pr211 u')).
-          * cbn. apply (εx (pr111 u')).
-        + unfold is_gen_reluniv_mor.
-          etrans. apply pathsinv0.
-          apply (nat_trans_ax (pr1 ε)).
-          apply idpath.
-      - use make_dirprod.
-        + use gen_reluniv_mor_eq.
-          * apply (maponpaths (λ k, pr1 k _) (iso_after_iso_inv ε)).
-          * apply (maponpaths (λ k, pr1 k _) (iso_after_iso_inv ε)).
-        + use gen_reluniv_mor_eq.
-          * apply (maponpaths (λ k, pr1 k _) (iso_inv_after_iso ε)).
-          * apply (maponpaths (λ k, pr1 k _) (iso_inv_after_iso ε)).
-    Defined.
-
-    Definition reluniv_functor_with_ess_surj_after_inv_id
-               (u' : reluniv_cat J')
-      : u' = reluniv_functor_with_ess_surj (inv_reluniv_with_ess_surj u').
-    Proof.
-      use isotoid.
-      - use reluniv_cat_is_univalent.
-        + apply C'_univ.
-        + apply ff_J'.
-        + apply D'_univ.
-      - apply reluniv_functor_with_ess_surj_after_inv_iso.
-    Defined.
-
-    Definition reluniv_functor_with_ess_surj_issurjective
-      : issurjective reluniv_functor_with_ess_surj.
-    Proof.
-      intros u'.
-      use hinhpr.
-      use tpair.
-      - apply (inv_reluniv_with_ess_surj u').
-      - apply pathsinv0, reluniv_functor_with_ess_surj_after_inv_id.
-    Defined.
-
-  End Surjective_if_R_split_ess_surj.
-
   End RelUniv_Transfer_with_ess_surj.
 
 End RelUniv_Transfer.
@@ -829,29 +541,29 @@ Section WeakRelUniv_Transfer.
     apply weak_relu_square_commutes.
   Defined.
 
-  Definition reluniv_functor_with_ess_surj_issurjective_AC
-              (C'_univ : is_univalent C')		
-              (AC : AxiomOfChoice.AxiomOfChoice)		
-              (obC_isaset : isaset C)		
-     : issurjective (reluniv_functor_with_ess_surj		
-                       _ _ _ _ J J'		
-                       R S α α_is_iso		
-                       S_pb C'_univ ff_J' S_full R_es		
-                    ).		
-   Proof.		
-     set (W := (weak_from_reluniv_functor J'		
-             ,, weak_from_reluniv_functor_is_catiso J' C'_univ ff_J')		
-         : catiso _ _).		
-     use (Core.issurjective_postcomp_with_weq _ (catiso_ob_weq W)).		
-     use (transportf (λ F, issurjective (pr11 F))		
-                     (! weak_relu_square_commutes_strictly C'_univ)).		
-     use issurjcomp.		
-     - apply weak_from_reluniv_functor_issurjective.		
-       apply AC.		
-       apply obC_isaset.		
-     - apply issurjectiveweq.		
-       apply (catiso_ob_weq (_,,weak_reluniv_functor_is_catiso)).		
-   Defined.
+  Definition reluniv_functor_with_ess_surj_issurjective
+             (C'_univ : is_univalent C')
+             (AC : AxiomOfChoice.AxiomOfChoice)
+             (obC_isaset : isaset C)
+    : issurjective (reluniv_functor_with_ess_surj
+                      _ _ _ _ J J'
+                      R S α α_is_iso
+                      S_pb C'_univ ff_J' S_full R_es
+                   ).
+  Proof.
+    set (W := (weak_from_reluniv_functor J'
+            ,, weak_from_reluniv_functor_is_catiso J' C'_univ ff_J')
+        : catiso _ _).
+    use (Core.issurjective_postcomp_with_weq _ (catiso_ob_weq W)).
+    use (transportf (λ F, issurjective (pr11 F))
+                    (! weak_relu_square_commutes_strictly C'_univ)).
+    use issurjcomp.
+    - apply weak_from_reluniv_functor_issurjective.
+      apply AC.
+      apply obC_isaset.
+    - apply issurjectiveweq.
+      apply (catiso_ob_weq (_,,weak_reluniv_functor_is_catiso)).
+  Defined.
 
 End WeakRelUniv_Transfer.
 
@@ -902,9 +614,10 @@ Section RelUniv_Yo_Rezk.
              (obC_isaset : isaset C)
     : issurjective transfer_of_RelUnivYoneda_functor.
   Proof.
-    use (reluniv_functor_with_ess_surj_issurjective_AC
+    use (reluniv_functor_with_ess_surj_issurjective
            _ _ _ _ Yo Yo
            _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
+           AC obC_isaset
         ).
     - apply is_univalent_preShv.
     - apply is_univalent_preShv.
@@ -914,8 +627,6 @@ Section RelUniv_Yo_Rezk.
     - apply fully_faithful_implies_full_and_faithful.
       apply right_adj_equiv_is_ff.
     - apply R_full.
-    - apply AC.
-    - apply obC_isaset.
   Defined.
 
   Definition transfer_of_WeakRelUnivYoneda_functor
@@ -953,4 +664,4 @@ Section RelUniv_Yo_Rezk.
     apply weak_relu_square_commutes_strictly.
   Defined.
 
-End RelUniv_Yo_Rezk.
+End RelUniv_Yo_Rezk.