Skip to content

Descent: strengthen OO_cancelL_conn_map ("if" dir of CORS 2.31) #2372

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

Open
jdchristensen wants to merge 1 commit into
base: master
Choose a base branch
from
+7 −7
Open

Descent: strengthen OO_cancelL_conn_map ("if" dir of CORS 2.31) #2372

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
14 changes: 7 additions & 7 deletions theories/Modalities/Descent.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -346,21 +346,21 @@ Definition equiv_OO_pullback {A B C : Type} (f : B -> A) (g : C -> A)
: O (Pullback f g) <~> O (Pullback (O_functor O' f) (O_functor O' g))
:= Build_Equiv _ _ _ (OO_inverts_functor_pullback_to_O f g).

(** The "if" direction of CORS Proposition 2.31, and the nontrivial part of Theorem 3.1(xi) of RSS. Note that we could also deduce Theorem 3.1(iii) of RSS from this. *)
(** This is a strengthening of the "if" direction of CORS Proposition 2.31. In 2.31, [g o f] is assumed to be [O']-connected, but here we only require it to be [O]-connected. When [O = O'], this gives the nontrivial part of Theorem 3.1(xi) of RSS. Note that we could also deduce Theorem 3.1(iii) of RSS from this. *)
Definition OO_cancelL_conn_map
{Y X Z : Type} (f : Y -> X) (g : X -> Z)
`{IsConnMap O' _ _ (g o f)} `{IsConnMap O' _ _ g}
`{IsConnMap O _ _ (g o f)} `{IsConnMap O' _ _ g}
: IsConnMap O f.
Proof.
apply conn_map_OO_inverts.
napply (cancelL_isequiv (O_functor O' g)).
1:exact _.
exact (isequiv_homotopic _ (O_functor_compose O' f g)).
intro x.
(* The fiber of [f] is equivalent to the fiber of a map between the fibers of [g o f] and [g], so this follows immediately from [OO_isconnected_hfiber]. *)
apply (isconnected_equiv' O _ (hfiber_hfiber_compose_map f g x)).
apply OO_isconnected_hfiber.
Defined.

End LeftExactness.

(** Here's the "only if" direction of CORS Proposition 2.31. Note that the hypotheses are different from those of the "if" direction, and the proof is shorter than the one given in CORS. *)
(** Here's the "only if" direction of CORS Proposition 2.31. Note that the hypotheses on [O] and [O'] are different from those of the "if" direction, and the proof is shorter than the one given in CORS. Also note that it is not possible to weaken the assumption on [g o f] to being [O]-connected (e.g. take [f] to be the identity). *)
Definition OO_cancelR_conn_map
(O' O : ReflectiveSubuniverse@{u}) `{O_leq@{u u u} O O', O' <= Sep O}
{Y X Z : Type} (f : Y -> X) (g : X -> Z)
Expand Down
Loading