Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Cubical.DPath Cubical.PathSquare Cubical.DPathSquare
  Cubical.PathCube Cubical.DPathCube.
Require Import Spaces.Circle Spaces.Torus.Torus.

(** In this file we prove that the torus is equivalent to the product of two circles. *)

(** Here is a cube filler for help with circle recursion into the torus *)
Definition c2t_square_and_cube
  : {s : PathSquare loop_a loop_a
      (ap (Circle_rec _ tbase loop_b) loop)
      (ap (Circle_rec _ tbase loop_b) loop)
    &  PathCube s surf hr hr
       (sq_G1 (Circle_rec_beta_loop _ _ _))
       (sq_G1 (Circle_rec_beta_loop _ _ _))}.
{s
: PathSquare loop_a loop_a
    (ap (Circle_rec Torus tbase loop_b) loop)
    (ap (Circle_rec Torus tbase loop_b) loop) &
PathCube s surf hr hr
  (sq_G1 (Circle_rec_beta_loop Torus tbase loop_b))
  (sq_G1 (Circle_rec_beta_loop Torus tbase loop_b))}
Proof.
{s
: PathSquare loop_a loop_a
    (ap (Circle_rec Torus tbase loop_b) loop)
    (ap (Circle_rec Torus tbase loop_b) loop) &
PathCube s surf hr hr
  (sq_G1 (Circle_rec_beta_loop Torus tbase loop_b))
  (sq_G1 (Circle_rec_beta_loop Torus tbase loop_b))}
  apply cu_fill_left.
Defined.

(** We define the map from the Torus to the Circles *)
Definition t2c : Torus -> Circle * Circle.
Torus -> Circle * Circle
Proof.
Torus -> Circle * Circle
  snapply Torus_rec.
Circle * Circle
?pb = ?pb
?pb = ?pb
PathSquare ?pla ?pla ?plb ?plb
  +
