Library HoTT.Spaces.NatSeq.UStructure
From HoTT Require Import Basics Types.
Require Import Spaces.Nat.Core.
Require Import Misc.UStructures.
Require Import List.Core List.Theory.
Require Import Spaces.NatSeq.Core.
Local Open Scope nat_scope.
Local Open Scope type_scope.
UStructure defined by seq_agree_lt
Instance sequence_type_us {X : Type} : UStructure (nat → X) | 10.
Proof.
snapply Build_UStructure.
- exact seq_agree_lt.
- exact (fun _ _ _ _ ⇒ idpath).
- exact (fun _ _ _ h _ _ ⇒ (h _ _)^).
- exact (fun _ _ _ _ h1 h2 _ _ ⇒ ((h1 _ _) @ (h2 _ _))).
- exact (fun _ _ _ h _ _ ⇒ h _ _).
Defined.
Definition sequence_type_us_zero {X : Type} (s t : nat → X) : s =[0] t
:= fun n hn ⇒ Empty_rec (not_lt_zero_r n hn).
Definition seq_cons_of_eq {X : Type} {n : nat} {s t : nat → X} {x : X}
(h : s =[n] t)
: (seq_cons x s) =[n.+1] (seq_cons x t).
Proof.
intros m hm; destruct m.
- reflexivity.
- exact (h m _).
Defined.
Proof.
snapply Build_UStructure.
- exact seq_agree_lt.
- exact (fun _ _ _ _ ⇒ idpath).
- exact (fun _ _ _ h _ _ ⇒ (h _ _)^).
- exact (fun _ _ _ _ h1 h2 _ _ ⇒ ((h1 _ _) @ (h2 _ _))).
- exact (fun _ _ _ h _ _ ⇒ h _ _).
Defined.
Definition sequence_type_us_zero {X : Type} (s t : nat → X) : s =[0] t
:= fun n hn ⇒ Empty_rec (not_lt_zero_r n hn).
Definition seq_cons_of_eq {X : Type} {n : nat} {s t : nat → X} {x : X}
(h : s =[n] t)
: (seq_cons x s) =[n.+1] (seq_cons x t).
Proof.
intros m hm; destruct m.
- reflexivity.
- exact (h m _).
Defined.
We can also rephrase the definition of seq_agree_lt using the list_restrict function.
Definition list_restrict_eq_iff_seq_agree_lt
{A : Type} {n : nat} {s t : nat → A}
: (list_restrict s n = list_restrict t n) ↔ s =[n] t.
Proof.
constructor.
- intros h m hm.
lhs_V exact (nth'_list_restrict s ((length_list_restrict _ _)^ # hm)).
rhs_V exact (nth'_list_restrict t ((length_list_restrict _ _)^ # hm)).
exact (nth'_path_list h _ _).
- intro h.
apply (path_list_nth' _ _
(length_list_restrict s n @ (length_list_restrict t n)^)).
intros i Hi.
lhs snapply nth'_list_restrict.
rhs snapply nth'_list_restrict.
exact (h i ((length_list_restrict s n) # Hi)).
Defined.
Definition list_restrict_eq_iff_seq_agree_inductive
{A : Type} {n : nat} {s t : nat → A}
: list_restrict s n = list_restrict t n ↔ seq_agree_inductive n s t
:= iff_compose
list_restrict_eq_iff_seq_agree_lt
seq_agree_lt_iff_seq_agree_inductive.
{A : Type} {n : nat} {s t : nat → A}
: (list_restrict s n = list_restrict t n) ↔ s =[n] t.
Proof.
constructor.
- intros h m hm.
lhs_V exact (nth'_list_restrict s ((length_list_restrict _ _)^ # hm)).
rhs_V exact (nth'_list_restrict t ((length_list_restrict _ _)^ # hm)).
exact (nth'_path_list h _ _).
- intro h.
apply (path_list_nth' _ _
(length_list_restrict s n @ (length_list_restrict t n)^)).
intros i Hi.
lhs snapply nth'_list_restrict.
rhs snapply nth'_list_restrict.
exact (h i ((length_list_restrict s n) # Hi)).
Defined.
Definition list_restrict_eq_iff_seq_agree_inductive
{A : Type} {n : nat} {s t : nat → A}
: list_restrict s n = list_restrict t n ↔ seq_agree_inductive n s t
:= iff_compose
list_restrict_eq_iff_seq_agree_lt
seq_agree_lt_iff_seq_agree_inductive.
Continuity
Definition uniformly_continuous_extensionality
{X Y : Type} {usY : UStructure Y} (p : (nat → X) → Y) {m : nat}
(c : uniformly_continuous p)
{u v : nat → X} (h : u == v)
: p u =[m] p v
:= (c m).2 u v (fun m _ ⇒ h m).
{X Y : Type} {usY : UStructure Y} (p : (nat → X) → Y) {m : nat}
(c : uniformly_continuous p)
{u v : nat → X} (h : u == v)
: p u =[m] p v
:= (c m).2 u v (fun m _ ⇒ h m).