(* -*- mode: coq; mode: visual-line -*- *)

Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import TruncType.
Require Import Truncations.Core Modalities.Modality Modalities.Descent.

(** ** Separatedness and path-spaces of truncations *)

Section SeparatedTrunc.

Local Open Scope subuniverse_scope.

(** The [n.+1]-truncation modality consists of the separated types for the [n]-truncation modality. *)
Global Instance O_eq_Tr (n : trunc_index)
  : Tr n.+1 <=> Sep (Tr n).
n: trunc_index
Tr n.+1 <=> Sep (Tr n)
Proof.
n: trunc_index
Tr n.+1 <=> Sep (Tr n)
  split; intros A A_inO.
n: trunc_index
A: Type
A_inO: In (Tr n.+1) A
In (Sep (Tr n)) A
n: trunc_index
A: Type
A_inO: In (Sep (Tr n)) A
In (Tr n.+1) A
  -
n: trunc_index
A: Type
A_inO: In (Tr n.+1) A
In (Sep (Tr n)) A intros x y; exact _.
  -
n: trunc_index
A: Type
A_inO: In (Sep (Tr n)) A
In (Tr n.+1) A rapply istrunc_S.
Defined.

(** It follows that [Tr n <<< Tr n.+1].  However, it is easier to prove this directly than to go through separatedness. *)
Global Instance O_leq_Tr (n : trunc_index)
  : Tr n <= Tr n.+1.
n: trunc_index
Tr n <= Tr n.+1
Proof.
n: trunc_index
Tr n <= Tr n.+1
  intros A ?; exact _.
Defined.

Global Instance O_strong_leq_Tr (n : trunc_index)
  : Tr n << Tr n.+1.
n: trunc_index
Tr n << Tr n.+1
Proof.
n: trunc_index
Tr n << Tr n.+1
  srapply O_strong_leq_trans_l.
Defined.

(** For some reason, this causes typeclass search to spin. *)
Local Instance O_lex_leq_Tr `{Univalence} (n : trunc_index)
  : Tr n <<< Tr n.+1.
H: Univalence
n: trunc_index
Tr n <<< Tr n.+1
Proof.
H: Univalence
n: trunc_index
Tr n <<< Tr n.+1
  intros A; unshelve econstructor; intros P' P_inO;
    pose (P := fun x => Build_TruncType n (P' x)).
H: Univalence
n: trunc_index
A: Type
P': A -> Type
P_inO: forall x : A, In (Tr n) (P' x)
P:= fun x : A =>
{|
  trunctype_type := P' x;
  trunctype_istrunc := istrunc_inO_tr (P' x)
|}: A -> n -Type
O_reflector (Tr n.+1) A -> Type
H: Univalence
n: trunc_index
A: Type
P': A -> Type
P_inO: forall x : A, In (Tr n) (P' x)
P:= fun x : A =>
{|
  trunctype_type := P' x;
  trunctype_istrunc := istrunc_inO_tr (P' x)
|}: A -> n -Type
forall x : O_reflector (Tr n.+1) A,
In (Tr n)
  ((fun (P' : A -> Type)
      (P_inO : forall x0 : A, In (Tr n) (P' x0)) =>
    let P :=
      fun x0 : A =>
      {|
        trunctype_type := P' x0;
        trunctype_istrunc := istrunc_inO_tr (P' x0)
      |} in
    ?Goal) P' P_inO x)
H: Univalence
n: trunc_index
A: Type
P': A -> Type
P_inO: forall x : A, In (Tr n) (P' x)
P:= fun x : A =>
{|
  trunctype_type := P' x;
  trunctype_istrunc := istrunc_inO_tr (P' x)
|}: A -> n -Type
forall x : A,
(fun (P' : A -> Type)
   (P_inO : forall x0 : A, In (Tr n) (P' x0)) =>
 let P :=
   fun x0 : A =>
   {|
     trunctype_type := P' x0;
     trunctype_istrunc := istrunc_inO_tr (P' x0)
   |} in
 ?Goal) P' P_inO (to (Tr n.+1) A x) <~> 
P' x
  -
H: Univalence
n: trunc_index
A: Type
P': A -> Type
P_inO: forall x : A, In (Tr n) (P' x)
P:= fun x : A =>
{|
  trunctype_type := P' x;
  trunctype_istrunc := istrunc_inO_tr (P' x)
|}: A -> n -Type
O_reflector (Tr n.+1) A -> Type refine (Trunc_rec P).
  -
H: Univalence
n: trunc_index
A: Type
P': A -> Type
P_inO: forall x : A, In (Tr n) (P' x)
P:= fun x : A =>
{|
  trunctype_type := P' x;
  trunctype_istrunc := istrunc_inO_tr (P' x)
|}: A -> n -Type
forall x : O_reflector (Tr n.+1) A,
In (Tr n)
  ((fun (P' : A -> Type)
      (P_inO : forall x0 : A, In (Tr n) (P' x0)) =>
    let P :=
      fun x0 : A =>
      {|
        trunctype_type := P' x0;
        trunctype_istrunc := istrunc_inO_tr (P' x0)
      |} in
    fun x0 : O_reflector (Tr n.+1) A =>
    trunctype_type (Trunc_rec P x0)) P' P_inO x) intros; simpl; exact _.
  -
H: Univalence
n: trunc_index
A: Type
P': A -> Type
P_inO: forall x : A, In (Tr n) (P' x)
P:= fun x : A =>
{|
  trunctype_type := P' x;
  trunctype_istrunc := istrunc_inO_tr (P' x)
|}: A -> n -Type
forall x : A,
(fun (P' : A -> Type)
   (P_inO : forall x0 : A, In (Tr n) (P' x0)) =>
 let P :=
   fun x0 : A =>
   {|
     trunctype_type := P' x0;
     trunctype_istrunc := istrunc_inO_tr (P' x0)
   |} in
 fun x0 : O_reflector (Tr n.+1) A =>
 trunctype_type (Trunc_rec P x0)) P' P_inO
  (to (Tr n.+1) A x) <~> P' x intros; cbn.
H: Univalence
n: trunc_index
A: Type
P': A -> Type
P_inO: forall x : A, In (Tr n) (P' x)
P:= fun x : A =>
{|
  trunctype_type := P' x;
  trunctype_istrunc := istrunc_inO_tr (P' x)
|}: A -> n -Type
x: A
P' x <~> P' x reflexivity.
Defined.

Definition path_Tr {n A} {x y : A}
  : Tr n (x = y) -> (tr x = tr y :> Tr n.+1 A)
  := path_OO (Tr n.+1) (Tr n) x y.

Definition equiv_path_Tr `{Univalence} {n} {A : Type} (x y : A)
  : Tr n (x = y) <~> (tr x = tr y :> Tr n.+1 A)
  := equiv_path_OO (Tr n.+1) (Tr n) x y.

End SeparatedTrunc.