Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Torus improvements, keeping Funext #1825

Merged
merged 6 commits into from
Jan 21, 2024
Merged

Torus improvements, keeping Funext #1825

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
a24d2a9
TorusHomotopy: simpler proof of loops_torus
jdchristensen Jan 20, 2024
8ad2035
Torus: explicitly record the fact that the loops commute
jdchristensen Jan 20, 2024
e07cde2
TorusEquivCircles: remove Section, for speed
jdchristensen Jan 21, 2024
9abe9e3
TorusEquivCircles: change indentation
jdchristensen Jan 21, 2024
13503a5
TorusEquivCircles: use nrefine and nrapply when possible
jdchristensen Jan 21, 2024
721b78c
Torus/*: update comments and naming
jdchristensen Jan 21, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
23 changes: 11 additions & 12 deletions theories/Spaces/Torus/Torus.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,8 +1,7 @@
Require Import Basics.
Require Import Cubical.

(* In this file we define the Torus as a HIT generated by two loops and
a square between them. *)
(** In this file we define the Torus as a HIT generated by two loops and a square between them. *)

Notation hr := (sq_refl_h _).
Notation vr := (sq_refl_v _).
Expand All @@ -16,13 +15,13 @@ Module Export Torus.
Axiom loop_b : tbase = tbase.
Axiom surf : PathSquare loop_a loop_a loop_b loop_b.

(* We define the induction principle for Torus *)
(** We define the induction principle for Torus *)
Definition Torus_ind (P : Torus -> Type) (pb : P tbase)
(pla : DPath P loop_a pb pb) (plb : DPath P loop_b pb pb)
(ps : DPathSquare P surf pla pla plb plb) (x : Torus) : P x
:= (match x with tbase => fun _ _ _ => pb end) pla plb ps.

(* We declare propsitional computational rules for loop_a and loop_b *)
(** We declare propositional computational rules for loop_a and loop_b *)
Axiom Torus_ind_beta_loop_a : forall (P : Torus -> Type) (pb : P tbase)
(pla : DPath P loop_a pb pb) (plb : DPath P loop_b pb pb)
(ps : DPathSquare P surf pla pla plb plb), DPathSquare P hr
Expand All @@ -33,9 +32,7 @@ Module Export Torus.
(ps : DPathSquare P surf pla pla plb plb), DPathSquare P hr
(dp_apD (Torus_ind P pb pla plb ps) (loop_b)) plb 1%dpath 1%dpath.

(* We write out the computation rule for surf even though we will not
use it. Instead we currently have an unfinished recursion computation
principle, but we don't currently know how to derive it from this *)
(** We write out the computation rule for surf even though we will not use it. Instead we currently have an unfinished recursion computation principle, but we don't currently know how to derive it from this *)
Axiom Torus_ind_beta_surf : forall (P : Torus -> Type) (pb : P tbase)
(pla : DPath P loop_a pb pb) (plb : DPath P loop_b pb pb)
(ps : DPathSquare P surf pla pla plb plb),
Expand All @@ -45,12 +42,12 @@ Module Export Torus.

End Torus.

(* We can now define Torus recursion as a sepcial case of Torus induction *)
(** We can now define Torus recursion as a special case of Torus induction *)
Definition Torus_rec (P : Type) (pb : P) (pla plb : pb = pb)
(ps : PathSquare pla pla plb plb) : Torus -> P
:= Torus_ind _ pb (dp_const pla) (dp_const plb) (ds_const ps).

(* We can derive the recursion computation rules for Torus_rec *)
(** We can derive the recursion computation rules for Torus_rec *)
Lemma Torus_rec_beta_loop_a (P : Type) (pb : P) (pla plb : pb = pb)
(ps : PathSquare pla pla plb plb)
: PathSquare (ap (Torus_rec P pb pla plb ps) loop_a) pla 1 1.
Expand All @@ -69,9 +66,7 @@ Proof.
apply moveR_equiv_V, dp_apD_const.
Defined.

(* We ought to be able to prove this from Torus_ind_beta_surf
but it is currently too difficult. Therefore we will leave it
as admitted where it will simply look like an axiom. *)
(** We ought to be able to prove this from Torus_ind_beta_surf but it is currently too difficult. Therefore we will leave it as admitted where it will simply look like an axiom. *)
Definition Torus_rec_beta_surf (P : Type) (pb : P) (pla plb : pb = pb)
(ps : PathSquare pla pla plb plb)
: PathCube (sq_ap (Torus_rec P pb pla plb ps) surf) ps
Expand All @@ -85,6 +80,10 @@ Admitted.
(** The torus is pointed. *)
Global Instance ispointed_torus : IsPointed Torus := tbase.

(** The loops commute. *)
Definition loops_commute_torus : loop_a @ loop_b = loop_b @ loop_a
:= equiv_sq_path^-1 surf.

(* TODO:
(* We ought to be able to prove the computation rules all at the same time *)
(* This gives me the idea of writing all our computation rules as a
Expand Down
Loading
Loading