Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]


Local Open Scope pointed_scope.

(** * Modalities, reflective subuniverses and pointed types *)

(** So far, everything is about general reflective subuniverses, but in the future results about modalities can be placed here as well. *)

Global Instance ispointed_O `{O : ReflectiveSubuniverse} (X : Type)
  `{IsPointed X} : IsPointed (O X) := to O _ (point X).

Definition pto (O : ReflectiveSubuniverse@{u}) (X : pType@{u})
  : X ->* [O X, _]
  := Build_pMap X [O X, _] (to O X) idpath.

(** If [A] is already [O]-local, then Coq knows that [pto] is an equivalence, so we can simply define: *)
Definition pequiv_pto `{O : ReflectiveSubuniverse} {X : pType} `{In O X}
  : X <~>* [O X, _] := Build_pEquiv _ _ (pto O X) _.

(** Applying [O_rec] to a pointed map yields a pointed map. *)
Definition pO_rec `{O : ReflectiveSubuniverse} {X Y : pType}
  `{In O Y} (f : X ->* Y) : [O X, _] ->* Y
  := Build_pMap [O X, _] _ (O_rec f) (O_rec_beta _ _ @ point_eq f).


O: ReflectiveSubuniverse
X, Y: pType
H: In O Y
f: X ->* Y
pO_rec f o* pto O X ==* f


O: ReflectiveSubuniverse
X, Y: pType
H: In O Y
f: X ->* Y
pO_rec f o* pto O X ==* f

  
O: ReflectiveSubuniverse
X, Y: pType
H: In O Y
f: X ->* Y
pO_rec f o* pto O X == f
O: ReflectiveSubuniverse
X, Y: pType
H: In O Y
f: X ->* Y
?p pt =
dpoint_eq (pO_rec f o* pto O X) @ (dpoint_eq f)^

  
O: ReflectiveSubuniverse
X, Y: pType
H: In O Y
f: X ->* Y
O_rec_beta f pt =
dpoint_eq (pO_rec f o* pto O X) @ (dpoint_eq f)^

  
O: ReflectiveSubuniverse
X, Y: pType
H: In O Y
f: X ->* Y
O_rec_beta f pt =
(1 @ (O_rec_beta f pt @ point_eq f)) @ (dpoint_eq f)^

  
O: ReflectiveSubuniverse
X, Y: pType
H: In O Y
f: X ->* Y
O_rec_beta f pt @ dpoint_eq f =
1 @ (O_rec_beta f pt @ point_eq f)

  exact (concat_1p _)^.
Defined.

(** A pointed version of the universal property. *)

H: Funext
O: ReflectiveSubuniverse
P, Q: pType
H0: In O Q
([O P, ispointed_O P] ->** Q) <~>* (P ->** Q)


H: Funext
O: ReflectiveSubuniverse
P, Q: pType
H0: In O Q
([O P, ispointed_O P] ->** Q) <~>* (P ->** Q)

  
H: Funext
O: ReflectiveSubuniverse
P, Q: pType
H0: In O Q
([O P, ispointed_O P] ->** Q) ->* (P ->** Q)
H: Funext
O: ReflectiveSubuniverse
P, Q: pType
H0: In O Q
IsEquiv ?pointed_equiv_fun

  (* We could just use the map [e] defined in the next bullet, but we want Coq to immediately unfold the underlying map to this. *)
  
