diff --git a/docs/about/cycle.md b/docs/about/cycle.md
new file mode 100644
index 0000000..1fdf345
--- /dev/null
+++ b/docs/about/cycle.md
@@ -0,0 +1,33 @@
+# Cyclic proofs and sappho
+
+It seems that cyclic proofs and sappho would be a good fit. The decision
+process of sappho's subtyping relation is based on the sequent calculus. Cyclic
+proofs is a system of proof search which looks for cycles in a proof tree where
+recursion leads to infinite growth of its branches. It would allow us to avoid
+explicitly using co-induction and thus simplify the description of the
+subtyping relation substantially.
+
+
+## Cyclic proofs summarized
+
+A pre-proof tree is made up of nodes representing the sequents and
+edges corresponding to the pairing of a premise with the conclusion of the
+proof rules used to derive it.
+
+In an infinite pre-proof tree there might be cycles. These are paths along
+which equivalent nodes repeat infinitely often. If we are able to identify such
+a path, and the proof makes "progress" each round of the cycle, we can admiss
+it as a proof. If this can be done for all infinite paths, the pre-proof tree
+admissable as an actual proof tree.
+
+
+In order to use this strategy to decide our subtyping relation, we need:
+* Proof rules
+* Proof tree cycle detection
+* Admissability check, i.e. does the cycle make progress.
+
+See here for more info:
+
+[fxpl/ln notes on cyclic
+proofs][github.com/fxpl/ln/blob/main/sequel/papper/notes/cyclic-proofs.md]
+