Bedrock Institute

Mechanizing the metaphysics of V

Outcrop Core and Outcrop Site: reusable semantic Markdown rendering and interactive formal-mathematics textbooks.

QIIT Brouwer-tree ordinals in Cubical Agda, with a recursive computing order defined without {-# TERMINATING #-}