The future of cubism - integrating inductive families - no-confusion - injectivity for records - with and paths? - positivity checking? (check silenced warning) - cubical library - integrating with standard library? - subsprint: check wether standard library works. - 2-level type theory - subsprint: test & document 2-level TT - replace Setω, I, partial, subtypes - Jesper has implemented a 2-level (fibrant universe and non-fibrant) - use the ≡ of the non-fibrant as the the definitional equality. using rewriting rules. - move code from Haskell into agda. - experiment: implement cartesian version of cubical - do semisimplicial types (Reedy limits) - subsprint: merge 2-level with cubical - UIP and cubical (setoid TT). omit glue, but want hprop. glue -> propext, XTT? - what is cartesian tt and why should we care - compatible with mathematical models and classical logic - no ∧,∨,~ on I - hcomp -> hcom - subsprint: start implementing cartesian tt