Abelianization (#877)

src/category-theory/full-large-subcategories.lagda.md

@@ -8,6 +8,7 @@ module category-theory.full-large-subcategories where
 
 ```agda
 open import category-theory.full-large-subprecategories
+open import category-theory.functors-large-categories
 open import category-theory.large-categories
 open import category-theory.large-precategories
 
@@ -203,3 +204,23 @@ module _
     large-category-Full-Large-Subcategory =
     is-large-category-Full-Large-Subcategory
 ```
+
+### The forgetful functor from a full large subcategory to the ambient large category
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level} {γ : Level → Level}
+  (C : Large-Category α β)
+  (P : Full-Large-Subcategory γ C)
+  where
+
+  forgetful-functor-Full-Large-Subcategory :
+    functor-Large-Category
+      ( λ l → l)
+      ( large-category-Full-Large-Subcategory C P)
+      ( C)
+  forgetful-functor-Full-Large-Subcategory =
+    forgetful-functor-Full-Large-Subprecategory
+      ( large-precategory-Large-Category C)
+      ( P)
+```

src/category-theory/full-large-subprecategories.lagda.md

@@ -7,11 +7,13 @@ module category-theory.full-large-subprecategories where
 <details><summary>Imports</summary>
 
 ```agda
+open import category-theory.functors-large-precategories
 open import category-theory.isomorphisms-in-large-categories
 open import category-theory.isomorphisms-in-large-precategories
 open import category-theory.large-categories
 open import category-theory.large-precategories
 
+open import foundation.function-types
 open import foundation.fundamental-theorem-of-identity-types
 open import foundation.identity-types
 open import foundation.propositions
@@ -190,6 +192,34 @@ module _
     iso-eq-Large-Precategory large-precategory-Full-Large-Subprecategory
 ```
 
+### The forgetful functor from a full large subprecategory to the ambient large precategory
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level} {γ : Level → Level}
+  (C : Large-Precategory α β)
+  (P : Full-Large-Subprecategory γ C)
+  where
+
+  forgetful-functor-Full-Large-Subprecategory :
+    functor-Large-Precategory
+      ( λ l → l)
+      ( large-precategory-Full-Large-Subprecategory C P)
+      ( C)
+  obj-functor-Large-Precategory
+    forgetful-functor-Full-Large-Subprecategory =
+    inclusion-subtype P
+  hom-functor-Large-Precategory
+    forgetful-functor-Full-Large-Subprecategory =
+    id
+  preserves-comp-functor-Large-Precategory
+    forgetful-functor-Full-Large-Subprecategory g f =
+    refl
+  preserves-id-functor-Large-Precategory
+    forgetful-functor-Full-Large-Subprecategory =
+    refl
+```
+
 ## Properties
 
 ### A full large subprecategory of a large category is a large category

src/category-theory/representable-functors-large-precategories.lagda.md

@@ -55,7 +55,7 @@ module _
     {l2 l3 : Level}
     {X : obj-Large-Precategory C l2} {Y : obj-Large-Precategory C l3} →
     hom-Large-Precategory C X Y →
-    type-hom-Set
+    hom-Set
       ( obj-representable-functor-Large-Precategory X)
       ( obj-representable-functor-Large-Precategory Y)
   hom-representable-functor-Large-Precategory =

src/commutative-algebra/full-ideals-commutative-rings.lagda.md

@@ -79,14 +79,14 @@ module _
   is-closed-under-addition-full-ideal-Commutative-Ring :
     is-closed-under-addition-subset-Commutative-Ring A
       subset-full-ideal-Commutative-Ring
-  is-closed-under-addition-full-ideal-Commutative-Ring =
-    is-closed-under-addition-full-ideal-Ring (ring-Commutative-Ring A)
+  is-closed-under-addition-full-ideal-Commutative-Ring {x} {y} =
+    is-closed-under-addition-full-ideal-Ring (ring-Commutative-Ring A) {x} {y}
 
   is-closed-under-negatives-full-ideal-Commutative-Ring :
     is-closed-under-negatives-subset-Commutative-Ring A
       subset-full-ideal-Commutative-Ring
-  is-closed-under-negatives-full-ideal-Commutative-Ring =
-    is-closed-under-negatives-full-ideal-Ring (ring-Commutative-Ring A)
+  is-closed-under-negatives-full-ideal-Commutative-Ring {x} =
+    is-closed-under-negatives-full-ideal-Ring (ring-Commutative-Ring A) {x}
 
   is-additive-subgroup-full-ideal-Commutative-Ring :
     is-additive-subgroup-subset-Commutative-Ring A

