(* -*- mode: coq; mode: visual-line -*- *)
Require Import HoTT.Basics HoTT.Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Modalities.Modality Modalities.Open.

Local Open Scope path_scope.

(** * Coreflective subuniverses. *)

(** In this file we study "coreflective subuniverses" that are defined dually to reflective subuniverses.  However, it turns out that there are many fewer examples of these.  The "internal" nature of such definitions, which in the reflective case makes the subuniverse automatically an exponential ideal, in the coreflective case has much stronger consequences: it forces the entire coreflection to be determined by the image of [Unit], which can be an arbitrary hprop.  Thus, this file is essentially just a no-go theorem: there are no coreflective subuniverses other than a certain class of fairly simple ones (which we call "co-open" since they are dual to open modalities).

In particular, since we do not foresee many applications of this file, we don't bother introducing modules to make the definitions more universe polymorphic the way we did for reflective subuniverses. *)

Record CoreflectiveSubuniverse :=
  { inF : Type -> HProp ;
    F_coreflector : Type -> Type ;
    F_inF : forall X, inF (F_coreflector X) ;
    fromF : forall X, F_coreflector X -> X ;
    (** We also don't bother defining [ooLiftableAlong] so as to state the universal property without [Funext]. *)
    isequiv_fromF_postcompose
    : forall {Y X} {Y_inF : inF Y},
        IsEquiv (fun (g : Y -> F_coreflector X) => fromF X o g)
    (** Similarly, we don't bother asserting repleteness; we'll just use univalence. *)
  }.

Coercion F_coreflector : CoreflectiveSubuniverse >-> Funclass.

Section CoreflectiveSubuniverse.
  Context `{Univalence}.
  Context {F : CoreflectiveSubuniverse}.

  (** We begin by extracting the corecursor, its computation rule, and its eta principle. *)

  Definition F_corec {Y X} `(inF F Y) (f : Y -> X) : Y -> F X.
H: Univalence
F: CoreflectiveSubuniverse
Y, X: Type
inF0: inF F Y
f: Y -> X
Y -> F X
  Proof.
H: Univalence
F: CoreflectiveSubuniverse
Y, X: Type
inF0: inF F Y
f: Y -> X
Y -> F X
    refine ((fun (g : Y -> F X) => fromF F X o g)^-1 f).
H: Univalence
F: CoreflectiveSubuniverse
Y, X: Type
inF0: inF F Y
f: Y -> X
IsEquiv
  (fun (g : Y -> F X) (x : Y) => fromF F X (g x))
    by apply isequiv_fromF_postcompose.
  Defined.

  Definition F_corec_beta {Y X} (YF : inF F Y) (f : Y -> X)
  : fromF F X o F_corec YF f == f.
H: Univalence
F: CoreflectiveSubuniverse
Y, X: Type
YF: inF F Y
f: Y -> X
fromF F X o F_corec YF f == f
  Proof.
H: Univalence
F: CoreflectiveSubuniverse
Y, X: Type
YF: inF F Y
f: Y -> X
fromF F X o F_corec YF f == f
    apply ap10, (eisretr (fun g => fromF F X o g)).
  Defined.

  Definition F_coindpaths {Y X} `(inF F Y) (g h : Y -> F X)
             (p : fromF F X o g == fromF F X o h)
  : g == h.
H: Univalence
F: CoreflectiveSubuniverse
Y, X: Type
inF0: inF F Y
g, h: Y -> F X
p: fromF F X o g == fromF F X o h
g == h
  Proof.
H: Univalence
F: CoreflectiveSubuniverse
Y, X: Type
inF0: inF F Y
g, h: Y -> F X
p: fromF F X o g == fromF F X o h
g == h
    apply ap10.
H: Univalence
F: CoreflectiveSubuniverse
Y, X: Type
inF0: inF F Y
g, h: Y -> F X
p: fromF F X o g == fromF F X o h
g = h
    refine (equiv_inj (fun k => fromF F X o k) _).
H: Univalence
F: CoreflectiveSubuniverse
Y, X: Type
inF0: inF F Y
g, h: Y -> F X
p: fromF F X o g == fromF F X o h
IsEquiv
  (fun (k : Y -> F X) (x : Y) => fromF F X (k x))
H: Univalence
F: CoreflectiveSubuniverse
Y, X: Type
inF0: inF F Y
g, h: Y -> F X
p: fromF F X o g == fromF F X o h
(fun x : Y => fromF F X (g x)) =
(fun x : Y => fromF F X (h x))
    -
H: Univalence
F: CoreflectiveSubuniverse
Y, X: Type
inF0: inF F Y
g, h: Y -> F X
p: fromF F X o g == fromF F X o h
IsEquiv
  (fun (k : Y -> F X) (x : Y) => fromF F X (k x)) by apply isequiv_fromF_postcompose.
    -
H: Univalence
F: CoreflectiveSubuniverse
Y, X: Type
inF0: inF F Y
g, h: Y -> F X
p: fromF F X o g == fromF F X o h
(fun x : Y => fromF F X (g x)) =
(fun x : Y => fromF F X (h x)) by apply path_arrow.
  Defined.

  (** The functorial action of the coreflector. *)
  Definition F_functor {X Y} (f : X -> Y) : F X -> F Y
    := F_corec (F_inF F X) (f o fromF F X).

  (** The coreflector preserves hprops (since it is a right adjoint and thus preserves limits). *)
  Local Instance ishprop_coreflection A `{IsHProp A} : IsHProp (F A).
H: Univalence
F: CoreflectiveSubuniverse
A: Type
IsHProp0: IsHProp A
IsHProp (F A)
  Proof.
H: Univalence
F: CoreflectiveSubuniverse
A: Type
IsHProp0: IsHProp A
IsHProp (F A)
    apply hprop_allpath; intros x y.
H: Univalence
F: CoreflectiveSubuniverse
A: Type
IsHProp0: IsHProp A
x, y: F A
x = y
    exact (F_coindpaths (F_inF F A) (const x) (const y)
                        (fun _ => path_ishprop _ _) x).
  Defined.

  (** A type lies in [F] as soon as [fromF] admits a section. *)
  Definition inF_fromF_sect X (s : X -> F X) (p : fromF F X o s == idmap)
  : inF F X.
H: Univalence
F: CoreflectiveSubuniverse
X: Type
s: X -> F X
p: fromF F X o s == idmap
inF F X
  Proof.
H: Univalence
F: CoreflectiveSubuniverse
X: Type
s: X -> F X
p: fromF F X o s == idmap
inF F X
    refine (transport (inF F) (path_universe (fromF F X)) (F_inF F X)).
H: Univalence
F: CoreflectiveSubuniverse
X: Type
s: X -> F X
p: fromF F X o s == idmap
IsEquiv (fromF F X)
    refine (isequiv_adjointify _ s p _).
H: Univalence
F: CoreflectiveSubuniverse
X: Type
s: X -> F X
p: fromF F X o s == idmap
(fun x : F X => s (fromF F X x)) == idmap
    change (s o fromF F X == idmap).
H: Univalence
F: CoreflectiveSubuniverse
X: Type
s: X -> F X
p: fromF F X o s == idmap
s o fromF F X == idmap
    apply F_coindpaths; try apply F_inF.
H: Univalence
F: CoreflectiveSubuniverse
X: Type
s: X -> F X
p: fromF F X o s == idmap
(fun x : F X => fromF F X (s (fromF F X x))) ==
(fun x : F X => fromF F X x)
    intros x; apply p.
  Defined.

  (** So far, nothing unexpected has happened.  Now, however, we claim that [F] is completely determined by the image of [Unit], which by [ishprop_coreflection] is an hprop.  Specifically, we claim that [X] lies in [F] exactly when [X -> F Unit]. *)
  Definition inF_equiv_implies_funit X
  : inF F X <~> (X -> F Unit).
H: Univalence
F: CoreflectiveSubuniverse
X: Type
inF F X <~> (X -> F Unit)
  Proof.
H: Univalence
F: CoreflectiveSubuniverse
X: Type
inF F X <~> (X -> F Unit)
    apply equiv_iff_hprop.
H: Univalence
F: CoreflectiveSubuniverse
X: Type
inF F X -> X -> F Unit
H: Univalence
F: CoreflectiveSubuniverse
X: Type
(X -> F Unit) -> inF F X
    -
H: Univalence
F: CoreflectiveSubuniverse
X: Type
inF F X -> X -> F Unit intros ?.
H: Univalence
F: CoreflectiveSubuniverse
X: Type
X0: inF F X
X -> F Unit apply F_corec; try assumption.
H: Univalence
F: CoreflectiveSubuniverse
X: Type
X0: inF F X
X -> Unit
      exact (fun _ => tt).
    -
H: Univalence
F: CoreflectiveSubuniverse
X: Type
(X -> F Unit) -> inF F X intros f.
H: Univalence
F: CoreflectiveSubuniverse
X: Type
f: X -> F Unit
inF F X
      simple refine (inF_fromF_sect X _ _).
H: Univalence
F: CoreflectiveSubuniverse
X: Type
f: X -> F Unit
X -> F X
H: Univalence
F: CoreflectiveSubuniverse
X: Type
f: X -> F Unit
fromF F X o ?s == idmap
      +
H: Univalence
F: CoreflectiveSubuniverse
X: Type
f: X -> F Unit
X -> F X intros x.
H: Univalence
F: CoreflectiveSubuniverse
X: Type
f: X -> F Unit
x: X
F X
        exact (F_functor (unit_name x) (f x)).
      +
H: Univalence
F: CoreflectiveSubuniverse
X: Type
f: X -> F Unit
fromF F X
o (fun x : X => F_functor (unit_name x) (f x)) ==
idmap intros x; unfold F_functor.
H: Univalence
F: CoreflectiveSubuniverse
X: Type
f: X -> F Unit
x: X
fromF F X
  (F_corec (F_inF F Unit) (fun _ : F Unit => x) (f x)) =
x
        exact (F_corec_beta (F_inF F Unit) (const x) (f x)).
  Defined.

End CoreflectiveSubuniverse.

(** Conversely, we will now show that for any hprop [U], the types [X] such that [X -> U] are a coreflective subuniverse, which we call "co-open" since it is dual to the open modality. *)

Section CoOpen.
  Context `{Funext} (U : HProp).

  Definition coOp : CoreflectiveSubuniverse.
H: Funext
U: HProp
CoreflectiveSubuniverse
  Proof.
H: Funext
U: HProp
CoreflectiveSubuniverse
    simple refine (Build_CoreflectiveSubuniverse
              (fun X => Build_HProp (X -> U))
              (fun X => X * U)
              (fun X => @snd X U)
              (fun X => @fst X U) _); try exact _.
H: Funext
U: HProp
forall Y X : Type,
(fun X0 : Type => Build_HProp (X0 -> U)) Y ->
IsEquiv
  (fun g : Y -> (fun X0 : Type => X0 * U) X =>
   (fun X0 : Type => fst) X o g)
    intros Y X YU; simpl in *.
H: Funext
U: HProp
Y, X: Type
YU: Y -> U
IsEquiv (fun (g : Y -> X * U) (x : Y) => fst (g x))
    refine (isequiv_adjointify _ (fun h y => (h y , YU y)) _ _).
H: Funext
U: HProp
Y, X: Type
YU: Y -> U
(fun (x : Y -> X) (x0 : Y) => x x0) == idmap
H: Funext
U: HProp
Y, X: Type
YU: Y -> U
(fun (x : Y -> X * U) (y : Y) => (fst (x y), YU y)) ==
idmap
    -
H: Funext
U: HProp
Y, X: Type
YU: Y -> U
(fun (x : Y -> X) (x0 : Y) => x x0) == idmap intros g; apply path_arrow; intros y; reflexivity.
    -
H: Funext
U: HProp
Y, X: Type
YU: Y -> U
(fun (x : Y -> X * U) (y : Y) => (fst (x y), YU y)) ==
idmap intros h; apply path_arrow; intros y.
H: Funext
U: HProp
Y, X: Type
YU: Y -> U
h: Y -> X * U
y: Y
(fst (h y), YU y) = h y
      apply path_prod; [ reflexivity | by apply path_ishprop ].
  Defined.

  (** Thus, each coreflective subuniverses are uniquely determined by an hprop.  Moreover, the coreflective subuniverse corresponding to an hprop [U] is closely related to the open modality [Op U].  Specifically, they form an _adjoint modality pair_ in the sense that the subuniverses are canonically equivalent, and the coreflection and reflection respect this equivalence.  In categorical language, this says that the inclusion of an open subtopos is the center of a local geometric morphism in the other direction.  We express this concisely as follows. *)

  Definition coopen_isequiv_open X
  : IsEquiv (O_functor (Op U) (fromF coOp X)).
H: Funext
U: HProp
X: Type
O_inverts (Op U) (fromF coOp X)
  Proof.
H: Funext
U: HProp
X: Type
O_inverts (Op U) (fromF coOp X)
    refine (isequiv_adjointify _ (fun ux => fun u => (ux u , u)) _ _).
H: Funext
U: HProp
X: Type
(fun x : U -> X =>
 O_functor (Op U) (fromF coOp X)
   (fun u : U => (x u, u))) == idmap
H: Funext
U: HProp
X: Type
(fun (x : U -> X * U) (u : U) =>
 (O_functor (Op U) (fromF coOp X) x u, u)) == idmap
    -
H: Funext
U: HProp
X: Type
(fun x : U -> X =>
 O_functor (Op U) (fromF coOp X)
   (fun u : U => (x u, u))) == idmap intros ux; simpl in *.
H: Funext
U: HProp
X: Type
ux: U -> X
O_functor (Op U) fst (fun u : U => (ux u, u)) = ux
      apply path_arrow; intros u.
H: Funext
U: HProp
X: Type
ux: U -> X
u: U
O_functor (Op U) fst (fun u : U => (ux u, u)) u = ux u
      transitivity (O_functor (Op U) fst (to (Op U) (X * U) (ux u , u)) u).
H: Funext
U: HProp
X: Type
ux: U -> X
u: U
O_functor (Op U) fst (fun u : U => (ux u, u)) u =
O_functor (Op U) fst (to (Op U) (X * U) (ux u, u)) u
H: Funext
U: HProp
X: Type
ux: U -> X
u: U
O_functor (Op U) fst (to (Op U) (X * U) (ux u, u)) u =
ux u
      +
H: Funext
U: HProp
X: Type
ux: U -> X
u: U
O_functor (Op U) fst (fun u : U => (ux u, u)) u =
O_functor (Op U) fst (to (Op U) (X * U) (ux u, u)) u apply ap10, ap, path_arrow; intros u'; simpl in *.
H: Funext
U: HProp
X: Type
ux: U -> X
u, u': U
(ux u', u') = (ux u, u)
        apply path_prod; simpl; [ apply ap | ]; apply path_ishprop.
      +
H: Funext
U: HProp
X: Type
ux: U -> X
u: U
O_functor (Op U) fst (to (Op U) (X * U) (ux u, u)) u =
ux u exact (ap10 (to_O_natural (Op U) (@fst X U) (ux u , u)) u).
    -
H: Funext
U: HProp
X: Type
(fun (x : U -> X * U) (u : U) =>
 (O_functor (Op U) (fromF coOp X) x u, u)) == idmap intros uux; simpl in *.
H: Funext
U: HProp
X: Type
uux: U -> X * U
(fun u : U => (O_functor (Op U) fst uux u, u)) = uux
      apply path_arrow; intros u.
H: Funext
U: HProp
X: Type
uux: U -> X * U
u: U
(O_functor (Op U) fst uux u, u) = uux u
      apply path_prod; [ simpl | apply path_ishprop ].
H: Funext
U: HProp
X: Type
uux: U -> X * U
u: U
O_functor (Op U) fst uux u = fst (uux u)
      transitivity (O_functor (Op U) fst (to (Op U) _ (fst (uux u) , u)) u).
H: Funext
U: HProp
X: Type
uux: U -> X * U
u: U
O_functor (Op U) fst uux u =
O_functor (Op U) fst
  (to (Op U) (X * U) (fst (uux u), u)) u
H: Funext
U: HProp
X: Type
uux: U -> X * U
u: U
O_functor (Op U) fst
  (to (Op U) (X * U) (fst (uux u), u)) u = fst (uux u)
      +
H: Funext
U: HProp
X: Type
uux: U -> X * U
u: U
O_functor (Op U) fst uux u =
O_functor (Op U) fst
  (to (Op U) (X * U) (fst (uux u), u)) u apply ap10, ap, path_arrow; intros u'.
H: Funext
U: HProp
X: Type
uux: U -> X * U
u, u': U
uux u' = to (Op U) (X * U) (fst (uux u), u) u'
        apply path_prod; simpl.
H: Funext
U: HProp
X: Type
uux: U -> X * U
u, u': U
fst (uux u') = fst (uux u)
H: Funext
U: HProp
X: Type
uux: U -> X * U
u, u': U
snd (uux u') = u
        *
H: Funext
U: HProp
X: Type
uux: U -> X * U
u, u': U
fst (uux u') = fst (uux u) exact (ap fst (ap uux (path_ishprop u' u))).
        *
H: Funext
U: HProp
X: Type
uux: U -> X * U
u, u': U
snd (uux u') = u apply path_ishprop.
      +
H: Funext
U: HProp
X: Type
uux: U -> X * U
u: U
O_functor (Op U) fst
  (to (Op U) (X * U) (fst (uux u), u)) u = fst (uux u) exact (ap10 (to_O_natural (Op U) (@fst X U) (fst (uux u) , u)) u).
  Defined.

  Definition coopen_equiv_open X
  : Op U (coOp X) <~> Op U X
    := Build_Equiv _ _ (O_functor (Op U) (fromF coOp X))
                  (coopen_isequiv_open X).

End CoOpen.