B.P. Ahrens
29 records found
1
Authored
Univalent categories constitute a well-behaved and useful notion of category in univalent foundations. The notion of univalence has subsequently been generalized to bicategories and other structures in (higher) category theory. Here, we zoom in on monoidal categories and study ...
Bicategorical type theory
Semantics and syntax
We develop semantics and syntax for bicategorical type theory. Bicategorical type theory features contexts, types, terms, and directed reductions between terms. This type theory is naturally interpreted in a class of structured bicategories. We start by developing the semantic ...
C-systems were defined by Cartmell as models of generalized algebraic theories. B-systems were defined by Voevodsky in his quest to formulate and prove an initiality conjecture for type theories. They play a crucial role in Voevodsky's construction of a syntactic C-system from ...
In the present work, we describe what was necessary to genera ...
Contributed
Calculating the Fundamental Group of the Circle in Homotopy Type Theory
Formalized in the Coq Unimath library
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 ...
A Computer-Checked Library of Category Theory
Functors and F-Coalgebras
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
Formalising the Symmetry Book
Formalising the Symmetry Book using the UniMath library
Navigating Through Digital Printing Systems
The Use of a Domain-Specific Language for Route Finding in Digital Printing Systems
Cloud Monads
A novel concept for monadic abstraction over state in serverless cloud applications
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 ...