B.P. Ahrens
16 records found
1
Formalising the Symmetry Book
Formalising the Symmetry Book using the UniMath library
Isomorphism is equality
A Coq formalisation of the proofs Isomorphism is equality by Coquand and Danielsson
A computer-checked library of category theory
Formally verifying currying via the product-exponential adjunction
A computer-checked library of category theory
Defining functors and their algebras
A Computer-Checked Library of Category Theory
Universal Properties of Category Theory in Functional Programming
A Computer-Checked Library of Category Theory
Functors and F-Coalgebras
The monad and examples from Haskell
A computer-checked library for Category Theory in Lean
Some concepts from it are often used in functional programming.
This paper will focus on the Monad and a few implementations of it from Haskell.
We will also present the computer-checked library we have written to ...
Calculating the Fundamental Group of the Circle in Homotopy Type Theory
Formalized in the Coq Unimath library
computers can understand. This enables computer-assisted proofs and the computerization of all mathematical knowledge. Homotopy Type Theory (HoTT) views types as topological spaces, unlocking new w ...