Require Import Pointed WildCat. Require Import Modalities.ReflectiveSubuniverse Truncations.Core. Require Import Algebra.AbGroups. Require Import Homotopy.HomotopyGroup. Require Import Homotopy.PinSn. Require Import Spaces.Int.Core 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 *)H: UnivalenceIsTrunc 1 Torusrefine (istrunc_equiv_istrunc _ equiv_torus_prod_Circle^-1). Qed. (** The torus is 0-connected *)H: UnivalenceIsTrunc 1 TorusH: UnivalenceIsConnected (Tr 0) TorusH: UnivalenceIsConnected (Tr 0) Torussrapply (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. *)H: UnivalenceIsConnected (Tr 0) (Circle * Circle)H: FunextT <~>* S1 * S1H: FunextT <~>* S1 * S1H: FunextT <~> [S1 * S1, ispointed_prod]H: Funext?f pt = ptreflexivity. Defined. (** Fundamental group of torus *)H: Funextequiv_torus_prod_Circle pt = ptH: UnivalenceGroupIsomorphism (Pi 1 T) (grp_prod abgroup_Z abgroup_Z)H: UnivalenceGroupIsomorphism (Pi 1 T) (grp_prod abgroup_Z abgroup_Z)H: UnivalenceGroupIsomorphism (Pi 1 T) ?GoalH: UnivalenceGroupIsomorphism ?Goal (grp_prod abgroup_Z abgroup_Z)H: UnivalenceGroupIsomorphism (Pi 1 (S1 * S1)) (grp_prod abgroup_Z abgroup_Z)H: UnivalenceGroupIsomorphism (Pi 1 (S1 * S1)) ?GoalH: UnivalenceGroupIsomorphism ?Goal (grp_prod abgroup_Z abgroup_Z)H: UnivalenceGroupIsomorphism (grp_prod (Pi 1 S1) (Pi 1 S1)) (grp_prod abgroup_Z abgroup_Z)1,2: apply pi1_circle. Defined. (** Loop space of torus *)H: UnivalencePi 1 S1 $<~> abgroup_ZH: UnivalencePi 1 S1 $<~> abgroup_ZH: Univalenceloops T <~>* Int * Int(* Since [T] is 1-truncated, [loops T] is 0-truncated, and is therefore equivalent to its 0-truncation. *)H: Univalenceloops T <~>* Int * Intnrapply pi1_torus. Defined.H: UnivalencepTr 0 (loops T) <~>* Int * Int