Circle * Circle exact (base, base). (* The point of the torus is taken to (base, base *)
  +
(base, base) = (base, base) exact (path_prod' loop 1). (* loop_a is taken to loop in the first *)
  +
(base, base) = (base, base) exact (path_prod' 1 loop). (* loop_b is taken to loop in the second *)
  +
PathSquare (path_prod' loop 1) (path_prod' loop 1)
  (path_prod' 1 loop) (path_prod' 1 loop) exact (sq_prod (hr, vr)). (* The square is the obvious product of squares *)
Defined.

(** We now define the curried function from the circles to the torus. *)
(** TODO: It's easy to remove [Funext] from this definition by using [intro] and [revert] appropriately, but then the cube algebra in the proof of [c2t'_beta] would need to be updated. See https://github.com/HoTT/Coq-HoTT/pull/1824. *)
Definition c2t' `{Funext} : Circle -> Circle -> Torus.
H: Funext
Circle -> Circle -> Torus
Proof.
H: Funext
Circle -> Circle -> Torus
  snapply Circle_rec.
H: Funext
Circle -> Torus
H: Funext
?b = ?b
  +
H: Funext
Circle -> Torus snapply Circle_rec.     (* Double circle recursion *)
H: Funext
Torus
H: Funext
?b = ?b
    -
H: Funext
Torus exact tbase.      (* The basepoint is sent to the point of the torus *)
    -
H: Funext
tbase = tbase exact loop_b.     (* The second loop is sent to loop_b *)
  +
H: Funext
Circle_rec Torus tbase loop_b =
Circle_rec Torus tbase loop_b apply path_forall.  (* We use function extensionality here to induct *)
H: Funext
Circle_rec Torus tbase loop_b ==
Circle_rec Torus tbase loop_b
    snapply Circle_ind.  (* Circle induction as a DPath *)
H: Funext
(fun x : Circle =>
 Circle_rec Torus tbase loop_b x =
 Circle_rec Torus tbase loop_b x) base
H: Funext
transport
  (fun x : Circle =>
   Circle_rec Torus tbase loop_b x =
   Circle_rec Torus tbase loop_b x) loop ?b = ?b
    -
H: Funext
(fun x : Circle =>
 Circle_rec Torus tbase loop_b x =
 Circle_rec Torus tbase loop_b x) base exact loop_a.     (* The first loop is sent to loop_a *)
    -
H: Funext
transport
  (fun x : Circle =>
   Circle_rec Torus tbase loop_b x =
   Circle_rec Torus tbase loop_b x) loop loop_a =
loop_a srapply sq_dp^-1. (* This DPath is actually a square *)
H: Funext
PathSquare loop_a loop_a
  (ap (Circle_rec Torus tbase loop_b) loop)
  (ap (Circle_rec Torus tbase loop_b) loop)
      apply (pr1 c2t_square_and_cube). (* We apply the cap we found above *)
Defined.

(** Here is the uncurried version *)
Definition c2t `{Funext} : Circle * Circle -> Torus.
H: Funext
Circle * Circle -> Torus
Proof.
H: Funext
Circle * Circle -> Torus
  apply uncurry, c2t'.
Defined.

(** Computation rules for c2t' as a cube filler *)
Definition c2t'_beta `{Funext} :
  {bl1 : PathSquare (ap (fun y => c2t' base y) loop) loop_b 1 1 &
  {bl2 : PathSquare (ap (fun x => c2t' x base) loop) loop_a 1 1 &
  PathCube (sq_ap011 c2t' loop loop) surf bl2 bl2 bl1 bl1}}.
H: Funext
{bl1
: PathSquare (ap (fun y : Circle => c2t' base y) loop)
    loop_b 1 1 &
{bl2
: PathSquare (ap (fun x : Circle => c2t' x base) loop)
    loop_a 1 1 &
PathCube (sq_ap011 c2t' loop loop) surf bl2 bl2 bl1
  bl1}}
Proof.
H: Funext
{bl1
: PathSquare (ap (fun y : Circle => c2t' base y) loop)
    loop_b 1 1 &
{bl2
: PathSquare (ap (fun x : Circle => c2t' x base) loop)
    loop_a 1 1 &
PathCube (sq_ap011 c2t' loop loop) surf bl2 bl2 bl1
  bl1}}
  nrefine (_;_;_).
H: Funext
PathCube (sq_ap011 c2t' loop loop) surf ?Goal0 ?Goal0
  ?Goal ?Goal
  unfold sq_ap011.
H: Funext
PathCube
  (sq_dp
     (apD
        (fun y : Circle =>
         ap (fun x : Circle => c2t' x y) loop) loop))
  surf ?Goal0 ?Goal0 ?Goal ?Goal
  (* 1. Unfusing ap *)
  nrefine (cu_concat_lr (cu_ds (dp_apD_nat
    (fun y => ap_compose _ (fun f => f y) _) _)) _
    (sji0:=?[X1]) (sji1:=?X1) (sj0i:=?[Y1]) (sj1i:=?Y1) (pj11:=1)).
H: Funext
PathCube
  (sq_dp
     (apD
        (fun y : Circle =>
         ap (fun f : Circle -> Torus => f y)
           (ap c2t' loop)) loop)) surf ?X1 ?X1 ?Y1 
  ?Y1
  (* 2. Reducing c2t' on loop *)
  nrefine (cu_concat_lr (cu_ds (dp_apD_nat
    (fun x => ap_apply_l _ _ @ apD10 (ap _(Circle_rec_beta_loop _ _ _)) x) _)) _
    (sji0:=?[X2]) (sji1:=?X2) (sj0i:=?[Y2]) (sj1i:=?Y2) (pj11:=1)).
H: Funext
PathCube
  (sq_dp
     (apD
        (fun x : Circle =>
         ap10
           (path_forall
              (Circle_rec Torus tbase loop_b)
              (Circle_rec Torus tbase loop_b)
              (Circle_ind
                 (fun x0 : Circle =>
                  Circle_rec Torus tbase loop_b x0 =
                  Circle_rec Torus tbase loop_b x0)
                 loop_a
                 (sq_dp^-1 c2t_square_and_cube.1))) x)
        loop)) surf ?X2 ?X2 ?Y2 ?Y2
  (* 3. Reducing ap10 on function extensionality *)
  nrefine (cu_concat_lr (cu_ds (dp_apD_nat (ap10_path_forall _ _ _) _)) _
    (sji0:=?[X3]) (sji1:=?X3) (sj0i:=?[Y3]) (sj1i:=?Y3) (pj11:=1)).
H: Funext
PathCube
  (sq_dp
     (apD
        (Circle_ind
           (fun x : Circle =>
            Circle_rec Torus tbase loop_b x =
            Circle_rec Torus tbase loop_b x) loop_a
           (sq_dp^-1 c2t_square_and_cube.1)) loop))
  surf ?X3 ?X3 ?Y3 ?Y3
  (* 4. Reducing Circle_ind on loop *)
  nrefine (cu_concat_lr (cu_G11 (ap _ (Circle_ind_beta_loop _ _ _))) _
    (sji0:=?[X4]) (sji1:=?X4) (sj0i:=?[Y4]) (sj1i:=?Y4) (pj11:=1)).
H: Funext
PathCube (sq_dp (sq_dp^-1 c2t_square_and_cube.1)) surf
  ?X4 ?X4 ?Y4 ?Y4
  (* 5. collapsing equivalence *)
  nrefine (cu_concat_lr (cu_G11 (eisretr _ _)) _
    (sji0:=?[X5]) (sji1:=?X5) (sj0i:=?[Y5]) (sj1i:=?Y5) (pj11:=1)).
H: Funext
PathCube c2t_square_and_cube.1 surf ?X5 ?X5 ?Y5 ?Y5
  (* 6. filling the cube *)
  apply c2t_square_and_cube.2.
Defined.

Local Open Scope path_scope.
Local Open Scope cube_scope.

(** We now prove that t2c is a section of c2t *)
Definition t2c2t `{Funext} : c2t o t2c == idmap.
H: Funext
c2t o t2c == idmap
Proof.
H: Funext
c2t o t2c == idmap
  (* We start with Torus induction *)
  nrefine (Torus_ind _ 1 _ _ _).
H: Funext
DPathSquare (fun x : Torus => c2t (t2c x) = x) surf
  ?Goal ?Goal ?Goal0 ?Goal0
  (* Our DPathSquare is really just a cube *)
  apply cu_ds^-1.
H: Funext
PathCube (sq_dp ?Goal) (sq_dp ?Goal) (sq_dp ?Goal0)
  (sq_dp ?Goal0)
  (sq_ap (fun x : Torus => c2t (t2c x)) surf)
  (sq_ap idmap surf)
  (* We pretend that our sides have sq_dpath o sq_dpath^-1
    and get rid of them *)
  refine (cu_GGGGcc (eisretr _ _)^ (eisretr _ _)^
    (eisretr _ _)^ (eisretr _ _)^ _).
H: Funext
PathCube ?Goal ?Goal ?Goal0 ?Goal0
  (sq_ap (fun x : Torus => c2t (t2c x)) surf)
  (sq_ap idmap surf)
  (* Apply a symmetry to get the faces on the right side *)
  apply cu_rot_tb_fb.
H: Funext
PathCube (sq_ap (fun x : Torus => c2t (t2c x)) surf)
  (sq_ap idmap surf) (sq_tr ?Goal) (sq_tr ?Goal)
  (sq_tr ?Goal0) (sq_tr ?Goal0)
  (* Clean up other faces *)
  refine (cu_ccGGGG (eisretr _ _)^ (eisretr _ _)^
    (eisretr _ _)^ (eisretr _ _)^ _).
H: Funext
PathCube (sq_ap (fun x : Torus => c2t (t2c x)) surf)
  (sq_ap idmap surf) ?Goal ?Goal ?Goal0 ?Goal0
  (* Now we finish the proof with the following composition of cubes *)
  exact ((sq_ap_compose t2c c2t surf)
    @lr (cu_ap c2t (Torus_rec_beta_surf _ _ _ _ _ ))
    @lr (sq_ap_uncurry _ _ _)
    @lr (pr2 (pr2 c2t'_beta))
    @lr (cu_flip_lr (sq_ap_idmap _))).
Defined.

(* NOTE: The last step in the previous proof can be done as a sequence of
   refines however Coq really struggles to unify this. Below is the original
   way we proved the last statement before making it short and sweet. As can
   be seen, we need to give refine hints using existential variables which is
   tedious to write out, and perhaps motivates why we wrote it as one big
   concatenation. Ideally the way below should be as smooth as the way above,
   since above is difficult to write directly without having tried below.

  (* Now we decompose the cube with middle sq_ap_compose *)
  (* Note: coq sucks at unifying this so we have to explicitly give paths *)
  refine (cu_concat_lr (sq_ap_compose t2c c2t surf) _
    (sji0:=?[X1]) (sji1:=?X1) (sj0i:=?[Y1]) (sj1i:=?Y1) (pj11:=1)).
  (* Now we reduce (sq_ap t2c surf) *)
  refine (cu_concat_lr (cu_ap c2t (Torus_rec_beta_surf _ _ _ _ _ )) _
    (sji0:=?[X2]) (sji1:=?X2) (sj0i:=?[Y2]) (sj1i:=?Y2) (pj11:=1)).
  (* We now uncurry c2t inside sq_ap *)
  refine (cu_concat_lr (sq_ap_uncurry _ _ _) _
    (sji0:=?[X3]) (sji1:=?X3) (sj0i:=?[Y3]) (sj1i:=?Y3) (pj11:=1)).
  (* Reduce sq_ap2 c2t' loop loop *)
  refine (cu_concat_lr (pr2 (pr2 c2t'_beta)) _
    (sji0:=?[X4]) (sji1:=?X4) (sj0i:=?[Y4]) (sj1i:=?Y4) (pj11:=1)).
  (* Finally flip and sq_ap idmap *)
  refine (cu_flip_lr (sq_ap_idmap _)).

*)

Local Notation apcs := (ap_compose_sq _ _ _).

Definition sq_ap011_compose {A B C D : Type} (f : A -> B -> C) (g : C -> D)
  {a a' : A} (p : a = a') {b b' : B} (q : b = b')
  : PathCube (sq_ap011 (fun x y => g (f x y)) p q) (sq_ap g (sq_ap011 f p q))
      apcs apcs apcs apcs.
A, B, C, D: Type
f: A -> B -> C
g: C -> D
a, a': A
p: a = a'
b, b': B
q: b = b'
PathCube
  (sq_ap011 (fun (x : A) (y : B) => g (f x y)) p q)
  (sq_ap g (sq_ap011 f p q)) apcs apcs apcs apcs
Proof.
A, B, C, D: Type
f: A -> B -> C
g: C -> D
a, a': A
p: a = a'
b, b': B
q: b = b'
PathCube
  (sq_ap011 (fun (x : A) (y : B) => g (f x y)) p q)
  (sq_ap g (sq_ap011 f p q)) apcs apcs apcs apcs
  by destruct p, q.
Defined.

(** We now prove t2c is a retraction of c2t *)
Definition c2t2c `{Funext} : t2c o c2t == idmap.
H: Funext
t2c o c2t == idmap
Proof.
H: Funext
t2c o c2t == idmap
  napply prod_ind.
H: Funext
forall fst snd : Circle,
t2c (c2t (fst, snd)) = (fst, snd)
  (* Start with double circle induction *)
  snrefine (Circle_ind _ (Circle_ind _ 1 _) _).
H: Funext
transport
  (fun x : Circle => t2c (c2t (base, x)) = (base, x))
  loop 1 = 1
H: Funext
transport
  (fun x : Circle =>
   forall snd : Circle, t2c (c2t (x, snd)) = (x, snd))
  loop
  (Circle_ind
     (fun x : Circle =>
      t2c (c2t (base, x)) = (base, x)) 1 ?l) =
Circle_ind
  (fun x : Circle => t2c (c2t (base, x)) = (base, x))
  1 ?l
  (* Change the second loop case into a square and shelve *)
  1: apply sq_dp^-1, sq_tr^-1; shelve.
H: Funext
transport
  (fun x : Circle =>
   forall snd : Circle, t2c (c2t (x, snd)) = (x, snd))
  loop
  (Circle_ind
     (fun x : Circle =>
      t2c (c2t (base, x)) = (base, x)) 1
     (sq_dp^-1 (sq_tr^-1 ?Goal))) =
Circle_ind
  (fun x : Circle => t2c (c2t (base, x)) = (base, x))
  1 (sq_dp^-1 (sq_tr^-1 ?Goal))
  (* Take the forall out of the DPath *)
  apply dp_forall_domain.
H: Funext
forall x : Circle,
DPath (fun t : Circle => t2c (c2t (t, x)) = (t, x))
  loop
  (Circle_ind
     (fun x0 : Circle =>
      t2c (c2t (base, x0)) = (base, x0)) 1
     (sq_dp^-1 (sq_tr^-1 ?Goal)) x)
  (Circle_ind
     (fun x0 : Circle =>
      t2c (c2t (base, x0)) = (base, x0)) 1
     (sq_dp^-1 (sq_tr^-1 ?Goal)) x)
  intro x; apply sq_dp^-1; revert x.
H: Funext
forall x : Circle,
PathSquare
  (Circle_ind
     (fun x0 : Circle =>
      t2c (c2t (base, x0)) = (base, x0)) 1
     (sq_dp^-1 (sq_tr^-1 ?Goal)) x)
  (Circle_ind
     (fun x0 : Circle =>
      t2c (c2t (base, x0)) = (base, x0)) 1
     (sq_dp^-1 (sq_tr^-1 ?Goal)) x)
  (ap (fun x0 : Circle => t2c (c2t (x0, x))) loop)
  (ap (fun x0 : Circle => (x0, x)) loop)
  snrefine (Circle_ind _ _ _).
H: Funext
(fun x : Circle =>
 PathSquare
   (Circle_ind
      (fun x0 : Circle =>
       t2c (c2t (base, x0)) = (base, x0)) 1
      (sq_dp^-1 (sq_tr^-1 ?Goal)) x)
   (Circle_ind
      (fun x0 : Circle =>
       t2c (c2t (base, x0)) = (base, x0)) 1
      (sq_dp^-1 (sq_tr^-1 ?Goal)) x)
   (ap (fun x0 : Circle => t2c (c2t (x0, x))) loop)
   (ap (fun x0 : Circle => (x0, x)) loop)) base
H: Funext
transport
  (fun x : Circle =>
   PathSquare
     (Circle_ind
        (fun x0 : Circle =>
         t2c (c2t (base, x0)) = (base, x0)) 1
        (sq_dp^-1 (sq_tr^-1 ?Goal)) x)
     (Circle_ind
        (fun x0 : Circle =>
         t2c (c2t (base, x0)) = (base, x0)) 1
        (sq_dp^-1 (sq_tr^-1 ?Goal)) x)
     (ap (fun x0 : Circle => t2c (c2t (x0, x))) loop)
     (ap (fun x0 : Circle => (x0, x)) loop)) loop 
  ?b = ?b
  1: apply sq_tr^-1; shelve.
H: Funext
transport
  (fun x : Circle =>
   PathSquare
     (Circle_ind
        (fun x0 : Circle =>
         t2c (c2t (base, x0)) = (base, x0)) 1
        (sq_dp^-1 (sq_tr^-1 ?Goal)) x)
     (Circle_ind
        (fun x0 : Circle =>
         t2c (c2t (base, x0)) = (base, x0)) 1
        (sq_dp^-1 (sq_tr^-1 ?Goal)) x)
     (ap (fun x0 : Circle => t2c (c2t (x0, x))) loop)
     (ap (fun x0 : Circle => (x0, x)) loop)) loop
  (sq_tr^-1 ?Goal0) = sq_tr^-1 ?Goal0
  apply dp_cu.
H: Funext
PathCube (sq_tr^-1 ?Goal0) (sq_tr^-1 ?Goal0)
  (sq_dp
     (apD
        (Circle_ind
           (fun x : Circle =>
            t2c (c2t (base, x)) = (base, x)) 1
           (sq_dp^-1 (sq_tr^-1 ?Goal))) loop))
  (sq_dp
     (apD
        (Circle_ind
           (fun x : Circle =>
            t2c (c2t (base, x)) = (base, x)) 1
           (sq_dp^-1 (sq_tr^-1 ?Goal))) loop))
  (sq_dp
     (apD
        (fun x : Circle =>
         ap (fun x0 : Circle => t2c (c2t (x0, x)))
           loop) loop))
  (sq_dp
     (apD
        (fun x : Circle =>
         ap (fun x0 : Circle => (x0, x)) loop) loop))
  nrefine (cu_ccGGcc _ _ _).
H: Funext
?Goal1 =
sq_dp
  (apD
     (Circle_ind
        (fun x : Circle =>
         t2c (c2t (base, x)) = (base, x)) 1
        (sq_dp^-1 (sq_tr^-1 ?Goal))) loop)
H: Funext
?Goal2 =
sq_dp
  (apD
     (Circle_ind
        (fun x : Circle =>
         t2c (c2t (base, x)) = (base, x)) 1
        (sq_dp^-1 (sq_tr^-1 ?Goal))) loop)
H: Funext
PathCube (sq_tr^-1 ?Goal0) (sq_tr^-1 ?Goal0) ?Goal1
  ?Goal2
  (sq_dp
     (apD
        (fun x : Circle =>
         ap (fun x0 : Circle => t2c (c2t (x0, x)))
           loop) loop))
  (sq_dp
     (apD
        (fun x : Circle =>
         ap (fun x0 : Circle => (x0, x)) loop) loop))
  1,2: exact (ap sq_dp (Circle_ind_beta_loop _ _ _)
    @ eisretr _ _)^.
H: Funext
PathCube (sq_tr^-1 ?Goal0) (sq_tr^-1 ?Goal0)
  (sq_tr^-1 ?Goal) (sq_tr^-1 ?Goal)
  (sq_dp
     (apD
        (fun x : Circle =>
         ap (fun x0 : Circle => t2c (c2t (x0, x)))
           loop) loop))
  (sq_dp
     (apD
        (fun x : Circle =>
         ap (fun x0 : Circle => (x0, x)) loop) loop))
  apply cu_rot_tb_fb.
H: Funext
PathCube
  (sq_dp
     (apD
        (fun x : Circle =>
         ap (fun x0 : Circle => t2c (c2t (x0, x)))
           loop) loop))
  (sq_dp
     (apD
        (fun x : Circle =>
         ap (fun x0 : Circle => (x0, x)) loop) loop))
  (sq_tr (sq_tr^-1 ?Goal0)) (sq_tr (sq_tr^-1 ?Goal0))
  (sq_tr (sq_tr^-1 ?Goal)) (sq_tr (sq_tr^-1 ?Goal))
  nrefine (cu_ccGGGG _ _ _ _ _).
H: Funext
?Goal1 = sq_tr (sq_tr^-1 ?Goal0)
H: Funext
?Goal2 = sq_tr (sq_tr^-1 ?Goal0)
H: Funext
?Goal3 = sq_tr (sq_tr^-1 ?Goal)
H: Funext
?Goal4 = sq_tr (sq_tr^-1 ?Goal)
H: Funext
PathCube
  (sq_dp
     (apD
        (fun x : Circle =>
         ap (fun x0 : Circle => t2c (c2t (x0, x)))
           loop) loop))
  (sq_dp
     (apD
        (fun x : Circle =>
         ap (fun x0 : Circle => (x0, x)) loop) loop))
  ?Goal1 ?Goal2 ?Goal3 ?Goal4
  1,2,3,4: exact (eisretr _ _)^.
H: Funext
PathCube
  (sq_dp
     (apD
        (fun x : Circle =>
         ap (fun x0 : Circle => t2c (c2t (x0, x)))
           loop) loop))
  (sq_dp
     (apD
        (fun x : Circle =>
         ap (fun x0 : Circle => (x0, x)) loop) loop))
  ?Goal0 ?Goal0 ?Goal ?Goal
  exact ((sq_ap011_compose c2t' t2c loop loop)
    @lr (cu_ap t2c (c2t'_beta.2.2))
    @lr (Torus_rec_beta_surf _ _ _ _ _)
    @lr (cu_flip_lr (sq_ap_idmap _))
    @lr (sq_ap_uncurry _ _ _)).
Defined.

(* refine (cu_concat_lr (sq_ap2_compose c2t' t2c loop loop) _
    (sji0:=?[X1]) (sji1:=?X1) (sj0i:=?[Y1]) (sj1i:=?Y1) (pj11:=1)).
  refine (cu_concat_lr (cu_ap t2c (c2t'_beta.2.2)) _
    (sji0:=?[X2]) (sji1:=?X2) (sj0i:=?[Y2]) (sj1i:=?Y2) (pj11:=1)).
  refine (cu_concat_lr (Torus_rec_beta_surf _ _ _ _ _) _
    (sji0:=?[X3]) (sji1:=?X3) (sj0i:=?[Y3]) (sj1i:=?Y3) (pj11:=1)).
  refine (cu_concat_lr (cu_flip_lr (sq_ap_idmap _)) _
    (sji0:=?[X4]) (sji1:=?X4) (sj0i:=?[Y4]) (sj1i:=?Y4) (pj11:=1)).
  apply sq_ap_uncurry. *)

Definition equiv_torus_prod_Circle `{Funext} : Torus <~> Circle * Circle
  := equiv_adjointify t2c c2t c2t2c t2c2t.