μ-types, attempts 2 and 3

[rolyp]

Address some limitations of initial implementation:

• LaTeX in Notes
  • Type schemas (not System F style polymorphism), kinding contexts
  • Rather than separate syntax for polynomials, just have \mu.\tau (where \tau can't contain a function type)
  • Closed function spaces is a strict overapproximation of a strict positivity constraint
• Agda
  • Syntax of types, kinding rules
  • Generalise Poly to close under post-composition with arbitrary (strong) functor T
  • "Slicing" semantics which decorates every type constructor with T
• Interpret in generic C with finite products, finite (distributive) coproducts and ω-colimits, rather than Fam(C)
  • ❌ bad idea -- the W-type construction does the recursion in the index setoid, sidestepping colimits in C entirely, but if Fam(C) itself needs ω-colimits then so does C (and also needs cocontinuous products)
• Revisit fam-mu-types but with language-syntax-2
• Extend conservativity with Definable-mu

See also:

• CBN and similar translations for inductive types #35
• Extend definability to infinite coproducts #29

[rolyp]

To add to notes:

• Poly_𝒞 gives Nunes–Vákár style definition as subcategory of Cat, but formalisation instead use a syntactic Poly datatype (const/var/+/×/μ, de Bruijn over n) interpreted by fobj.