diff --git a/README.md b/README.md
index 5f66243..ae69ec3 100644
--- a/README.md
+++ b/README.md
@@ -24,3 +24,96 @@ n ∈ nominal
 a ∈ opname
 ```
 
+## sappho subtyping rules
+
+```
+s, t, γ ⊢ δ
+---- [conj-left]
+s & t, γ ⊢ δ
+
+γ ⊢ s, t, δ
+---- [disj-right]
+γ ⊢ s | t, δ
+
+s, γ ⊢ δ
+t, γ ⊢ δ
+---- [disj-left]
+s | t, γ ⊢ δ
+
+γ ⊢ s, δ
+γ ⊢ t, δ
+---- [conj-right]
+γ ⊢ s & t, δ
+
+// XXX
+s => t, s, t, γ ⊢ δ
+---- [impl-left]
+s => t, s, γ ⊢ δ
+
+// discussion about implication below
+s, γ ⊢ t, δ
+---- [impl-right]
+γ ⊢ s => t, δ
+
+
+// box works as a kind of "forall" for concrete types
+box t, t, γ ⊢ δ
+---- [box-left]
+box t, γ ⊢ δ
+
+// (.)-- filters the contexts.
+γ-- ⊢ t, δ--
+---- [box-right]
+γ ⊢ box t, δ
+
+
+
+```
+
+
+### context operators
+
+```
+(t, γ)-- =def= t, γ--       if t == box s
+               γ--          otherwise
+```
+
+What happens when box is buried under type operators, like box s & box t? It
+could be that the above definition filters out too much of the contexts.
+
+My gut feeling™ makes me think it is just a matter of reordering sequent rules
+to get keep the things wanted in context, which for an algorithm sucks, but from
+a declarative standpoint would be okay. This needs some further validation, and
+of course a reformulation for the actual algorithm.
+
+
+
+
+### implication
+```
+
+γ ⊢ s => t, u => s, δ
+
+if s, then u => s holds
+if ¬s, then s => t holds
+
+```
+
+
+
+### interpretation of ⊢
+what is the interpretation of
+
+γ ⊢ δ?
+
+
+given a concrete type k
+
+conjunction of γ hold for k
+
+then 
+
+disjunction of δ hold for k
+
+
+