akuklev Goto Github PK

Requirements:

1. Nice handling of constructive Concrete Mathematics, Real Analysis, Basic Linear, Commutative and Universal Algebra, (non-higher) Category Theory
2. Support LEM and set-level AC as modalities. Ideally, also weaker forms of AC, nameley Dependent Choice and Ultrafilter Lemma.
3. (ideally) Eat itself (“The Gentle Art of Levitation” kind) and support Higher Category Theory

Technically, (1) requires:

1. Enough Univalent Universes and QIITs, in particular:
   • Unordered collections (unordered tuples, lists, finite sets, etc.)
   • Cauchy Reals and Partiality Monad
   • FOLDS-models satisfying higher structure identity principle
2. Have or fake subset types, support algebraic ornaments with implicit conversions
3. Have proper “large” categories and ZMC/S-style handling of smallness, enough commulativity to prove a nice version of Yoneda

We don't know yet, how to implement (3), but having enough quotient-inductive-inductive-recursive types to have initial algebras for all XATs is certainly a start. Perhaps having Equaliser Coinductive Types (dual of QITs) containing a form of strict equality in disguise, should be enough to define higher functors.

• Intuitionistic type theory with liberal identity type (i.e. without uniqueness of identity proofs) and dependent sums is known to play a role of “algebraic” presentation of finitely complete ∞-categories, if we add dependent products locally cartesian closed ∞-categories arise, addition of univalent universes leads to ∞-pretoposes. Type-theoretic description of weak ω-categories was recently given.
• We elaborate this intuition to a notion of extended algebraic theories (XATs), which can be seen as a generalization of Cartmell's Generalised Algebraic Theories w/o equations on sorts, and as stratification of Essentially Algebraic Theories. In particular, the initial model existence proof for EATs can be adopted.
• We describe their categorical (“functorial”) semantics in the doctrine of weak model categories.
• We show how bidirectionally presented type theories are XATs.
• We study two instances of Baez-Dolan microcosm principle:
  • Category of models of a given theory is a weak model category itself
  • For a large class of theories T, a theory T' can be derived, so that there is a natural notion of V-enriched T-s for each T'-algebra V. For example, for the theory T of ordinary categories, T' is the theory of virtual double categories, so that for any virtual double category V the notion of V-enriched categories can be defined.

Develop a syntactic formalism and a doctrine implementing semantics for algebraic theories over a generalized field K. In the case of 𝔽₁, the logic of joinable partial computations should emerge., Hopf Algebras reduce to Groups etc. For complex disk, the theories relevant to quantum measurement and entanglement might probably emerge.

• Adjoint Logics to encompass concurrency (typed actor model)
• Linear Type Theory (Spectra, Quantum Computing)
• Typed quantum actor model?
• Algebraic effects as finitely-presented monads: free monads modulo “relations” in form of a related Dijkstra monad
• Algebraic coeffects: as protocols of communication to indeterministic objects with incapsulated mutable state

• Elaborate on duality between rapidly-growing “Nat -> Nat” functions and natural ordinal notation systems (a form of inductive types), provide a straightforward way to encode both by a diaphantine equation: equation has solution for arbitrary x ⇔ “the relational description does indeed define a total rapidly-growing function” ⇔ “transfinite induction up to θ always terminates”.
• A finitist logical system for ordinal analysis (where complex cut elimination proofs can be carried out) implemented as extrinsic type system for diophantine equations. No unconditionally true judgements beyond ω², conditional judgements of the form “well-founded induction up to θ proves consistency of logical system Ξ” with meaning explanation “totality of a relationally-described rapidly-growing function for arguments up to n implies cut-elimination for Ξ-sentences with length up to n”. Ideally a self-verifying theory.

School Geometry is the subject where most students first encounter formal proofs. A language for machine-verifiable yet easily human-readable proofs would greatly expand accessability of good math education, especially if incorporated into a visial tool (an app for tablet computers) that helps to construct one's own proofs, understand the other's proofs, play, share and learn the language and tools step-by-step in a gamified fasion. <www.euclidea.xyz>

Doing hundreeds of excersises to learn how to calculate, how to deal with algebraic expressions, solve equations, etc. is extremly boring, while being the only known way to internalise the language of mathematics. At the age of clip culture-leaning progressive education and ever increasing ADHS prevalence, most kids never get fluent enough in quantitative and conceptual languages of mathematics and natural sciences to enjoy them. Gamification seems to be at least a partial way out. <www.triradix.com>