From HoTT Require Import Basics Types.From HoTT Require Import Basics Types.
From HoTT.WildCat Require Import Core Equiv.
Require Import Pointed.
Require Import Modalities.ReflectiveSubuniverse Truncations.Core.
From HoTT.Algebra.AbGroups Require Import AbelianGroup Z.
Require Import Homotopy.HomotopyGroup.
Require Import Homotopy.PinSn.
Require Import Spaces.Int Spaces.Circle.

Require Import Spaces.Torus.Torus.
Require Import Spaces.Torus.TorusEquivCircles.

Local Open Scope trunc_scope.
Local Open Scope pointed_scope.

(** ** Fundamental group of the torus .*)

(** The torus is 1-truncated *)

Instance is1type_torus `{Univalence} : IsTrunc 1 Torus.
H: Univalence
IsTrunc 1 Torus
Proof.
H: Univalence
IsTrunc 1 Torus
  exact (istrunc_equiv_istrunc _ equiv_torus_prod_Circle^-1).
Qed.

(** The torus is 0-connected *)

Instance isconnected_torus `{Univalence} : IsConnected 0 Torus.
H: Univalence
IsConnected (Tr 0) Torus
Proof.
H: Univalence
IsConnected (Tr 0) Torus
  srapply (isconnected_equiv' _ _ equiv_torus_prod_Circle^-1).
H: Univalence
IsConnected (Tr 0) (Circle * Circle)
  srapply (isconnected_equiv' _ _ (equiv_sigma_prod0 _ _)).
Qed.

(** We give these notations for the pointed versions. *)
Local Notation T := ([Torus, _]).
Local Notation S1 := ([Circle, _]).

(** A pointed version of the equivalence from TorusEquivCircles.v. *)
(** TODO: If [Funext] is removed from there, remove it from here as well. *)
Lemma pequiv_torus_prod_circles `{Funext} : T  <~>* S1 * S1.
H: Funext
T <~>* S1 * S1
Proof.
H: Funext
T <~>* S1 * S1
  srapply Build_pEquiv'.
H: Funext
T <~> [S1 * S1, ispointed_prod]
H: Funext
?f pt = pt
  1: exact equiv_torus_prod_Circle.
H: Funext
equiv_torus_prod_Circle pt = pt
  reflexivity.
Defined.

(** Fundamental group of torus *)
Theorem pi1_torus `{Univalence}
  : GroupIsomorphism (Pi 1 T) (grp_prod abgroup_Z abgroup_Z).
H: Univalence
GroupIsomorphism (Pi 1 T) (grp_prod abgroup_Z abgroup_Z)
Proof.
H: Univalence
GroupIsomorphism (Pi 1 T) (grp_prod abgroup_Z abgroup_Z)
  etransitivity.
H: Univalence
GroupIsomorphism (Pi 1 T) ?Goal
H: Univalence
GroupIsomorphism ?Goal (grp_prod abgroup_Z abgroup_Z)
  1: exact (emap (Pi 1) pequiv_torus_prod_circles).
H: Univalence
GroupIsomorphism (Pi 1 (S1 * S1)) (grp_prod abgroup_Z abgroup_Z)
  etransitivity.
H: Univalence
GroupIsomorphism (Pi 1 (S1 * S1)) ?Goal
H: Univalence
GroupIsomorphism ?Goal (grp_prod abgroup_Z abgroup_Z)
  1: apply grp_iso_pi_prod.
H: Univalence
GroupIsomorphism (grp_prod (Pi 1 S1) (Pi 1 S1))
  (grp_prod abgroup_Z abgroup_Z)
  apply grp_iso_prod.
H: Univalence
Pi 1 S1 $<~> abgroup_Z
H: Univalence
Pi 1 S1 $<~> abgroup_Z
  1,2: exact pi1_circle.
Defined.

(** Loop space of torus *)
Theorem loops_torus `{Univalence} : loops T <~>* Int * Int.
H: Univalence
loops T <~>* Int * Int
Proof.
H: Univalence
loops T <~>* Int * Int
  (* Since [T] is 1-truncated, [loops T] is 0-truncated, and is therefore equivalent to its 0-truncation. *)
  refine (_ o*E pequiv_ptr (n:=0)).
H: Univalence
pTr 0 (loops T) <~>* Int * Int
  exact pi1_torus.
Defined.