updated extra/Subtyping-phil.lagda.md (#1017)

plfa · Jul 24, 2024 · ed27745 · ed27745
1 parent 496fdb1
commit ed27745
Showing 1 changed file with 5 additions and 4 deletions.
diff --git a/extra/Subtyping-phil.lagda.md b/extra/Subtyping-phil.lagda.md
@@ -155,14 +155,15 @@ Field = String
 ## Types
 
 ```agda
+data Type : Set
+
 Type* : List Field → Set
+Type* as = ∀ (a : Field) → (a ∈ as) → Type
 
-data Type : Set where
+data Type where
   _⇒_   : Type → Type → Type
   `ℕ    : Type
-  ⦗_⦂_⦘ :  (as : List Field) → (AS : Map as Type) → {distinct as} → Type
-
-Type* as = ∀ (a : Field) → (a ∈ as) → Type
+  ⦗_⦂_⦘ :  (as : List Field) → (AS : Type* as) → {distinct as} → Type
 ```
 
 In addition to function types `A ⇒ B` and natural numbers `ℕ`, we