Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Apr 21, 2020
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
341 changes: 26 additions & 315 deletions TypeTheory/ALV2/RelUnivTransfer.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.

Expand Down Expand Up @@ -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.
Expand All @@ -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
Expand Down Expand Up @@ -953,4 +664,4 @@ Section RelUniv_Yo_Rezk.
apply weak_relu_square_commutes_strictly.
Defined.

End RelUniv_Yo_Rezk.
End RelUniv_Yo_Rezk.
Loading