Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc.Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc.
Require Import Basics.Equivalences Types.Empty Types.Unit Types.Prod.
Require Import Modalities.ReflectiveSubuniverse Truncations.Core.
Require Import Spaces.List.Core.

(** * Path spaces of lists *)

(** This proof was adapted from a proof given in Agda/cubical by Evan Cavallo. *)

Section PathList.
  Context {A : Type}.
  
  (** We'll show that this type is equivalent to the path space [l = l'] in [list A]. *)
  Fixpoint ListEq (l l' : list A) : Type :=
    match l, l' with
      | nil, nil => Unit
      | cons x xs, cons x' xs' => (x = x') * ListEq xs xs'
      | _, _ => Empty
    end.

  #[export] Instance reflexive_listeq : Reflexive ListEq.
A: Type
Reflexive ListEq 
  Proof.
A: Type
Reflexive ListEq
    intros l.
A: Type
l: list A
ListEq l l
    induction l as [| a l IHl].
A: Type
ListEq nil nil
A: Type
a: A
l: list A
IHl: ListEq l l
ListEq (a :: l) (a :: l)
    -
A: Type
ListEq nil nil exact tt.
    -
A: Type
a: A
l: list A
IHl: ListEq l l
ListEq (a :: l) (a :: l) exact (idpath, IHl).
  Defined.

  Local Definition encode {l1 l2} (p : l1 = l2) : ListEq l1 l2.
A: Type
l1, l2: list A
p: l1 = l2
ListEq l1 l2
  Proof.
A: Type
l1, l2: list A
p: l1 = l2
ListEq l1 l2
    by destruct p.
  Defined.

  Local Definition decode {l1 l2} (q : ListEq l1 l2) : l1 = l2.
A: Type
l1, l2: list A
q: ListEq l1 l2
l1 = l2
  Proof.
A: Type
l1, l2: list A
q: ListEq l1 l2
l1 = l2
    induction l1 as [| a l1 IHl1 ] in l2, q |- *.
A: Type
l2: list A
q: ListEq nil l2
nil = l2
A: Type
a: A
l1, l2: list A
q: ListEq (a :: l1) l2
IHl1: forall l0 : list A, ListEq l1 l0 -> l1 = l0
(a :: l1)%list = l2
    1: by destruct l2.
A: Type
a: A
l1, l2: list A
q: ListEq (a :: l1) l2
IHl1: forall l0 : list A, ListEq l1 l0 -> l1 = l0
(a :: l1)%list = l2
    destruct l2.
A: Type
a: A
l1: list A
q: ListEq (a :: l1) nil
IHl1: forall l2 : list A, ListEq l1 l2 -> l1 = l2
(a :: l1)%list = nil
A: Type
a: A
l1: list A
a0: A
l2: list A
q: ListEq (a :: l1) (a0 :: l2)
IHl1: forall l0 : list A, ListEq l1 l0 -> l1 = l0
(a :: l1)%list = (a0 :: l2)%list
    1: contradiction.
A: Type
a: A
l1: list A
a0: A
l2: list A
q: ListEq (a :: l1) (a0 :: l2)
IHl1: forall l0 : list A, ListEq l1 l0 -> l1 = l0
(a :: l1)%list = (a0 :: l2)%list
    destruct q as [p q].
A: Type
a: A
l1: list A
a0: A
l2: list A
p: a = a0
q: ListEq l1 l2
IHl1: forall l0 : list A, ListEq l1 l0 -> l1 = l0
(a :: l1)%list = (a0 :: l2)%list
    exact (ap011 (cons (A:=_)) p (IHl1 _ q)).
  Defined.

  Local Definition decode_refl {l} : decode (reflexivity l) = idpath.
A: Type
l: list A
decode (reflexivity l) = 1
  Proof.
A: Type
l: list A
decode (reflexivity l) = 1
    induction l.
A: Type
decode (reflexivity nil) = 1
A: Type
a: A
l: list A
IHl: decode (reflexivity l) = 1
decode (reflexivity (a :: l)%list) = 1
    1: reflexivity.
A: Type
a: A
l: list A
IHl: decode (reflexivity l) = 1
decode (reflexivity (a :: l)%list) = 1
    exact (ap02 (cons a) IHl).
  Defined.

  Local Definition decode_encode {l1 l2} (p : l1 = l2)
    : decode (encode p) = p.
A: Type
l1, l2: list A
p: l1 = l2
decode (encode p) = p
  Proof.
A: Type
l1, l2: list A
p: l1 = l2
decode (encode p) = p
    destruct p.
A: Type
l1: list A
decode (encode 1) = 1
    exact decode_refl.
  Defined.

  (** By case analysis on both lists, it's easy to show that [ListEq] is [n.+1]-truncated if [A] is [n.+2]-truncated. *)
  #[export] Instance istrunc_listeq n {l1 l2} {H : IsTrunc n.+2 A}
    : IsTrunc n.+1 (ListEq l1 l2).
A: Type
n: trunc_index
l1, l2: list A
H: IsTrunc n.+2 A
IsTrunc n.+1 (ListEq l1 l2)
  Proof.
A: Type
n: trunc_index
l1, l2: list A
H: IsTrunc n.+2 A
IsTrunc n.+1 (ListEq l1 l2)
    induction l1 in l2 |- *.
A: Type
n: trunc_index
l2: list A
H: IsTrunc n.+2 A
IsTrunc n.+1 (ListEq nil l2)
A: Type
n: trunc_index
a: A
l1, l2: list A
H: IsTrunc n.+2 A
IHl1: forall l0 : list A, IsTrunc n.+1 (ListEq l1 l0)
IsTrunc n.+1 (ListEq (a :: l1) l2)
    -
A: Type
n: trunc_index
l2: list A
H: IsTrunc n.+2 A
IsTrunc n.+1 (ListEq nil l2) destruct l2.
A: Type
n: trunc_index
H: IsTrunc n.+2 A
IsTrunc n.+1 (ListEq nil nil)
A: Type
n: trunc_index
a: A
l2: list A
H: IsTrunc n.+2 A
IsTrunc n.+1 (ListEq nil (a :: l2))
      1,2: exact _.
    -
A: Type
n: trunc_index
a: A
l1, l2: list A
H: IsTrunc n.+2 A
IHl1: forall l0 : list A, IsTrunc n.+1 (ListEq l1 l0)
IsTrunc n.+1 (ListEq (a :: l1) l2) destruct l2.
A: Type
n: trunc_index
a: A
l1: list A
H: IsTrunc n.+2 A
IHl1: forall l2 : list A, IsTrunc n.+1 (ListEq l1 l2)
IsTrunc n.+1 (ListEq (a :: l1) nil)
A: Type
n: trunc_index
a: A
l1: list A
a0: A
l2: list A
H: IsTrunc n.+2 A
IHl1: forall l0 : list A, IsTrunc n.+1 (ListEq l1 l0)
IsTrunc n.+1 (ListEq (a :: l1) (a0 :: l2))
      1: exact _.
A: Type
n: trunc_index
a: A
l1: list A
a0: A
l2: list A
H: IsTrunc n.+2 A
IHl1: forall l0 : list A, IsTrunc n.+1 (ListEq l1 l0)
IsTrunc n.+1 (ListEq (a :: l1) (a0 :: l2))
      exact istrunc_prod.
  Defined.

  (** The path space of lists is a retract of [ListEq], therefore it is [n.+1]-truncated if [ListEq] is [n.+1]-truncated. By the previous result, this holds when [A] is [n.+2]-truncated. *) 
  #[export] Instance istrunc_list n {H : IsTrunc n.+2 A} : IsTrunc n.+2 (list A).
A: Type
n: trunc_index
H: IsTrunc n.+2 A
IsTrunc n.+2 (list A)
  Proof.
A: Type
n: trunc_index
H: IsTrunc n.+2 A
IsTrunc n.+2 (list A)
    apply istrunc_S.
A: Type
n: trunc_index
H: IsTrunc n.+2 A
forall x y : list A, IsTrunc n.+1 (x = y)
    intros x y.
A: Type
n: trunc_index
H: IsTrunc n.+2 A
x, y: list A
IsTrunc n.+1 (x = y)
    exact (inO_retract_inO n.+1 _ _ encode decode decode_encode).
  Defined.

  (** With a little more work, we can show that [ListEq] is also a retract of the path space. *)
  Local Definition encode_decode {l1 l2} (p : ListEq l1 l2)
    : encode (decode p) = p.
A: Type
l1, l2: list A
p: ListEq l1 l2
encode (decode p) = p
  Proof.
A: Type
l1, l2: list A
p: ListEq l1 l2
encode (decode p) = p
    induction l1 in l2, p |- *.
A: Type
l2: list A
p: ListEq nil l2
encode (decode p) = p
A: Type
a: A
l1, l2: list A
p: ListEq (a :: l1) l2
IHl1: forall (l0 : list A) (p0 : ListEq l1 l0), encode (decode p0) = p0
encode (decode p) = p
    1: destruct l2; by destruct p.
A: Type
a: A
l1, l2: list A
p: ListEq (a :: l1) l2
IHl1: forall (l0 : list A) (p0 : ListEq l1 l0), encode (decode p0) = p0
encode (decode p) = p
    destruct l2.
A: Type
a: A
l1: list A
p: ListEq (a :: l1) nil
IHl1: forall (l2 : list A) (p0 : ListEq l1 l2), encode (decode p0) = p0
encode (decode p) = p
A: Type
a: A
l1: list A
a0: A
l2: list A
p: ListEq (a :: l1) (a0 :: l2)
IHl1: forall (l0 : list A) (p0 : ListEq l1 l0), encode (decode p0) = p0
encode (decode p) = p
    1: by destruct p.
A: Type
a: A
l1: list A
a0: A
l2: list A
p: ListEq (a :: l1) (a0 :: l2)
IHl1: forall (l0 : list A) (p0 : ListEq l1 l0), encode (decode p0) = p0
encode (decode p) = p
    cbn in p.
A: Type
a: A
l1: list A
a0: A
l2: list A
p: (a = a0) * ListEq l1 l2
IHl1: forall (l0 : list A) (p0 : ListEq l1 l0), encode (decode p0) = p0
encode (decode p) = p
    destruct p as [r p].
A: Type
a: A
l1: list A
a0: A
l2: list A
r: a = a0
p: ListEq l1 l2
IHl1: forall (l0 : list A) (p0 : ListEq l1 l0), encode (decode p0) = p0
encode (decode (r, p)) = (r, p)
    apply path_prod.
A: Type
a: A
l1: list A
a0: A
l2: list A
r: a = a0
p: ListEq l1 l2
IHl1: forall (l0 : list A) (p0 : ListEq l1 l0), encode (decode p0) = p0
fst (encode (decode (r, p))) = fst (r, p)
A: Type
a: A
l1: list A
a0: A
l2: list A
r: a = a0
p: ListEq l1 l2
IHl1: forall (l0 : list A) (p0 : ListEq l1 l0), encode (decode p0) = p0
snd (encode (decode (r, p))) = snd (r, p)
    -
A: Type
a: A
l1: list A
a0: A
l2: list A
r: a = a0
p: ListEq l1 l2
IHl1: forall (l0 : list A) (p0 : ListEq l1 l0), encode (decode p0) = p0
fst (encode (decode (r, p))) = fst (r, p) simpl.
A: Type
a: A
l1: list A
a0: A
l2: list A
r: a = a0
p: ListEq l1 l2
IHl1: forall (l0 : list A) (p0 : ListEq l1 l0), encode (decode p0) = p0
fst (encode (ap011 cons r (decode p))) = r
      destruct (decode p).
A: Type
a: A
l1: list A
a0: A
r: a = a0
p: ListEq l1 l1
IHl1: forall (l2 : list A) (p0 : ListEq l1 l2), encode (decode p0) = p0
fst (encode (ap011 cons r 1)) = r
      by destruct r.
    -
A: Type
a: A
l1: list A
a0: A
l2: list A
r: a = a0
p: ListEq l1 l2
IHl1: forall (l0 : list A) (p0 : ListEq l1 l0), encode (decode p0) = p0
snd (encode (decode (r, p))) = snd (r, p) rhs_V napply IHl1.
A: Type
a: A
l1: list A
a0: A
l2: list A
r: a = a0
p: ListEq l1 l2
IHl1: forall (l0 : list A) (p0 : ListEq l1 l0), encode (decode p0) = p0
snd (encode (decode (r, p))) = encode (decode (snd (r, p)))
      simpl.
A: Type
a: A
l1: list A
a0: A
l2: list A
r: a = a0
p: ListEq l1 l2
IHl1: forall (l0 : list A) (p0 : ListEq l1 l0), encode (decode p0) = p0
snd (encode (ap011 cons r (decode p))) = encode (decode p)
      destruct (decode p).
A: Type
a: A
l1: list A
a0: A
r: a = a0
p: ListEq l1 l1
IHl1: forall (l2 : list A) (p0 : ListEq l1 l2), encode (decode p0) = p0
snd (encode (ap011 cons r 1)) = encode 1
      by destruct r.
  Defined.

  (** Giving us a way of characterizing paths in lists. *)
  Definition equiv_path_list {l1 l2}
    : ListEq l1 l2 <~> l1 = l2
    := equiv_adjointify decode encode decode_encode encode_decode.

End PathList.