From HoTT Require Import Basics Types.From HoTT Require Import Basics Types.
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. *)
#[export] 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. *)
#[export] 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.

#[export] 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'0 : A -> Type) (P_inO0 : forall x0 : A, In (Tr n) (P'0 x0)) =>
    let P0 :=
      fun x0 : A =>
      {|
        trunctype_type := P'0 x0;
        trunctype_istrunc := istrunc_inO_tr (P'0 x0)
      |} in
    ?Goal@{P':=P'0; P_inO:=P_inO0}) 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'0 : A -> Type) (P_inO0 : forall x0 : A, In (Tr n) (P'0 x0)) =>
 let P0 :=
   fun x0 : A =>
   {|
     trunctype_type := P'0 x0; trunctype_istrunc := istrunc_inO_tr (P'0 x0)
   |} in
 ?Goal@{P':=P'0; P_inO:=P_inO0}) 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 exact (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'0 : A -> Type) (P_inO0 : forall x0 : A, In (Tr n) (P'0 x0)) =>
    let P0 :=
      fun x0 : A =>
      {|
        trunctype_type := P'0 x0;
        trunctype_istrunc := istrunc_inO_tr (P'0 x0)
      |} in
    fun x0 : O_reflector (Tr n.+1) A => trunctype_type (Trunc_rec P0 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'0 : A -> Type) (P_inO0 : forall x0 : A, In (Tr n) (P'0 x0)) =>
 let P0 :=
   fun x0 : A =>
   {|
     trunctype_type := P'0 x0; trunctype_istrunc := istrunc_inO_tr (P'0 x0)
   |} in
 fun x0 : O_reflector (Tr n.+1) A => trunctype_type (Trunc_rec P0 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 x0 : A, In (Tr n) (P' x0)
P:= fun x0 : A =>
{| trunctype_type := P' x0; trunctype_istrunc := istrunc_inO_tr (P' x0) |}: 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.