From 4a3547982603cb3d6a6abf13ce029021506b3860 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sun, 14 Apr 2024 18:55:09 +0100 Subject: [PATCH 1/3] truncation level of lists Signed-off-by: Ali Caglayan --- theories/Spaces/List.v | 83 ++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 79 insertions(+), 4 deletions(-) diff --git a/theories/Spaces/List.v b/theories/Spaces/List.v index b6df01f77ac..2d731c03af4 100644 --- a/theories/Spaces/List.v +++ b/theories/Spaces/List.v @@ -1,12 +1,13 @@ -Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids. -Require Import Classes.implementations.list. +Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc. +Require Import Classes.implementations.list Types.Unit Types.Empty Types.Prod. +Require Import Modalities.ReflectiveSubuniverse Truncations.Core. Local Open Scope list_scope. -(** ** Lemmas about lists *) - (** Note that [list] is currently defined in Basics.Datatypes. *) +(** ** Lemmas about lists *) + Section Fold_Left_Recursor. Variables (A : Type) (B : Type). Variable f : A -> B -> A. @@ -69,3 +70,77 @@ Proof. lhs_V nrapply ap_compose. nrapply (ap_compose (fun l => l ++ z)). Defined. + +(** ** Path spaces of lists *) + +(** This proof was adapted from a proof givaen in agda/cubical by Evan Cavallo. *) + +Section PathList. + Context {A : Type}. + + (** This type is equivalent to the path space of lists. We don't actually show that it is equivalent to the type of paths but rather that it is a retract of it. This is sufficient to determine the h-level of the type of lists. *) + 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. + + Global Instance reflexive_listeq : Reflexive ListEq. + Proof. + intros l. + induction l as [| a l IHl]. + - exact tt. + - by split. + Defined. + + Local Definition encode {l1 l2} (p : l1 = l2) : ListEq l1 l2. + Proof. + by destruct p. + Defined. + + Local Definition decode {l1 l2} (q : ListEq l1 l2) : l1 = l2. + Proof. + induction l1 as [| a l1 IHl1 ] in l2, q |- *. + 1: by destruct l2. + destruct l2. + 1: contradiction. + destruct q as [p q]. + exact (ap011 (cons (A:=_)) p (IHl1 _ q)). + Defined. + + Local Definition decode_refl {l} : decode (reflexivity l) = idpath. + Proof. + induction l. + 1: reflexivity. + exact (ap02 (cons a) IHl). + Defined. + + Local Definition decode_encode {l1 l2} (p : l1 = l2) + : decode (encode p) = p. + Proof. + destruct p. + apply 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. *) + Global Instance istrunc_listeq n {l1 l2} {H : IsTrunc n.+2 A} + : IsTrunc n.+1 (ListEq l1 l2). + Proof. + induction l1 in l2 |- *. + - destruct l2. + 1,2: exact _. + - destruct l2. + 1: exact _. + rapply istrunc_prod. + Defined. + + (** Since [ListEq] is a retract of the path space of lists, the latter is n.+1-truncated hence [list A] is n.+2-truncated. *) + Global Instance istrunc_list n {H : IsTrunc n.+2 A} : IsTrunc n.+2 (list A). + Proof. + apply istrunc_S. + intros x y. + rapply (inO_retract_inO n.+1 _ _ encode decode decode_encode). + Defined. + +End PathList. From ece8fa66f9141ba3c1ca231b598e73612422aca8 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 15 Apr 2024 20:24:45 +0100 Subject: [PATCH 2/3] review comments Signed-off-by: Ali Caglayan --- theories/Spaces/List.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/theories/Spaces/List.v b/theories/Spaces/List.v index 2d731c03af4..b5437caabb6 100644 --- a/theories/Spaces/List.v +++ b/theories/Spaces/List.v @@ -78,7 +78,7 @@ Defined. Section PathList. Context {A : Type}. - (** This type is equivalent to the path space of lists. We don't actually show that it is equivalent to the type of paths but rather that it is a retract of it. This is sufficient to determine the h-level of the type of lists. *) + (** This type is equivalent to the path space of lists. We don't actually show that it is equivalent to the type of paths but rather that the path type is a retract of this type. This is sufficient to determine the h-level of the type of lists. *) Fixpoint ListEq (l l' : list A) : Type := match l, l' with | nil, nil => Unit @@ -91,7 +91,7 @@ Section PathList. intros l. induction l as [| a l IHl]. - exact tt. - - by split. + - exact (idpath, IHl). Defined. Local Definition encode {l1 l2} (p : l1 = l2) : ListEq l1 l2. @@ -123,7 +123,7 @@ Section PathList. apply 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. *) + (** By case analysis on both lists, it's easy to show that [ListEq] is [n.+1]-truncated if [A] is [n.+2]-truncated. *) Global Instance istrunc_listeq n {l1 l2} {H : IsTrunc n.+2 A} : IsTrunc n.+1 (ListEq l1 l2). Proof. @@ -135,7 +135,7 @@ Section PathList. rapply istrunc_prod. Defined. - (** Since [ListEq] is a retract of the path space of lists, the latter is n.+1-truncated hence [list A] is n.+2-truncated. *) + (** 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. *) Global Instance istrunc_list n {H : IsTrunc n.+2 A} : IsTrunc n.+2 (list A). Proof. apply istrunc_S. From 095817a887c4deb2687304719ebfb01c4d0c8884 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 15 Apr 2024 20:39:37 +0100 Subject: [PATCH 3/3] typo --- theories/Spaces/List.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Spaces/List.v b/theories/Spaces/List.v index b5437caabb6..13e40c53716 100644 --- a/theories/Spaces/List.v +++ b/theories/Spaces/List.v @@ -73,7 +73,7 @@ Defined. (** ** Path spaces of lists *) -(** This proof was adapted from a proof givaen in agda/cubical by Evan Cavallo. *) +(** This proof was adapted from a proof given in agda/cubical by Evan Cavallo. *) Section PathList. Context {A : Type}.