Library UniMath.Ktheory.Halfline
Require Import UniMath.Foundations.UnivalenceAxiom
UniMath.Ktheory.Utilities.
Require Import UniMath.CategoryTheory.Core.Categories.
Require UniMath.Ktheory.Nat.
Notation ℕ := nat.
Definition target_paths {Y} (f:ℕ->Y) := ∏ n, f n=f(S n).
Definition gHomotopy {Y} (f:ℕ->Y) (s:target_paths f) := fun
y:Y => ∑ (h:nullHomotopyFrom f y), ∏ n, h(S n) = h n @ s n.
Definition GuidedHomotopy {Y} (f:ℕ->Y) (s:target_paths f) :=
total2 (gHomotopy f s).
Theorem iscontrGuidedHomotopy {Y} {f:ℕ->Y} (s:target_paths f) :
iscontr (GuidedHomotopy f s).
Show proof.
intros. unfold GuidedHomotopy, nullHomotopyFrom.
refine (@iscontrweqb _ (∑ y, y=f 0) _ _).
{ apply weqfibtototal. intro y.
exact (Nat.Uniqueness.hNatRecursion_weq
(λ n, y = f n) (λ n hn, hn @ s n)). }
{ apply iscontrcoconustot. }
refine (@iscontrweqb _ (∑ y, y=f 0) _ _).
{ apply weqfibtototal. intro y.
exact (Nat.Uniqueness.hNatRecursion_weq
(λ n, y = f n) (λ n hn, hn @ s n)). }
{ apply iscontrcoconustot. }
Definition halfline := ∥ ℕ ∥.
Definition makeNullHomotopy {Y} {f:ℕ->Y} (s:target_paths f) {y:Y} (h0:y=f 0) :
nullHomotopyFrom f y.
Show proof.
intros. intro n. induction n as [|n IHn]. { exact (h0). } { exact (IHn @ s _). }
Definition map {Y} {f:ℕ->Y} (s:target_paths f) :
halfline -> GuidedHomotopy f s.
Show proof.
intros r. apply (squash_to_prop r).
{ apply isapropifcontr. apply iscontrGuidedHomotopy. }
{ intro n. exists (f n). induction n as [|n IHn].
{ exists (makeNullHomotopy s (idpath _)). intro n. reflexivity. }
{ exact (transportf (gHomotopy f s) (s n) IHn). } }
{ apply isapropifcontr. apply iscontrGuidedHomotopy. }
{ intro n. exists (f n). induction n as [|n IHn].
{ exists (makeNullHomotopy s (idpath _)). intro n. reflexivity. }
{ exact (transportf (gHomotopy f s) (s n) IHn). } }
Definition map_path {Y} {f:ℕ->Y} (s:target_paths f) :
∏ n, map s (squash_element n) = map s (squash_element (S n)).
Show proof.
intros. apply (two_arg_paths_f (s n)).
simpl. reflexivity.
simpl. reflexivity.
Definition map_path_check {Y} {f:ℕ->Y} (s:target_paths f) (n:ℕ) :
∏ p : map s (squash_element n) = map s (squash_element (S n)),
ap pr1 p = s n.
Show proof.
intros. set (q := map_path s n).
assert (path_inverse_to_right : q=p).
{ apply (hlevelntosn 1). apply (hlevelntosn 0). apply iscontrGuidedHomotopy. }
destruct path_inverse_to_right. apply total2_paths2_comp1.
assert (path_inverse_to_right : q=p).
{ apply (hlevelntosn 1). apply (hlevelntosn 0). apply iscontrGuidedHomotopy. }
destruct path_inverse_to_right. apply total2_paths2_comp1.
Definition halfline_map {Y} {target_points:ℕ->Y} (s:target_paths target_points) :
halfline -> Y.
Show proof.
intros r. exact (pr1 (map s r)).
Definition check_values {Y} {target_points:ℕ->Y}
(s:target_paths target_points) (n:ℕ) :
halfline_map s (squash_element n) = target_points n.
Show proof.
reflexivity.
Definition check_paths {Y} {target_points:ℕ->Y}
(s:target_paths target_points) (n:ℕ) :
ap (halfline_map s) (squash_path n (S n)) = s n.
Show proof.
intros. refine (_ @ map_path_check s n _).
apply pathsinv0. apply maponpathscomp.
apply pathsinv0. apply maponpathscomp.