CF
C. Farkas
info
Please Note
<p>This page displays the records of the person named above and is not linked to a unique person identifier. This record may need to be merged to a profile.</p>
2 records found
1
A display map category, originally just called a class of display maps with a stability condition, can be used to model dependent type theory. There are several other constructions on categories that can serve a similar purpose, such as comprehension categories. In fact, the similarity of such concept has been well-known, and there even have been comparisons made using bicategories of such categorical notions.
In this thesis, I aim to formalise one such comparison, and implement it in a proof assistant. In order to do this, I needed to formalise display map categories, some related concepts, to then construct their bicategory, and show the comparison as a pseudofunctor into the bicategory of comprehension categories. The formalisation has been done using Univalent Foundations, while the implementation has been completed using Rocq, and more specifically the UniMath library.
...
In this thesis, I aim to formalise one such comparison, and implement it in a proof assistant. In order to do this, I needed to formalise display map categories, some related concepts, to then construct their bicategory, and show the comparison as a pseudofunctor into the bicategory of comprehension categories. The formalisation has been done using Univalent Foundations, while the implementation has been completed using Rocq, and more specifically the UniMath library.
...
A display map category, originally just called a class of display maps with a stability condition, can be used to model dependent type theory. There are several other constructions on categories that can serve a similar purpose, such as comprehension categories. In fact, the similarity of such concept has been well-known, and there even have been comparisons made using bicategories of such categorical notions.
In this thesis, I aim to formalise one such comparison, and implement it in a proof assistant. In order to do this, I needed to formalise display map categories, some related concepts, to then construct their bicategory, and show the comparison as a pseudofunctor into the bicategory of comprehension categories. The formalisation has been done using Univalent Foundations, while the implementation has been completed using Rocq, and more specifically the UniMath library.
In this thesis, I aim to formalise one such comparison, and implement it in a proof assistant. In order to do this, I needed to formalise display map categories, some related concepts, to then construct their bicategory, and show the comparison as a pseudofunctor into the bicategory of comprehension categories. The formalisation has been done using Univalent Foundations, while the implementation has been completed using Rocq, and more specifically the UniMath library.
The monad and examples from Haskell
A computer-checked library for Category Theory in Lean
Category Theory is a widely used field of Mathematics.
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 help us in this task. ...
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 help us in this task. ...
Category Theory is a widely used field of Mathematics.
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 help us in this task.
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 help us in this task.