KW
K.F. Wullaert
12 records found
1
Authored
We present a formalization of different categorical structures used to interpret linear logic. Our formalization takes place in UniMath, a library of univalent mathematics based on the Coq proof assistant. All the categorical structures we formalize are based on monoidal categ ...
We describe a generic construction of non-wellfounded syntax involving variable binding and its monadic substitution operation.
Our construction of the syntax and its substitution takes place in category theory, notably by using monoidal categories and strong functors be ...
Our construction of the syntax and its substitution takes place in category theory, notably by using monoidal categories and strong functors be ...
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 ...
Contributed
Denotational semantics of type theories provide a framework for understanding and reasoning about type theories and the behaviour of programs and proofs. In particular, it is important to study what can and can not be proved within Martin-Löf Type Theory (MLTT) as it is the basis
...
Calculating the Fundamental Group of the Circle in Homotopy Type Theory
Formalized in the Coq Unimath library
The goal of this paper is to formalize the Fundamental Group of the Circle within Coq and the Unimath library, as described in the paper by Mr Licata and Mr Shulman, and show it is isomorphic to Z. Fundamental groups are a powerful algebraic invariant for studying Homotopy theory
...
Isomorphism is equality
A Coq formalisation of the proofs Isomorphism is equality by Coquand and Danielsson
This paper will give a formalisation of proofs, given in the paper "isomorphism is equality", in the proof assistant language Coq. The formalisations will be added to UniMath library. A library containing machine readable proofs in the mathematical field of Homotopy Type theory,
...
Formalising the Symmetry Book
Formalising the Symmetry Book using the UniMath library
To address the challenge of the time-consuming nature of proofreading proofs, computer proof assistants—such as the Coq proof assistant—have been developed. The Univalent Mathematics project aims to formalise mathematics using the Coq proof assistant from a univalent perspective,
...
This paper focuses on implementing and verifying the proofs presented in ``Finite Sets in Homotopy Type Theory" within the UniMath library. The UniMath library currently lacks support for higher inductive types, which are crucial for reasoning about finite sets in Homotopy Type T
...
Type Theory enables mathematicians to perform proofs in a formal language that
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 ...
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 ...
This paper is a literature survey on homotopy type theory, analyzing the formalization of sets within homotopy type theory. Set theory is embedded in homotopy type theory via h-sets, with all h-sets forming the type Set. This paper presents the properties of the type Se
...
This report explores the differences in implementations of homotopy type theory using different definitions of finite sets. The expressive ability of homotopy theory is explored when using the newly established definition and implementation of Kuratowski finite sets. This impleme
...
The incorporation of the univalence axiom into homotopy type theory has facilitated a new way of proving a basic result in algebraic topology: that the fundamental group of the circle is the integers (π1(S1) ≃ Z). This proof is formalised by Licata and Shulman. However, while the
...