Merge pull request #2312 from jdchristensen/add-From-HoTT

Add "From HoTT" before many "Require" commands

Author: jdchristensen

theories/Algebra/AbGroups/AbHom.v

@@ -1,4 +1,4 @@
-Require Import Basics Types.
+From HoTT Require Import Basics Types.
 Require Import WildCat HSet Truncations.Core Modalities.ReflectiveSubuniverse.
 Require Import Groups.Group Groups.QuotientGroup AbelianGroup Biproduct.
 

theories/Algebra/AbGroups/AbProjective.v

@@ -1,4 +1,4 @@
-Require Import Basics Types AbelianGroup AbPullback
+From HoTT Require Import Basics Types AbelianGroup AbPullback
   WildCat.Core Limits.Pullback ReflectiveSubuniverse Truncations.Core.
 
 (** * Projective abelian groups *)

theories/Algebra/AbGroups/AbPullback.v

@@ -1,4 +1,4 @@
-Require Import Basics.
+From HoTT Require Import Basics.
 Require Import Limits.Pullback Cubical.PathSquare.
 Require Export Algebra.Groups.GrpPullback.
 Require Import Algebra.AbGroups.AbelianGroup.

theories/Algebra/AbGroups/AbPushout.v

@@ -1,4 +1,4 @@
-Require Import Basics Types Truncations.Core.
+From HoTT Require Import Basics Types Truncations.Core.
 Require Import WildCat.Core HSet.
 Require Import Algebra.Groups.Group.
 Require Export Algebra.Groups.QuotientGroup.

theories/Algebra/AbGroups/AbelianGroup.v

@@ -1,4 +1,4 @@
-Require Import Basics Types.
+From HoTT Require Import Basics Types.
 Require Import Spaces.Nat.Core Spaces.Int.
 Require Export Classes.interfaces.canonical_names (Zero, zero, Plus, plus, Negate, negate, Involutive, involutive).
 Require Export Classes.interfaces.abstract_algebra (IsAbGroup(..), abgroup_group, abgroup_commutative).

theories/Algebra/AbGroups/Abelianization.v

@@ -1,4 +1,4 @@
-Require Import Basics Types Truncations.Core.
+From HoTT Require Import Basics Types Truncations.Core.
 Require Import Cubical.DPath WildCat.
 Require Import Colimits.Coeq.
 Require Import Algebra.AbGroups.AbelianGroup.

theories/Algebra/AbGroups/Biproduct.v

@@ -1,4 +1,4 @@
-Require Import Basics Types Truncations.Core.
+From HoTT Require Import Basics Types Truncations.Core.
 Require Import WildCat.
 Require Import HSet.
 Require Import AbelianGroup.

theories/Algebra/AbGroups/Centralizer.v

@@ -1,4 +1,4 @@
-Require Import Basics Types Truncations.Core.
+From HoTT Require Import Basics Types Truncations.Core.
 Require Import HFiber AbelianGroup.
 
 (* Given a group [G], we define the centralizer of an element [g : G] as a subgroup and use this to show that the cyclic subgroup generated by [g] is abelian. *)

theories/Algebra/AbGroups/Z.v

@@ -1,4 +1,4 @@
-Require Import Basics.
+From HoTT Require Import Basics.
 Require Import Spaces.Pos.Core Spaces.Int.
 Require Import Algebra.AbGroups.AbelianGroup.
 

theories/Algebra/AbSES/BaerSum.v

@@ -1,4 +1,4 @@
-Require Import Basics Types.
+From HoTT Require Import Basics Types.
 Require Import WildCat Pointed.Core.
 Require Import AbGroups.AbelianGroup AbGroups.Biproduct AbGroups.AbHom.
 Require Import AbSES.Core AbSES.Pullback AbSES.Pushout AbSES.DirectSum.