add complete lifted sets

1 files changed, 17 insertions, 8 deletions

diff --git a/README.md b/README.md
index dedb96d..130bfc1 100644
--- a/README.md
+++ b/README.md
@@ -23,7 +23,7 @@ Note: the checker does not presently support η-equivalence in all cases and so
 ### Judgements
 - `C ctx` means `C` is a context.
 - `C ⊢ X set` means `X` is a set in context `C`.
-- `C ⊢ m : X` means `m` is a match of set `X`.
+- `C ⊢ m : X` means `m` is an element of set `X`.
 - `C ⊢ S signature` means `S` is a signature in context `C`.
 - `C ⊢ I :: S` means `I` is an instance of signature `S`.
 
@@ -52,11 +52,11 @@ For each `B ∈ { Nat, Int, Float, Str }`:
 - **η.** `m=record { x0=m .x0, ..., xn=m .xn }` when `m : record { ... }`.
 
 #### Variants
-- **Formation.** `C ⊢ variant { v0 : X0 | ... | vn : Xn } set` when each `C ⊢ Xi set`.
-- **Intro.** `C ⊢ vi. m : variant { v0 : X0 | ... | vn : Xn }` when `C ⊢ m : Xi`.
-- **Elim.** `C ⊢ case m of { v0. x0 => n0 | ... | vn. xn => nn } : X` when `C ⊢ m : variant { v0 : X0 | ... | vn : Xn }` and, for each `i`, `C, xi : Xi ⊢ ni : X`.
-- **β.** `case vi. m of { ... | vi. xi => ni | ... }=ni[m/xi]`.
-- **η.** `m=case m of { v0. x0 => v0. x0 | ... | vn. xn => vn. xn }` when `m : variant { ... }`.
+- **Formation.** `C ⊢ variant [ v0 : X0 | ... | vn : Xn ] set` when each `C ⊢ Xi set`.
+- **Intro.** `C ⊢ vi. m : variant [ v0 : X0 | ... | vn : Xn ]` when `C ⊢ m : Xi`.
+- **Elim.** `C ⊢ case m of [ v0. x0 => n0 | ... | vn. xn => nn ] : X` when `C ⊢ m : variant [ v0 : X0 | ... | vn : Xn ]` and, for each `i`, `C, xi : Xi ⊢ ni : X`.
+- **β.** `case vi. m of [ ... | vi. xi => ni | ... ]=ni[m/xi]`.
+- **η.** `m=case m of [ v0. x0 => v0. x0 | ... | vn. xn => vn. xn ]` when `m : variant [ ... ]`.
 
 ### The signature layer
 
@@ -87,13 +87,22 @@ For each `B ∈ { Nat, Int, Float, Str }`:
 
 #### Instances via case analysis
 A construction admitting an instance of any signature, given an element of a variant set and a branch for every tag.
-- **Intro.** `C ⊢ case m of { v0. x0 => I0 | ... | vn. xn => In } :: S` when `C ⊢ S signature`, `C ⊢ m : variant { v0. : X0 | ... | vn. : Xn }`, and, for each `i`, `C, xi : Xi ⊢ Ii :: S`.
-- **β.** `case vi. m of { ... | vi. xi => Ii | ... }=Ii[m/xi]`.
+- **Intro.** `C ⊢ case m of [ v0. x0 => I0 | ... | vn. xn => In ] :: S` when `C ⊢ S signature`, `C ⊢ m : variant [ v0. : X0 | ... | vn. : Xn ]`, and, for each `i`, `C, xi : Xi ⊢ Ii :: S`.
+- **β.** `case vi. m of [ ... | vi. xi => Ii | ... ]=Ii[m/xi]`.
+
+#### Lifted sets
+- **Formation.** `C ⊢ <X> signature` when `C ⊢ X set`.
+- **Intro.** `C ⊢ <m> :: <X>` when `C ⊢ m : X`.
+- **Elim.** `C ⊢ element-of(I) : X` when `C ⊢ I :: <X>`.
+- **β.** `element-of(<m>)=m` when `m : X`.
+- **η.** `I=<element-of(I)>` when `I :: <X>`.
 
 ### Notes
 
 There are no formal large eliminators, and as such we cannot perform case analysis on an element and produce varying set or signatures. However, the former construction may be losslessly encoded by detouring through instances-via-case-analysis and the signature `Set`. That is, `set-of(case m of [ ... | vi. xi => Xi :: Set | ... ])` is a set that varies depending on an element.
 
+The signatures `Set` and `<_>` each give a full isomorphism between the corresponding set-layer and signature-layer notion (sets ~ instances of `Set`; elements of `X` ~ instances of `<X>`), via `set-of`/`element-of` respectively. These are parallel in some sense, and do not interact.
+
 # License
 
 Copyright tslil clingman 2026, this programme is free software and is made available under the terms of the GPL v3 or later. See LICENSE for details.