Implementation plan for HK-DOT

[Blaisorblade]

An updated version of my plan from August 2020:

• stop indexing the Coq types of Dot semantic types by arity (via dependent types) (Drop dependent typing for predicates, try 3 #347);
• New: Limit dependency on sTEq_Eta Limit dependency on sTEq_Eta #345
• add syntax for HK-DOT (HK-gDOT syntax, v3 #302)
• New: optionally: fork the syntactic type system.
• Maybe: drop (typing rules for) singleton types (?), since they don't respect functionality. We could allow singletons that don't mention type parameters, but that complicates the judgment.
• (Dot: Enable syntactic values in types #365) enable writing syntactic values in types, for examples such as F.F (\nu z. { A = Int }) (aka, F Int). This might depend on the previous step, but the changes to the semantics don't.
• Then tackle functionality of type constructors (Define path equality and prove functionality of type constructors #396). (TODO: add the remaining steps from the plan).

[Blaisorblade]

TODO write down binary logrel on paper.