src/commutative-algebra/groups-of-units-commutative-rings.lagda.md

@@ -182,15 +182,17 @@ module _
     inclusion-group-of-units-Ring (ring-Commutative-Ring A)
 
   preserves-mul-inclusion-group-of-units-Commutative-Ring :
-    (x y : type-group-of-units-Commutative-Ring) →
+    {x y : type-group-of-units-Commutative-Ring} →
     inclusion-group-of-units-Commutative-Ring
       ( mul-group-of-units-Commutative-Ring x y) ＝
     mul-Commutative-Ring A
       ( inclusion-group-of-units-Commutative-Ring x)
       ( inclusion-group-of-units-Commutative-Ring y)
-  preserves-mul-inclusion-group-of-units-Commutative-Ring =
+  preserves-mul-inclusion-group-of-units-Commutative-Ring {x} {y} =
     preserves-mul-inclusion-group-of-units-Ring
       ( ring-Commutative-Ring A)
+      { x}
+      { y}
 
   hom-inclusion-group-of-units-Commutative-Ring :
     hom-Monoid monoid-group-of-units-Commutative-Ring
@@ -221,7 +223,7 @@ module _
       ( f)
 
   preserves-mul-hom-group-of-units-hom-Commutative-Ring :
-    (x y : type-group-of-units-Commutative-Ring A) →
+    {x y : type-group-of-units-Commutative-Ring A} →
     map-group-of-units-hom-Commutative-Ring
       ( mul-group-of-units-Commutative-Ring A x y) ＝
     mul-group-of-units-Commutative-Ring B
@@ -254,7 +256,7 @@ module _
       ( f)
 
   preserves-inv-hom-group-of-units-hom-Commutative-Ring :
-    (x : type-group-of-units-Commutative-Ring A) →
+    {x : type-group-of-units-Commutative-Ring A} →
     map-group-of-units-hom-Commutative-Ring
       ( inv-group-of-units-Commutative-Ring A x) ＝
     inv-group-of-units-Commutative-Ring B

src/commutative-algebra/homomorphisms-commutative-semirings.lagda.md

@@ -78,7 +78,7 @@ module _
         ( f)
 
     preserves-addition-hom-Commutative-Semiring :
-      (x y : type-Commutative-Semiring A) →
+      {x y : type-Commutative-Semiring A} →
       map-hom-Commutative-Semiring (add-Commutative-Semiring A x y) ＝
       add-Commutative-Semiring B
         ( map-hom-Commutative-Semiring x)
@@ -99,7 +99,7 @@ module _
         ( f)
 
     preserves-mul-hom-Commutative-Semiring :
-      (x y : type-Commutative-Semiring A) →
+      {x y : type-Commutative-Semiring A} →
       map-hom-Commutative-Semiring (mul-Commutative-Semiring A x y) ＝
       mul-Commutative-Semiring B
         ( map-hom-Commutative-Semiring x)
@@ -157,7 +157,7 @@ module _
       ( semiring-Commutative-Semiring A)
 
   preserves-mul-id-hom-Commutative-Semiring :
-    (x y : type-Commutative-Semiring A) →
+    {x y : type-Commutative-Semiring A} →
     mul-Commutative-Semiring A x y ＝ mul-Commutative-Semiring A x y
   preserves-mul-id-hom-Commutative-Semiring =
     preserves-mul-id-hom-Semiring (semiring-Commutative-Semiring A)
@@ -219,7 +219,7 @@ module _
       ( f)
 
   preserves-mul-comp-hom-Commutative-Semiring :
-    (x y : type-Commutative-Semiring A) →
+    {x y : type-Commutative-Semiring A} →
     map-comp-hom-Commutative-Semiring (mul-Commutative-Semiring A x y) ＝
     mul-Commutative-Semiring C
       ( map-comp-hom-Commutative-Semiring x)

src/commutative-algebra/ideals-commutative-rings.lagda.md

@@ -140,7 +140,7 @@ module _
     is-in-ideal-Commutative-Ring x →
     is-in-ideal-Commutative-Ring (neg-Commutative-Ring R x)
   is-closed-under-negatives-ideal-Commutative-Ring =
