Require Export Basics.PathGroupoids. Require Export Basics.Contractible. Require Export Basics.Equivalences. Require Export Basics.Trunc. Require Export Basics.Decidable. Require Export Basics.Utf8. Require Export Basics.Notations. Require Export Basics.Tactics. Require Export Basics.Nat. Require Export Basics.Numeral.