From 5d922af0b58798c84a0e6e044d66cf462f1cdee3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Thu, 25 Jul 2024 15:01:41 +0300 Subject: [PATCH] missing using Co-authored-by: damiano --- posts/tradeoff-of-defining-types-as-subobjects.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/posts/tradeoff-of-defining-types-as-subobjects.md b/posts/tradeoff-of-defining-types-as-subobjects.md index a75c0cb9..0b8d725b 100644 --- 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.