-    pr2 (pr2 is-additive-subgroup-ideal-Commutative-Ring) _
+    pr2 (pr2 is-additive-subgroup-ideal-Commutative-Ring)
 
   is-closed-under-left-multiplication-ideal-Commutative-Ring :
     is-closed-under-left-multiplication-subset-Commutative-Ring R

src/commutative-algebra/intersections-ideals-commutative-rings.lagda.md

@@ -81,25 +81,25 @@ module _
     is-closed-under-addition-subset-Commutative-Ring R
       ( subset-intersection-ideal-Commutative-Ring)
   pr1
-    ( is-closed-under-addition-intersection-ideal-Commutative-Ring x y
+    ( is-closed-under-addition-intersection-ideal-Commutative-Ring
       ( H1 , H2)
       ( K1 , K2)) =
-    is-closed-under-addition-ideal-Commutative-Ring R I x y H1 K1
+    is-closed-under-addition-ideal-Commutative-Ring R I H1 K1
   pr2
-    ( is-closed-under-addition-intersection-ideal-Commutative-Ring x y
+    ( is-closed-under-addition-intersection-ideal-Commutative-Ring
       ( H1 , H2)
       ( K1 , K2)) =
-    is-closed-under-addition-ideal-Commutative-Ring R J x y H2 K2
+    is-closed-under-addition-ideal-Commutative-Ring R J H2 K2
 
   is-closed-under-negatives-intersection-ideal-Commutative-Ring :
     is-closed-under-negatives-subset-Commutative-Ring R
       ( subset-intersection-ideal-Commutative-Ring)
   pr1
-    ( is-closed-under-negatives-intersection-ideal-Commutative-Ring x
+    ( is-closed-under-negatives-intersection-ideal-Commutative-Ring
       ( H1 , H2)) =
     is-closed-under-negatives-ideal-Commutative-Ring R I H1
   pr2
-    ( is-closed-under-negatives-intersection-ideal-Commutative-Ring x
+    ( is-closed-under-negatives-intersection-ideal-Commutative-Ring
       ( H1 , H2)) =
     is-closed-under-negatives-ideal-Commutative-Ring R J H2
 

src/commutative-algebra/isomorphisms-commutative-rings.lagda.md

@@ -172,7 +172,7 @@ module _
       ( ring-Commutative-Ring B)
 
   preserves-add-iso-Commutative-Ring :
-    (f : iso-Commutative-Ring) (x y : type-Commutative-Ring A) →
+    (f : iso-Commutative-Ring) {x y : type-Commutative-Ring A} →
     map-iso-Commutative-Ring f (add-Commutative-Ring A x y) ＝
     add-Commutative-Ring B
       ( map-iso-Commutative-Ring f x)
@@ -183,7 +183,7 @@ module _
       ( ring-Commutative-Ring B)
 
   preserves-neg-iso-Commutative-Ring :
-    (f : iso-Commutative-Ring) (x : type-Commutative-Ring A) →
+    (f : iso-Commutative-Ring) {x : type-Commutative-Ring A} →
     map-iso-Commutative-Ring f (neg-Commutative-Ring A x) ＝
     neg-Commutative-Ring B (map-iso-Commutative-Ring f x)
   preserves-neg-iso-Commutative-Ring =
@@ -192,7 +192,7 @@ module _
       ( ring-Commutative-Ring B)
 
   preserves-mul-iso-Commutative-Ring :
-    (f : iso-Commutative-Ring) (x y : type-Commutative-Ring A) →
+    (f : iso-Commutative-Ring) {x y : type-Commutative-Ring A} →
     map-iso-Commutative-Ring f (mul-Commutative-Ring A x y) ＝
     mul-Commutative-Ring B
       ( map-iso-Commutative-Ring f x)
@@ -243,7 +243,7 @@ module _
       ( ring-Commutative-Ring B)
 
   preserves-add-inv-iso-Commutative-Ring :
-    (f : iso-Commutative-Ring) (x y : type-Commutative-Ring B) →
+    (f : iso-Commutative-Ring) {x y : type-Commutative-Ring B} →
     map-inv-iso-Commutative-Ring f (add-Commutative-Ring B x y) ＝
     add-Commutative-Ring A
       ( map-inv-iso-Commutative-Ring f x)
@@ -254,7 +254,7 @@ module _
       ( ring-Commutative-Ring B)
 
   preserves-neg-inv-iso-Commutative-Ring :
-    (f : iso-Commutative-Ring) (x : type-Commutative-Ring B) →
+    (f : iso-Commutative-Ring) {x : type-Commutative-Ring B} →
     map-inv-iso-Commutative-Ring f (neg-Commutative-Ring B x) ＝
     neg-Commutative-Ring A (map-inv-iso-Commutative-Ring f x)
   preserves-neg-inv-iso-Commutative-Ring =
@@ -263,7 +263,7 @@ module _
       ( ring-Commutative-Ring B)
 
   preserves-mul-inv-iso-Commutative-Ring :
-    (f : iso-Commutative-Ring) (x y : type-Commutative-Ring B) →
+    (f : iso-Commutative-Ring) {x y : type-Commutative-Ring B} →
     map-inv-iso-Commutative-Ring f (mul-Commutative-Ring B x y) ＝
     mul-Commutative-Ring A
       ( map-inv-iso-Commutative-Ring f x)

src/commutative-algebra/nilradical-commutative-rings.lagda.md

@@ -59,7 +59,7 @@ is-closed-under-addition-nilradical-Commutative-Ring :
   {l : Level} (A : Commutative-Ring l) →
   is-closed-under-addition-subset-Commutative-Ring A
     ( subset-nilradical-Commutative-Ring A)
-is-closed-under-addition-nilradical-Commutative-Ring A x y =
+is-closed-under-addition-nilradical-Commutative-Ring A {x} {y} =
   is-nilpotent-add-Ring
     ( ring-Commutative-Ring A)
     ( x)

src/commutative-algebra/poset-of-radical-ideals-commutative-rings.lagda.md

@@ -180,7 +180,7 @@ module _
   preserves-order-ideal-radical-ideal-Commutative-Ring I J H = H
 
   ideal-radical-ideal-hom-large-poset-Commutative-Ring :
-    hom-set-Large-Poset
+    hom-Large-Poset
       ( λ l → l)
       ( radical-ideal-Commutative-Ring-Large-Poset A)
       ( ideal-Commutative-Ring-Large-Poset A)

src/commutative-algebra/products-ideals-commutative-rings.lagda.md

@@ -227,8 +227,6 @@ module _
       ( product-subset-Commutative-Ring A S T)
       ( is-closed-under-addition-ideal-subset-Commutative-Ring A
         ( product-subset-Commutative-Ring A S T)
-        ( _)
-        ( _)
         ( is-closed-under-eq-ideal-subset-Commutative-Ring' A
           ( product-subset-Commutative-Ring A S T)
           ( is-closed-under-right-multiplication-ideal-Commutative-Ring A
@@ -276,8 +274,6 @@ module _
       ( product-subset-Commutative-Ring A S T)
       ( is-closed-under-addition-ideal-subset-Commutative-Ring A
         ( product-subset-Commutative-Ring A S T)
-        ( _)
-        ( _)
         ( is-closed-under-eq-ideal-subset-Commutative-Ring' A
           ( product-subset-Commutative-Ring A S T)
           ( is-closed-under-right-multiplication-ideal-Commutative-Ring A
@@ -329,14 +325,8 @@ module _
       ( product-subset-Commutative-Ring A S T)
       ( is-closed-under-addition-ideal-subset-Commutative-Ring A
         ( product-subset-Commutative-Ring A S T)
-        ( add-Commutative-Ring A _ _)
-        ( add-Commutative-Ring A _ _)
         ( is-closed-under-addition-ideal-subset-Commutative-Ring A
           ( product-subset-Commutative-Ring A S T)
-          ( mul-Commutative-Ring A _ _)
-          ( mul-Commutative-Ring A
-            ( mul-Commutative-Ring A _ _)
-            ( ev-formal-combination-subset-Commutative-Ring A T l))
           ( is-closed-under-eq-ideal-subset-Commutative-Ring' A
             ( product-subset-Commutative-Ring A S T)
             ( is-closed-under-right-multiplication-ideal-Commutative-Ring A
@@ -361,8 +351,6 @@ module _
             Hs l))
         ( is-closed-under-addition-ideal-subset-Commutative-Ring A
           ( product-subset-Commutative-Ring A S T)
-          ( _)
-          ( _)
           ( right-backward-inclusion-preserves-product-ideal-subset-Commutative-Ring
             Ht k)
           ( backward-inclusion-preserves-product-ideal-subset-Commutative-Ring'

src/commutative-algebra/radicals-of-ideals-commutative-rings.lagda.md

@@ -106,7 +106,7 @@ module _
   is-closed-under-addition-radical-of-ideal-Commutative-Ring :
     is-closed-under-addition-subset-Commutative-Ring A
       ( subset-radical-of-ideal-Commutative-Ring)
-  is-closed-under-addition-radical-of-ideal-Commutative-Ring x y H K =
+  is-closed-under-addition-radical-of-ideal-Commutative-Ring {x} {y} H K =
     apply-universal-property-trunc-Prop H
       ( subset-radical-of-ideal-Commutative-Ring (add-Commutative-Ring A x y))
       ( λ (n , p) →
@@ -117,7 +117,7 @@ module _
             intro-∃
               ( n +ℕ m)
               ( is-closed-under-eq-ideal-Commutative-Ring' A I
-                ( is-closed-under-addition-ideal-Commutative-Ring A I _ _
+                ( is-closed-under-addition-ideal-Commutative-Ring A I
                   ( is-closed-under-right-multiplication-ideal-Commutative-Ring
                     ( A)
                     ( I)
@@ -135,7 +135,7 @@ module _
   is-closed-under-negatives-radical-of-ideal-Commutative-Ring :
     is-closed-under-negatives-subset-Commutative-Ring A
       ( subset-radical-of-ideal-Commutative-Ring)
-  is-closed-under-negatives-radical-of-ideal-Commutative-Ring x H =
+  is-closed-under-negatives-radical-of-ideal-Commutative-Ring {x} H =
     apply-universal-property-trunc-Prop H
       ( subset-radical-of-ideal-Commutative-Ring (neg-Commutative-Ring A x))
       ( λ (n , p) →
@@ -238,7 +238,7 @@ module _
         ( H))
 
   radical-of-ideal-hom-large-poset-Commutative-Ring :
-    hom-set-Large-Poset
+    hom-Large-Poset
       ( λ l → l)
       ( ideal-Commutative-Ring-Large-Poset A)
       ( radical-ideal-Commutative-Ring-Large-Poset A)

src/elementary-number-theory/integer-fractions.lagda.md

@@ -184,11 +184,11 @@ transitive-sim-fraction-ℤ x y z s r =
                             ( denominator-fraction-ℤ x)
                             ( denominator-fraction-ℤ y)))))))))))))
 
-eq-rel-sim-fraction-ℤ : Equivalence-Relation lzero fraction-ℤ
-pr1 eq-rel-sim-fraction-ℤ = sim-fraction-ℤ-Prop
-pr1 (pr2 eq-rel-sim-fraction-ℤ) = refl-sim-fraction-ℤ
-pr1 (pr2 (pr2 eq-rel-sim-fraction-ℤ)) = symmetric-sim-fraction-ℤ
-pr2 (pr2 (pr2 eq-rel-sim-fraction-ℤ)) = transitive-sim-fraction-ℤ
+equivalence-relation-sim-fraction-ℤ : equivalence-relation lzero fraction-ℤ
+pr1 equivalence-relation-sim-fraction-ℤ = sim-fraction-ℤ-Prop
+pr1 (pr2 equivalence-relation-sim-fraction-ℤ) = refl-sim-fraction-ℤ
+pr1 (pr2 (pr2 equivalence-relation-sim-fraction-ℤ)) = symmetric-sim-fraction-ℤ
+pr2 (pr2 (pr2 equivalence-relation-sim-fraction-ℤ)) = transitive-sim-fraction-ℤ
 ```
 
 ### The greatest common divisor of the numerator and a denominator of a fraction is always a positive integer

src/elementary-number-theory/rational-numbers.lagda.md

@@ -129,7 +129,7 @@ in-fraction-fraction-ℚ (pair (pair m (pair n n-pos)) p) =
 
 ```agda
 reflecting-map-sim-fraction :
-  reflecting-map-Equivalence-Relation eq-rel-sim-fraction-ℤ ℚ
+  reflecting-map-equivalence-relation equivalence-relation-sim-fraction-ℤ ℚ
 pr1 reflecting-map-sim-fraction = in-fraction-ℤ
 pr2 reflecting-map-sim-fraction {x} {y} H = eq-ℚ-sim-fractions-ℤ x y H
 ```