missing using

Co-authored-by: damiano <[email protected]>
leanprover-community · Jul 25, 2024 · 5d922af · 5d922af
1 parent c53c4f0
commit 5d922af
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/posts/tradeoff-of-defining-types-as-subobjects.md b/posts/tradeoff-of-defining-types-as-subobjects.md
@@ -93,7 +93,7 @@ deriving TopologicalSpace
 instance : MetricSpace Circle := Subtype.metricSpace
 ```
 
-In the Custom Structure design, these instances must be either copied over manually or transferred some kind of isomorphism.
+In the Custom Structure design, these instances must be either copied over manually or transferred using some kind of isomorphism.
 
 The Subobject design, by definition, lets all generic instances apply.