Library HoTT.Modalities.Lex
(* -*- mode: coq; mode: visual-line -*- *)
Require Import HoTT.Basics HoTT.Types.
Require Import HFiber Limits.Pullback Factorization Truncations.Core.
Require Import Modality Accessible Localization Descent Separated.
Local Open Scope path_scope.
Local Open Scope subuniverse_scope.
Require Import HoTT.Basics HoTT.Types.
Require Import HFiber Limits.Pullback Factorization Truncations.Core.
Require Import Modality Accessible Localization Descent Separated.
Local Open Scope path_scope.
Local Open Scope subuniverse_scope.
Lex modalities
Properties of lex modalities
RSS Theorem 3.1 (i)
Definition isconnected_paths
{A : Type} `{IsConnected O A} (x y : A)
: IsConnected O (x = y)
:= OO_isconnected_paths O O x y.
{A : Type} `{IsConnected O A} (x y : A)
: IsConnected O (x = y)
:= OO_isconnected_paths O O x y.
RSS Theorem 3.1 (iii)
Definition conn_map_lex
{Y X : Type} `{IsConnected O Y, IsConnected O X} (f : Y → X)
: IsConnMap O f
:= OO_conn_map_isconnected O O f.
{Y X : Type} `{IsConnected O Y, IsConnected O X} (f : Y → X)
: IsConnMap O f
:= OO_conn_map_isconnected O O f.
RSS Theorem 3.1 (iv)
Definition isequiv_mapino_isconnected
{Y X : Type} `{IsConnected O Y, IsConnected O X}
(f : Y → X) `{MapIn O _ _ f}
: IsEquiv f
:= OO_isequiv_mapino_isconnected O O f.
{Y X : Type} `{IsConnected O Y, IsConnected O X}
(f : Y → X) `{MapIn O _ _ f}
: IsEquiv f
:= OO_isequiv_mapino_isconnected O O f.
RSS Theorem 3.1 (vi)
Definition conn_map_functor_hfiber {A B C D : Type}
{f : A → B} {g : C → D} {h : A → C} {k : B → D}
`{IsConnMap O _ _ h, IsConnMap O _ _ k}
(p : k o f == g o h) (b : B)
: IsConnMap O (functor_hfiber p b)
:= OO_conn_map_functor_hfiber O O p b.
{f : A → B} {g : C → D} {h : A → C} {k : B → D}
`{IsConnMap O _ _ h, IsConnMap O _ _ k}
(p : k o f == g o h) (b : B)
: IsConnMap O (functor_hfiber p b)
:= OO_conn_map_functor_hfiber O O p b.
RSS Theorem 3.1 (vii)
Definition ispullback_connmap_mapino_commsq
{A B C D : Type} {f : A → B} {g : C → D} {h : A → C} {k : B → D}
(p : k o f == g o h)
`{O_inverts O h, O_inverts O k, MapIn O _ _ f, MapIn O _ _ g}
: IsPullback p
:= OO_ispullback_connmap_mapino O O p.
{A B C D : Type} {f : A → B} {g : C → D} {h : A → C} {k : B → D}
(p : k o f == g o h)
`{O_inverts O h, O_inverts O k, MapIn O _ _ f, MapIn O _ _ g}
: IsPullback p
:= OO_ispullback_connmap_mapino O O p.
RSS Theorem 3.1 (viii)
Global Instance conn_map_functor_hfiber_to_O
{Y X : Type} (f : Y → X) (x : X)
: IsConnMap O (functor_hfiber (fun y ⇒ (to_O_natural O f y)^) x)
:= OO_conn_map_functor_hfiber_to_O O O f x.
Global Instance isequiv_O_functor_hfiber
{A B} (f : A → B) (b : B)
: IsEquiv (O_functor_hfiber O f b).
Proof.
apply (isequiv_O_rec_O_inverts O).
apply O_inverts_conn_map.
refine (conn_map_homotopic
O (functor_hfiber (fun x ⇒ (to_O_natural O f x)^) b)
_ _ _).
intros [a p].
unfold functor_hfiber, functor_sigma. apply ap.
apply whiskerR, inv_V.
Defined.
Definition equiv_O_functor_hfiber
{A B} (f : A → B) (b : B)
: O (hfiber f b) <~> hfiber (O_functor O f) (to O B b)
:= Build_Equiv _ _ (O_functor_hfiber O f b) _.
{Y X : Type} (f : Y → X) (x : X)
: IsConnMap O (functor_hfiber (fun y ⇒ (to_O_natural O f y)^) x)
:= OO_conn_map_functor_hfiber_to_O O O f x.
Global Instance isequiv_O_functor_hfiber
{A B} (f : A → B) (b : B)
: IsEquiv (O_functor_hfiber O f b).
Proof.
apply (isequiv_O_rec_O_inverts O).
apply O_inverts_conn_map.
refine (conn_map_homotopic
O (functor_hfiber (fun x ⇒ (to_O_natural O f x)^) b)
_ _ _).
intros [a p].
unfold functor_hfiber, functor_sigma. apply ap.
apply whiskerR, inv_V.
Defined.
Definition equiv_O_functor_hfiber
{A B} (f : A → B) (b : B)
: O (hfiber f b) <~> hfiber (O_functor O f) (to O B b)
:= Build_Equiv _ _ (O_functor_hfiber O f b) _.
RSS Theorem 3.1 (ix)
Global Instance isequiv_path_O
{X : Type@{i}} (x y : X)
: IsEquiv (path_OO O O x y)
:= isequiv_path_OO O O x y.
Definition equiv_path_O {X : Type@{i}} (x y : X)
: O (x = y) <~> (to O X x = to O X y)
:= equiv_path_OO O O x y.
Definition equiv_path_O_to_O {X : Type} (x y : X)
: (equiv_path_O x y) o (to O (x = y)) == @ap _ _ (to O X) x y.
Proof.
intros p; unfold equiv_path_O, equiv_path_OO, path_OO; cbn.
apply O_rec_beta.
Defined.
{X : Type@{i}} (x y : X)
: IsEquiv (path_OO O O x y)
:= isequiv_path_OO O O x y.
Definition equiv_path_O {X : Type@{i}} (x y : X)
: O (x = y) <~> (to O X x = to O X y)
:= equiv_path_OO O O x y.
Definition equiv_path_O_to_O {X : Type} (x y : X)
: (equiv_path_O x y) o (to O (x = y)) == @ap _ _ (to O X) x y.
Proof.
intros p; unfold equiv_path_O, equiv_path_OO, path_OO; cbn.
apply O_rec_beta.
Defined.
RSS Theorem 3.1 (x). This justifies the term "left exact".
Global Instance O_inverts_functor_pullback_to_O
{A B C : Type} (f : B → A) (g : C → A)
: O_inverts O (functor_pullback f g (O_functor O f) (O_functor O g)
(to O A) (to O B) (to O C)
(to_O_natural O f) (to_O_natural O g))
:= OO_inverts_functor_pullback_to_O O O f g.
Definition equiv_O_pullback {A B C : Type} (f : B → A) (g : C → A)
: O (Pullback f g) <~> Pullback (O_functor O f) (O_functor O g)
:= equiv_O_rec_O_inverts
O (functor_pullback f g (O_functor O f) (O_functor O g)
(to O A) (to O B) (to O C)
(to_O_natural O f) (to_O_natural O g)).
Definition O_functor_pullback
{A B C : Type} (f : B → A) (g : C → A)
: IsPullback (O_functor_square O _ _ _ _ (pullback_commsq f g)).
Proof.
unfold IsPullback.
nrapply (isequiv_homotopic
(O_rec (functor_pullback _ _ _ _ _ _ _
(to_O_natural O f) (to_O_natural O g)))).
1: apply isequiv_O_rec_O_inverts; exact _.
apply O_indpaths.
etransitivity.
1: intro x; apply O_rec_beta.
symmetry.
snrapply pullback_homotopic; intros [b [c e]]; cbn.
all: change (to (modality_subuniv O)) with (to O).
- nrapply (to_O_natural O).
- nrapply (to_O_natural O).
- Open Scope long_path_scope.
lhs nrapply concat_p_pp.
lhs nrapply (concat_p_pp _ _ _ @@ 1).
rewrite to_O_natural_compose.
unfold O_functor_square.
rewrite O_functor_homotopy_beta.
rewrite 6 concat_pp_p.
do 3 apply whiskerL.
rhs_V nrapply concat_pp_p.
apply moveL_pM.
lhs_V nrapply inv_pp.
rhs_V nrapply inv_Vp.
apply (ap inverse).
nrapply to_O_natural_compose.
Close Scope long_path_scope.
Defined.
Definition diagonal_O_functor {A B : Type} (f : A → B)
: diagonal (O_functor O f) == equiv_O_pullback f f o O_functor O (diagonal f).
Proof.
apply O_indpaths; intros x.
refine (_ @ (ap _ (to_O_natural _ _ _))^).
cbn.
refine (_ @ (O_rec_beta _ _)^).
unfold diagonal, functor_pullback, functor_sigma; cbn.
apply ap, ap.
apply moveL_pV; exact (concat_1p_p1 _).
Defined.
{A B C : Type} (f : B → A) (g : C → A)
: O_inverts O (functor_pullback f g (O_functor O f) (O_functor O g)
(to O A) (to O B) (to O C)
(to_O_natural O f) (to_O_natural O g))
:= OO_inverts_functor_pullback_to_O O O f g.
Definition equiv_O_pullback {A B C : Type} (f : B → A) (g : C → A)
: O (Pullback f g) <~> Pullback (O_functor O f) (O_functor O g)
:= equiv_O_rec_O_inverts
O (functor_pullback f g (O_functor O f) (O_functor O g)
(to O A) (to O B) (to O C)
(to_O_natural O f) (to_O_natural O g)).
Definition O_functor_pullback
{A B C : Type} (f : B → A) (g : C → A)
: IsPullback (O_functor_square O _ _ _ _ (pullback_commsq f g)).
Proof.
unfold IsPullback.
nrapply (isequiv_homotopic
(O_rec (functor_pullback _ _ _ _ _ _ _
(to_O_natural O f) (to_O_natural O g)))).
1: apply isequiv_O_rec_O_inverts; exact _.
apply O_indpaths.
etransitivity.
1: intro x; apply O_rec_beta.
symmetry.
snrapply pullback_homotopic; intros [b [c e]]; cbn.
all: change (to (modality_subuniv O)) with (to O).
- nrapply (to_O_natural O).
- nrapply (to_O_natural O).
- Open Scope long_path_scope.
lhs nrapply concat_p_pp.
lhs nrapply (concat_p_pp _ _ _ @@ 1).
rewrite to_O_natural_compose.
unfold O_functor_square.
rewrite O_functor_homotopy_beta.
rewrite 6 concat_pp_p.
do 3 apply whiskerL.
rhs_V nrapply concat_pp_p.
apply moveL_pM.
lhs_V nrapply inv_pp.
rhs_V nrapply inv_Vp.
apply (ap inverse).
nrapply to_O_natural_compose.
Close Scope long_path_scope.
Defined.
Definition diagonal_O_functor {A B : Type} (f : A → B)
: diagonal (O_functor O f) == equiv_O_pullback f f o O_functor O (diagonal f).
Proof.
apply O_indpaths; intros x.
refine (_ @ (ap _ (to_O_natural _ _ _))^).
cbn.
refine (_ @ (O_rec_beta _ _)^).
unfold diagonal, functor_pullback, functor_sigma; cbn.
apply ap, ap.
apply moveL_pV; exact (concat_1p_p1 _).
Defined.
RSS Theorem 3.1 (xi)
Definition cancelL_conn_map
{Y X Z : Type} (f : Y → X) (g : X → Z)
`{IsConnMap O _ _ (g o f)} `{IsConnMap O _ _ g}
: IsConnMap O f
:= OO_cancelL_conn_map O O f g.
{Y X Z : Type} (f : Y → X) (g : X → Z)
`{IsConnMap O _ _ (g o f)} `{IsConnMap O _ _ g}
: IsConnMap O f
:= OO_cancelL_conn_map O O f g.
RSS Theorem 3.1 (xii)
Global Instance conn_map_O_inverts
{A B : Type} (f : A → B) `{O_inverts O f}
: IsConnMap O f
:= conn_map_OO_inverts O O f.
{A B : Type} (f : A → B) `{O_inverts O f}
: IsConnMap O f
:= conn_map_OO_inverts O O f.
RSS Theorem 3.1 (xiii)
Definition modal_over_connected_isconst_lex
(A : Type) `{IsConnected O A}
(P : A → Type) `{∀ x, In O (P x)}
: {Q : Type & In O Q × ∀ x, Q <~> P x}.
Proof.
pose proof (O_inverts_isconnected O (fun _:A ⇒ tt)).
∃ (OO_descend_O_inverts O O (fun _:A ⇒ tt) P tt); split.
- apply OO_descend_O_inverts_inO.
- intros; nrapply OO_descend_O_inverts_beta.
Defined.
(A : Type) `{IsConnected O A}
(P : A → Type) `{∀ x, In O (P x)}
: {Q : Type & In O Q × ∀ x, Q <~> P x}.
Proof.
pose proof (O_inverts_isconnected O (fun _:A ⇒ tt)).
∃ (OO_descend_O_inverts O O (fun _:A ⇒ tt) P tt); split.
- apply OO_descend_O_inverts_inO.
- intros; nrapply OO_descend_O_inverts_beta.
Defined.
RSS Theorem 3.11 (iii): in the accessible case, the universe is modal.
Part of RSS Corollary 3.9: lex modalities preserve n-types for all n. This is definitely not equivalent to lex-ness, since it is true for the truncation modalities that are not lex. But it is also not true of all modalities; e.g. the shape modality in a cohesive topos can take 0-types to oo-types. With a little more work, this can probably be proven without Funext.
Global Instance istrunc_O_lex `{Funext}
{n : trunc_index} {A : Type} `{IsTrunc n A}
: IsTrunc n (O A).
Proof.
generalize dependent A; simple_induction n n IHn; intros A ?.
- exact _.
{n : trunc_index} {A : Type} `{IsTrunc n A}
: IsTrunc n (O A).
Proof.
generalize dependent A; simple_induction n n IHn; intros A ?.
- exact _.
Already proven for all modalities.
- apply istrunc_S.
refine (O_ind (fun x ⇒ ∀ y, IsTrunc n (x = y)) _); intros x.
refine (O_ind (fun y ⇒ IsTrunc n (to O A x = y)) _); intros y.
refine (istrunc_equiv_istrunc _ (equiv_path_O x y)).
Defined.
End LexModality.
refine (O_ind (fun x ⇒ ∀ y, IsTrunc n (x = y)) _); intros x.
refine (O_ind (fun y ⇒ IsTrunc n (to O A x = y)) _); intros y.
refine (istrunc_equiv_istrunc _ (equiv_path_O x y)).
Defined.
End LexModality.
Equivalent characterizations of lex-ness
RSS 3.1 (xiii) implies lexness
Definition lex_from_modal_over_connected_isconst
(H : ∀ (A : Type) (A_isC : IsConnected O A)
(P : A → Type) (P_inO : ∀ x, In O (P x)),
{Q : Type & In O Q × ∀ x, Q <~> P x})
: Lex O.
Proof.
intros A; unshelve econstructor; intros P P_inO.
all:pose (Q := fun z:O A ⇒ H (hfiber (to O A) z) _ (P o pr1) _).
- exact (fun z ⇒ (Q z).1).
- exact (fun z ⇒ fst (Q z).2).
- intros x; cbn.
exact (snd (Q (to O A x)).2 (x;1)).
Defined.
(H : ∀ (A : Type) (A_isC : IsConnected O A)
(P : A → Type) (P_inO : ∀ x, In O (P x)),
{Q : Type & In O Q × ∀ x, Q <~> P x})
: Lex O.
Proof.
intros A; unshelve econstructor; intros P P_inO.
all:pose (Q := fun z:O A ⇒ H (hfiber (to O A) z) _ (P o pr1) _).
- exact (fun z ⇒ (Q z).1).
- exact (fun z ⇒ fst (Q z).2).
- intros x; cbn.
exact (snd (Q (to O A x)).2 (x;1)).
Defined.
RSS 3.11 (iii), the universe is modal, implies lex-ness
Definition lex_from_inO_typeO `{IsAccRSU O} `{In (lift_accrsu O) (Type_ O)}
: Lex O.
Proof.
apply (O_lex_leq_inO_TypeO O O).
Defined.
: Lex O.
Proof.
apply (O_lex_leq_inO_TypeO O O).
Defined.
RSS Theorem 3.1 (xi) implies lex-ness
Definition lex_from_cancelL_conn_map
(cancel : ∀ {Y X Z : Type} (f : Y → X) (g : X → Z),
(IsConnMap O (g o f)) → (IsConnMap O g)
→ IsConnMap O f)
: Lex O.
Proof.
apply lex_from_modal_over_connected_isconst; intros.
∃ (O {x:A & P x}); split; [ exact _ | intros x; symmetry ].
refine (Build_Equiv _ _ (fun p ⇒ to O _ (x ; p)) _).
nrefine (isequiv_conn_map_ino O _). 1-2:exact _.
revert x; apply conn_map_fiber.
nrefine (cancel _ _ _ _ (fun z:{x:A & O {x : A & P x}} ⇒ z.2) _ _).
1: clear cancel; exact _.
intros z.
refine (isconnected_equiv' O A _ _).
unfold hfiber.
refine (equiv_adjointify (fun x ⇒ ((x ; z) ; 1))
(fun y ⇒ y.1.1) _ _).
- intros [[x y] []]; reflexivity.
- intros x; reflexivity.
Defined.
(cancel : ∀ {Y X Z : Type} (f : Y → X) (g : X → Z),
(IsConnMap O (g o f)) → (IsConnMap O g)
→ IsConnMap O f)
: Lex O.
Proof.
apply lex_from_modal_over_connected_isconst; intros.
∃ (O {x:A & P x}); split; [ exact _ | intros x; symmetry ].
refine (Build_Equiv _ _ (fun p ⇒ to O _ (x ; p)) _).
nrefine (isequiv_conn_map_ino O _). 1-2:exact _.
revert x; apply conn_map_fiber.
nrefine (cancel _ _ _ _ (fun z:{x:A & O {x : A & P x}} ⇒ z.2) _ _).
1: clear cancel; exact _.
intros z.
refine (isconnected_equiv' O A _ _).
unfold hfiber.
refine (equiv_adjointify (fun x ⇒ ((x ; z) ; 1))
(fun y ⇒ y.1.1) _ _).
- intros [[x y] []]; reflexivity.
- intros x; reflexivity.
Defined.
RSS Theorem 3.1 (iii) implies lex-ness
Definition lex_from_conn_map_lex
(H : ∀ A B (f : A → B),
(IsConnected O A) → (IsConnected O B) →
IsConnMap O f)
: Lex O.
Proof.
apply lex_from_cancelL_conn_map.
intros Y X Z f g gfc gc x.
pose (h := @functor_hfiber Y Z X Z (g o f) g f idmap (fun a ⇒ 1%path)).
assert (cc := H _ _ (h (g x)) (gfc (g x)) (gc (g x))).
refine (isconnected_equiv' O _ _ (cc (x;1))).
unfold hfiber.
subst h; unfold functor_hfiber, functor_sigma; cbn.
refine (_ oE (equiv_sigma_assoc _ _)^-1).
apply equiv_functor_sigma_id; intros y; cbn.
refine (_ oE (equiv_functor_sigma_id _)).
2:intros; symmetry; apply equiv_path_sigma.
cbn.
refine (_ oE equiv_sigma_symm _).
apply equiv_sigma_contr; intros p.
destruct p; cbn.
refine (contr_equiv' { p : g (f y) = g (f y) & p = 1%path } _).
apply equiv_functor_sigma_id; intros p; cbn.
apply equiv_concat_l.
exact (concat_1p _ @ ap_idmap _).
Defined.
(H : ∀ A B (f : A → B),
(IsConnected O A) → (IsConnected O B) →
IsConnMap O f)
: Lex O.
Proof.
apply lex_from_cancelL_conn_map.
intros Y X Z f g gfc gc x.
pose (h := @functor_hfiber Y Z X Z (g o f) g f idmap (fun a ⇒ 1%path)).
assert (cc := H _ _ (h (g x)) (gfc (g x)) (gc (g x))).
refine (isconnected_equiv' O _ _ (cc (x;1))).
unfold hfiber.
subst h; unfold functor_hfiber, functor_sigma; cbn.
refine (_ oE (equiv_sigma_assoc _ _)^-1).
apply equiv_functor_sigma_id; intros y; cbn.
refine (_ oE (equiv_functor_sigma_id _)).
2:intros; symmetry; apply equiv_path_sigma.
cbn.
refine (_ oE equiv_sigma_symm _).
apply equiv_sigma_contr; intros p.
destruct p; cbn.
refine (contr_equiv' { p : g (f y) = g (f y) & p = 1%path } _).
apply equiv_functor_sigma_id; intros p; cbn.
apply equiv_concat_l.
exact (concat_1p _ @ ap_idmap _).
Defined.
RSS Theorem 3.1 (i) implies lex-ness
Definition lex_from_isconnected_paths
(H : ∀ (A : Type) (Ac : IsConnected O A) (x y : A),
IsConnected O (x = y))
: Lex O.
Proof.
apply lex_from_conn_map_lex.
intros A B f Ac Bc c.
rapply isconnected_sigma.
Defined.
(H : ∀ (A : Type) (Ac : IsConnected O A) (x y : A),
IsConnected O (x = y))
: Lex O.
Proof.
apply lex_from_conn_map_lex.
intros A B f Ac Bc c.
rapply isconnected_sigma.
Defined.
RSS Theorem 3.1 (iv) implies lex-ness
Definition lex_from_isequiv_ismodal_isconnected_types
(H : ∀ A B (f : A → B),
(IsConnected O A) → (IsConnected O B) →
(MapIn O f) → IsEquiv f)
: Lex O.
Proof.
apply lex_from_conn_map_lex.
intros A B f AC BC.
apply (conn_map_homotopic O _ _ (fact_factors (image O f))).
apply conn_map_compose; [ exact _ | ].
apply conn_map_isequiv.
apply H; [ | exact _ | exact _ ].
apply isconnected_conn_map_to_unit.
apply (cancelR_conn_map O (factor1 (image O f)) (const_tt _)).
Defined.
(H : ∀ A B (f : A → B),
(IsConnected O A) → (IsConnected O B) →
(MapIn O f) → IsEquiv f)
: Lex O.
Proof.
apply lex_from_conn_map_lex.
intros A B f AC BC.
apply (conn_map_homotopic O _ _ (fact_factors (image O f))).
apply conn_map_compose; [ exact _ | ].
apply conn_map_isequiv.
apply H; [ | exact _ | exact _ ].
apply isconnected_conn_map_to_unit.
apply (cancelR_conn_map O (factor1 (image O f)) (const_tt _)).
Defined.
RSS Theorem 3.1 (vii) implies lex-ness
Definition lex_from_ispullback_connmap_mapino_commsq
(H : ∀ {A B C D}
(f : A → B) (g : C → D) (h : A → C) (k : B → D),
(IsConnMap O f) → (IsConnMap O g) →
(MapIn O h) → (MapIn O k) →
∀ (p : k o f == g o h), IsPullback p)
: Lex O.
Proof.
apply lex_from_isequiv_ismodal_isconnected_types.
intros A B f AC BC fM.
specialize (H A Unit B Unit (const_tt _) (const_tt _) f idmap _ _ _ _
(fun _ ⇒ 1)).
unfold IsPullback, pullback_corec in H.
refine (@isequiv_compose _ _ _ H _ (fun x ⇒ x.2.1) _).
unfold Pullback.
refine (@isequiv_compose _ {b:Unit & B}
(functor_sigma idmap (fun a ⇒ pr1))
_ _ pr2 _).
refine (@isequiv_compose _ _ (equiv_sigma_prod0 Unit B)
_ _ snd _).
apply (equiv_isequiv (prod_unit_l B)).
Defined.
End ImpliesLex.
(H : ∀ {A B C D}
(f : A → B) (g : C → D) (h : A → C) (k : B → D),
(IsConnMap O f) → (IsConnMap O g) →
(MapIn O h) → (MapIn O k) →
∀ (p : k o f == g o h), IsPullback p)
: Lex O.
Proof.
apply lex_from_isequiv_ismodal_isconnected_types.
intros A B f AC BC fM.
specialize (H A Unit B Unit (const_tt _) (const_tt _) f idmap _ _ _ _
(fun _ ⇒ 1)).
unfold IsPullback, pullback_corec in H.
refine (@isequiv_compose _ _ _ H _ (fun x ⇒ x.2.1) _).
unfold Pullback.
refine (@isequiv_compose _ {b:Unit & B}
(functor_sigma idmap (fun a ⇒ pr1))
_ _ pr2 _).
refine (@isequiv_compose _ _ (equiv_sigma_prod0 Unit B)
_ _ snd _).
apply (equiv_isequiv (prod_unit_l B)).
Defined.
End ImpliesLex.
Lex reflective subuniverses
Definition ismodality_isequiv_O_functor_hfiber (O : ReflectiveSubuniverse)
(H : ∀ {A B : Type} (f : A → B) (b : B),
IsEquiv (O_functor_hfiber O f b))
: IsModality O.
Proof.
intros A'; rapply reflectsD_from_inO_sigma.
intros B B_inO.
pose (A := O A').
pose (g := O_rec pr1 : O {x : A & B x} → A).
transparent assert (p : (∀ x, g (to O _ x) = x.1)).
{ intros x; subst g; apply O_rec_beta. }
apply inO_isequiv_to_O.
apply isequiv_contr_map; intros x.
snrefine (contr_equiv' _ (hfiber_hfiber_compose_map _ g x)).
apply contr_map_isequiv.
unfold hfiber_compose_map.
transparent assert (h : (hfiber (@pr1 A B) (g x) <~> hfiber g (g x))).
{ refine (_ oE equiv_to_O O _).
refine (_ oE Build_Equiv _ _
(O_functor_hfiber O (@pr1 A B) (g x)) _).
unfold hfiber.
apply equiv_functor_sigma_id. intros y; cbn.
refine (_ oE (equiv_moveR_equiv_V _ _)).
apply equiv_concat_l.
apply moveL_equiv_V.
unfold g, O_functor.
revert y; apply O_indpaths; intros [a q]; cbn.
refine (_ @ (O_rec_beta _ _)^).
apply ap, O_rec_beta. }
refine (isequiv_homotopic (h oE equiv_hfiber_homotopic _ _ p (g x)) _).
intros [[a b] q]; cbn. clear h.
unfold O_functor_hfiber.
rewrite O_rec_beta.
unfold functor_sigma; cbn.
refine (path_sigma' _ 1 _).
rewrite O_indpaths_beta; cbn.
unfold moveL_equiv_V, moveR_equiv_V.
Open Scope long_path_scope.
Local Opaque eissect. (* work around bug 4533 *)
(* Even though https://github.com/coq/coq/issues/4533 is closed, this is still needed. *)
rewrite !ap_pp, !concat_p_pp, !ap_V.
unfold to_O_natural.
rewrite concat_pV_p.
subst p.
rewrite concat_pp_V.
rewrite concat_pp_p; apply moveR_Vp.
rewrite <- !(ap_compose (to O A) (to O A)^-1).
rapply @concat_A1p.
Local Transparent eissect. (* work around bug 4533 *)
Close Scope long_path_scope.
Qed.
(H : ∀ {A B : Type} (f : A → B) (b : B),
IsEquiv (O_functor_hfiber O f b))
: IsModality O.
Proof.
intros A'; rapply reflectsD_from_inO_sigma.
intros B B_inO.
pose (A := O A').
pose (g := O_rec pr1 : O {x : A & B x} → A).
transparent assert (p : (∀ x, g (to O _ x) = x.1)).
{ intros x; subst g; apply O_rec_beta. }
apply inO_isequiv_to_O.
apply isequiv_contr_map; intros x.
snrefine (contr_equiv' _ (hfiber_hfiber_compose_map _ g x)).
apply contr_map_isequiv.
unfold hfiber_compose_map.
transparent assert (h : (hfiber (@pr1 A B) (g x) <~> hfiber g (g x))).
{ refine (_ oE equiv_to_O O _).
refine (_ oE Build_Equiv _ _
(O_functor_hfiber O (@pr1 A B) (g x)) _).
unfold hfiber.
apply equiv_functor_sigma_id. intros y; cbn.
refine (_ oE (equiv_moveR_equiv_V _ _)).
apply equiv_concat_l.
apply moveL_equiv_V.
unfold g, O_functor.
revert y; apply O_indpaths; intros [a q]; cbn.
refine (_ @ (O_rec_beta _ _)^).
apply ap, O_rec_beta. }
refine (isequiv_homotopic (h oE equiv_hfiber_homotopic _ _ p (g x)) _).
intros [[a b] q]; cbn. clear h.
unfold O_functor_hfiber.
rewrite O_rec_beta.
unfold functor_sigma; cbn.
refine (path_sigma' _ 1 _).
rewrite O_indpaths_beta; cbn.
unfold moveL_equiv_V, moveR_equiv_V.
Open Scope long_path_scope.
Local Opaque eissect. (* work around bug 4533 *)
(* Even though https://github.com/coq/coq/issues/4533 is closed, this is still needed. *)
rewrite !ap_pp, !concat_p_pp, !ap_V.
unfold to_O_natural.
rewrite concat_pV_p.
subst p.
rewrite concat_pp_V.
rewrite concat_pp_p; apply moveR_Vp.
rewrite <- !(ap_compose (to O A) (to O A)^-1).
rapply @concat_A1p.
Local Transparent eissect. (* work around bug 4533 *)
Close Scope long_path_scope.
Qed.
Lexness via generators
Definition lex_gen `{Univalence} (O : Modality) `{IsAccModality O}
(lexgen : ∀ (i : ngen_indices (acc_ngen O)) (x y : ngen_type (acc_ngen O) i),
IsConnected O (x = y))
: Lex O.
Proof.
srapply lex_from_inO_typeO; [ exact _ | intros i ].
rapply ooextendable_TypeO_from_extension; intros P; srefine (_;_).
1:intros; ∃ (∀ x, P x); exact _.
assert (wc : ∀ y z, P y <~> P z).
{ intros y z.
(lexgen : ∀ (i : ngen_indices (acc_ngen O)) (x y : ngen_type (acc_ngen O) i),
IsConnected O (x = y))
: Lex O.
Proof.
srapply lex_from_inO_typeO; [ exact _ | intros i ].
rapply ooextendable_TypeO_from_extension; intros P; srefine (_;_).
1:intros; ∃ (∀ x, P x); exact _.
assert (wc : ∀ y z, P y <~> P z).
{ intros y z.
Here we use the hypothesis lexgen (typeclass inference finds it automatically).
refine (pr1 (isconnected_elim O _ (@equiv_transport _ P y z))). }
intros x; apply path_TypeO, path_universe_uncurried.
refine (equiv_adjointify (fun f ⇒ f x) (fun u y ⇒ wc x y ((wc x x)^-1 u)) _ _).
- intros u; apply eisretr.
- intros f; apply path_forall; intros y; apply moveR_equiv_M.
destruct (isconnected_elim O _ (fun y ⇒ (wc x y)^-1 (f y))) as [z p].
exact (p x @ (p y)^).
Defined.
intros x; apply path_TypeO, path_universe_uncurried.
refine (equiv_adjointify (fun f ⇒ f x) (fun u y ⇒ wc x y ((wc x x)^-1 u)) _ _).
- intros u; apply eisretr.
- intros f; apply path_forall; intros y; apply moveR_equiv_M.
destruct (isconnected_elim O _ (fun y ⇒ (wc x y)^-1 (f y))) as [z p].
exact (p x @ (p y)^).
Defined.
n-fold separation
Fixpoint nSep (n : trunc_index) (O : Subuniverse) : Subuniverse
:= match n with
| -2 ⇒ O
| n.+1 ⇒ Sep (nSep n O)
end.
:= match n with
| -2 ⇒ O
| n.+1 ⇒ Sep (nSep n O)
end.
The reason for indexing this notion by a trunc_index rather than a nat is that when O is lex, a type is n-O-separated if and only if its O-unit is an n-truncated map.
Definition nsep_iff_trunc_to_O (n : trunc_index) (O : Modality) `{Lex O} (A : Type)
: In (nSep n O) A ↔ IsTruncMap n (to O A).
Proof.
revert A; induction n as [|n IHn]; intros A; split; intros ?.
- apply contr_map_isequiv; rapply isequiv_to_O_inO.
- apply (inO_equiv_inO (O A) (to O A)^-1).
- apply istruncmap_from_ap; intros x y.
pose (i := fst (IHn (x = y)) _).
apply istruncmap_mapinO_tr, (mapinO_homotopic _ _ (equiv_path_O_to_O O x y)).
- intros x y.
apply (snd (IHn (x = y))).
pose (i := istruncmap_ap n (to O A) x y).
apply mapinO_tr_istruncmap in i.
apply istruncmap_mapinO_tr, (mapinO_homotopic _ ((equiv_path_O O x y)^-1 o (@ap _ _ (to O A) x y))).
{ intros p; apply moveR_equiv_V; symmetry; apply equiv_path_O_to_O. }
pose mapinO_isequiv. (* This speeds up the next line. *)
rapply mapinO_compose.
Defined.
: In (nSep n O) A ↔ IsTruncMap n (to O A).
Proof.
revert A; induction n as [|n IHn]; intros A; split; intros ?.
- apply contr_map_isequiv; rapply isequiv_to_O_inO.
- apply (inO_equiv_inO (O A) (to O A)^-1).
- apply istruncmap_from_ap; intros x y.
pose (i := fst (IHn (x = y)) _).
apply istruncmap_mapinO_tr, (mapinO_homotopic _ _ (equiv_path_O_to_O O x y)).
- intros x y.
apply (snd (IHn (x = y))).
pose (i := istruncmap_ap n (to O A) x y).
apply mapinO_tr_istruncmap in i.
apply istruncmap_mapinO_tr, (mapinO_homotopic _ ((equiv_path_O O x y)^-1 o (@ap _ _ (to O A) x y))).
{ intros p; apply moveR_equiv_V; symmetry; apply equiv_path_O_to_O. }
pose mapinO_isequiv. (* This speeds up the next line. *)
rapply mapinO_compose.
Defined.