Minor improvements

martinescardo · Sep 8, 2023 · 82ce8f9 · 82ce8f9
1 parent 72e37ac
commit 82ce8f9
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 24 deletions.
diff --git a/source/InjectiveTypes/MathematicalStructures.lagda b/source/InjectiveTypes/MathematicalStructures.lagda
@@ -665,24 +665,19 @@ Monoid-is-closed-under-prop-Π {𝓤} = V
     : (p : Ω 𝓤)
       (A : p holds → 𝓤 ̇)
       (α : (h : p holds) → monoid-structure (A h))
-    → ((h : p holds) → monoid-axioms (A h) (α h))
+      (F : (h : p holds) → monoid-axioms (A h) (α h))
     → monoid-axioms (Π A) (ρ⁻¹ p A α)
   axioms-closed-under-prop-Π p A α F = I , II , III , IV
    where
-    ρ⁻¹-remark : (p : Ω 𝓤)
-                 (A : p holds → 𝓤 ̇)
-                 (α : (h : p holds) → monoid-structure (A h))
-               → ρ⁻¹ p A α
-               ＝ (λ (f : Π A) (g : Π A) (h : p holds) → pr₁ (α h) (f h) (g h)) ,
-                                                         (λ h → pr₂ (α h))
-    ρ⁻¹-remark p A α = refl
-
     _·_ : Π A → Π A → Π A
     f · g = λ h → pr₁ (α h) (f h) (g h)
 
     e : Π A
     e h = pr₂ (α h)
 
+    ρ⁻¹-remark : ρ⁻¹ p A α ＝ (_·_ , e)
+    ρ⁻¹-remark = refl
+
     I : is-set (Π A)
     I = Π-is-set fe' (λ h →
          case F h of

diff --git a/source/InjectiveTypes/MathematicalStructuresMoreGeneral.lagda b/source/InjectiveTypes/MathematicalStructuresMoreGeneral.lagda
@@ -368,8 +368,8 @@ open monoid
 ∞-Magma∙-structure = monoid-structure
 
 ∞-Magma∙-structure-Π-condition : technical-condition
-                                 (∞-Magma∙-structure {𝓤})
-                                 universes-are-aflabby-Π
+                                  (∞-Magma∙-structure {𝓤})
+                                  universes-are-aflabby-Π
 ∞-Magma∙-structure-Π-condition =
  technical-condition-×
   universes-are-aflabby-Π
@@ -381,10 +381,7 @@ ainjectivity-of-∞-Magma∙ {𝓤} =
  ainjectivity-of-type-of-structures
   ∞-Magma∙-structure
   universes-are-aflabby-Π
-  (technical-condition-×
-    universes-are-aflabby-Π
-    ∞-Magma-structure-Π-condition
-    Pointed-Π-condition)
+  ∞-Magma∙-structure-Π-condition
 
 \end{code}
 
@@ -415,24 +412,20 @@ Monoid-Π-condition {𝓤} =
     : (p : Ω 𝓤)
       (A : p holds → 𝓤 ̇)
       (α : (h : p holds) → monoid-structure (A h))
-    → ((h : p holds) → monoid-axioms (A h) (α h))
+      (F : (h : p holds) → monoid-axioms (A h) (α h))
     → monoid-axioms (Π A) (σ p A α)
   axioms-Π-condition p A α F = I , II , III , IV
    where
-    σ-remark : (p : Ω 𝓤)
-               (A : p holds → 𝓤 ̇)
-               (α : (h : p holds) → monoid-structure (A h))
-             → σ p A α
-             ＝ (λ (f : Π A) (g : Π A) (h : p holds) → pr₁ (α h) (f h) (g h)) ,
-                                                      (λ h → pr₂ (α h))
-    σ-remark p A α = refl
-
     _·_ : Π A → Π A → Π A
     f · g = λ h → pr₁ (α h) (f h) (g h)
 
     e : Π A
     e h = pr₂ (α h)
 
+    σ-remark : σ p A α ＝ (_·_ , e)
+    σ-remark = refl
+
+
     I : is-set (Π A)
     I = Π-is-set fe' (λ h →
          case F h of