(n : nat) (X : pType) : HomotopyGroup_type n. Proof. destruct n. 1: exact (pTr 0 X). exact (Pi1 (iterated_loops n X)). Defined.
Require Import Basics Types Pointed HSet. Require Import Modalities.Modality. Require Import Truncations.Core Truncations.SeparatedTrunc. Require Import Algebra.AbGroups. Require Import WildCat.