[ re agda/#6368 ] Add blanket instance for TypeWithStr

agda · Jan 27, 2023 · f755e38 · f755e38
1 parent 545e873
commit f755e38
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 5 deletions.
diff --git a/Cubical/Algebra/Ring/Properties.agda b/Cubical/Algebra/Ring/Properties.agda
@@ -252,8 +252,6 @@ module RingHomTheory {R : Ring ℓ} {S : Ring ℓ'} (φ : RingHom R S) where
   open IsRingHom (φ .snd)
   private
     instance
-      _ = R
-      _ = S
       _ = snd R
       _ = snd S
     f = fst φ

diff --git a/Cubical/Algebra/Ring/Quotient.agda b/Cubical/Algebra/Ring/Quotient.agda
@@ -215,15 +215,13 @@ module UniversalProperty (R : Ring ℓ) (I : IdealsIn R) where
   Iₛ = fst I
   private
     instance
-      _ = R
       _ = snd R
 
   module _ {S : Ring ℓ'} (φ : RingHom R S) where
     open IsRingHom
     open RingHomTheory φ
     private
       instance
-        _ = S
         _ = snd S
       f = fst φ
       module φ = IsRingHom (snd φ)

diff --git a/Cubical/Foundations/Structure.agda b/Cubical/Foundations/Structure.agda
@@ -25,6 +25,10 @@ str = snd
 ⟨_⟩ : TypeWithStr ℓ S → Type ℓ
 ⟨_⟩ = typ
 
+instance
+  mkTypeWithStr : ∀ {ℓ} {S : Type ℓ → Type ℓ'} {X} → {{S X}} → TypeWithStr ℓ S
+  mkTypeWithStr {{i}} = _ , i
+
 -- An S-structure should have a notion of S-homomorphism, or rather S-isomorphism.
 -- This will be implemented by a function ι : StrEquiv S ℓ'
 -- that gives us for any two types with S-structure (X , s) and (Y , t) a family:
@@ -41,4 +45,3 @@ EquivAction {ℓ} S = {X Y : Type ℓ} → X ≃ Y → S X ≃ S Y
 EquivAction→StrEquiv : {S : Type ℓ → Type ℓ''}
   → EquivAction S → StrEquiv S ℓ''
 EquivAction→StrEquiv α (X , s) (Y , t) e = equivFun (α e) s ≡ t
-