H: Funext
O: ReflectiveSubuniverse
P, Q: pType
H0: In O Q
([O P, ispointed_O P] ->** Q) ->* (P ->** Q)
 exact (Build_pMap _ _ (fun f => f o* pto O P) 1).
  (* We'll give an equivalence that definitionally has the same underlying map. *)
  
H: Funext
O: ReflectiveSubuniverse
P, Q: pType
H0: In O Q
IsEquiv
  (Build_pMap ([O P, ispointed_O P] ->** Q) (P ->** Q)
     (fun f : [O P, ispointed_O P] ->** Q =>
      f o* pto O P) 1)
 
H: Funext
O: ReflectiveSubuniverse
P, Q: pType
H0: In O Q
([O P, ispointed_O P] ->* Q) <~> (P ->* Q)
H: Funext
O: ReflectiveSubuniverse
P, Q: pType
H0: In O Q
e:= ?Goal: ([O P, ispointed_O P] ->* Q) <~> (P ->* Q)
IsEquiv
  (Build_pMap ([O P, ispointed_O P] ->** Q) (P ->** Q)
     (fun f : [O P, ispointed_O P] ->** Q =>
      f o* pto O P) 1)

    
H: Funext
O: ReflectiveSubuniverse
P, Q: pType
H0: In O Q
([O P, ispointed_O P] ->* Q) <~> (P ->* Q)
 
H: Funext
O: ReflectiveSubuniverse
P, Q: pType
H0: In O Q
{f : [O P, ispointed_O P] -> Q & f pt = pt} <~>
{f : P -> Q & f pt = pt}

      
H: Funext
O: ReflectiveSubuniverse
P, Q: pType
H0: In O Q
([O P, ispointed_O P] -> Q) <~> (P -> Q)
H: Funext
O: ReflectiveSubuniverse
P, Q: pType
H0: In O Q
forall a : [O P, ispointed_O P] -> Q,
(fun f : [O P, ispointed_O P] -> Q => f pt = pt) a <~>
(fun f : P -> Q => f pt = pt) (?f a)

      
H: Funext
O: ReflectiveSubuniverse
P, Q: pType
H0: In O Q
([O P, ispointed_O P] -> Q) <~> (P -> Q)
 rapply equiv_o_to_O.
      
H: Funext
O: ReflectiveSubuniverse
P, Q: pType
H0: In O Q
forall a : [O P, ispointed_O P] -> Q,
(fun f : [O P, ispointed_O P] -> Q => f pt = pt) a <~>
(fun f : P -> Q => f pt = pt) (equiv_o_to_O O P Q a)
 
H: Funext
O: ReflectiveSubuniverse
P, Q: pType
H0: In O Q
f: [O P, ispointed_O P] -> Q
f (ispointed_O P) = pt <~> f (to O P pt) = pt

      (* [reflexivity] works here, but then the underlying map won't agree definitionally with precomposition by [pto P], since pointed composition inserts a reflexivity path here. *)
      apply (equiv_concat_l 1).
    
H: Funext
O: ReflectiveSubuniverse
P, Q: pType
H0: In O Q
e:= issig_pmap P Q
oE equiv_functor_sigma' (equiv_o_to_O O P Q)
     (fun f : [O P, ispointed_O P] -> Q =>
      equiv_concat_l 1 pt
      :
      (fun f0 : [O P, ispointed_O P] -> Q =>
       f0 pt = pt) f <~>
      (fun f0 : P -> Q => f0 pt = pt)
        (equiv_o_to_O O P Q f))
oE (issig_pmap [O P, ispointed_O P] Q)^-1: ([O P, ispointed_O P] ->* Q) <~> (P ->* Q)
IsEquiv
  (Build_pMap ([O P, ispointed_O P] ->** Q) (P ->** Q)
     (fun f : [O P, ispointed_O P] ->** Q =>
      f o* pto O P) 1)
 apply (equiv_isequiv e).
Defined.

(** ** Pointed functoriality *)

Definition O_pfunctor `(O : ReflectiveSubuniverse) {X Y : pType}
  (f : X ->* Y) : [O X, _] ->* [O Y, _]
  := pO_rec (pto O Y o* f).

(** Coq knows that [O_pfunctor O f] is an equivalence whenever [f] is. *)
Definition equiv_O_pfunctor `(O : ReflectiveSubuniverse) {X Y : pType}
  (f : X ->* Y) `{IsEquiv _ _ f} : [O X, _] <~>* [O Y, _]
  := Build_pEquiv _ _ (O_pfunctor O f) _.

(** Pointed naturality of [O_pfunctor]. *)

O: ReflectiveSubuniverse
X, Y: pType
f: X ->* Y
O_pfunctor O f o* pto O X ==* pto O Y o* f


O: ReflectiveSubuniverse
X, Y: pType
f: X ->* Y
O_pfunctor O f o* pto O X ==* pto O Y o* f

  nrapply pO_rec_beta.
Defined.

Definition pequiv_O_inverts `(O : ReflectiveSubuniverse) {X Y : pType}
  (f : X ->* Y) `{O_inverts O f}
  : [O X, _] <~>* [O Y, _]
  := Build_pEquiv _ _ (O_pfunctor O f) _.