Stars
Wherein I encode adjoint logic in Agda
An agda library for developing synthetic category theory - and other synthetic mathematics
Synthetic Tait computability in intensional type theory
pdmosses / agda-stdlib
Forked from agda/agda-stdlibA fork of the Agda standard library
Intrinsic Verification of Formal Grammar Theory
Mechanization of Synthetic Tait Computability in Istari
Type theories as quotient inductive-inductive-recursive types
The groupoid CwF of containers, in Cubical Agda
Generation of diagrams like flowcharts or sequence diagrams from text in a similar manner as markdown
Open the right browser at the right time
An Agda formalisation of the theory of directed containers
Kitcat is an experimental Univalent mathematics library for proof theory, category theory, and computer science formalization in Agda
An axiom-free formalization of category theory in Coq for personal study and practical work
Mechanized proofs and example programs for the paper Type Inference Logics, published at OOPSLA24.
A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainer=@palmskog]
A proof assistant for higher-dimensional type theory
📝A simple and elegant markdown editor, available for Linux, macOS and Windows.
This google chrome extension hides Reels and recommendations on Facebook
An encryption-focused open source note taking application
This is an experimental base library which is supposed to contain functional datastructures and reflection code.
A markup-based typesetting system that is powerful and easy to learn.
A proof assistant and a dependently-typed language