Pinned Repositories
agda-stdlib
The Agda standard library
Finite-Bags
groupoids
Groupoids vs 1-Types
HITs-Examples
Examples of Higher Inductive Types
nmvdw.github.io
replaceMin
RezkCompletion
The Rezk completion as a higher inductive types
SetHITs
Three-HITs
All higher inductive types can be obtained from three simple HITs.
UniMath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
nmvdw's Repositories
nmvdw/Three-HITs
All higher inductive types can be obtained from three simple HITs.
nmvdw/groupoids
Groupoids vs 1-Types
nmvdw/HITs-Examples
Examples of Higher Inductive Types
nmvdw/RezkCompletion
The Rezk completion as a higher inductive types
nmvdw/nmvdw.github.io
nmvdw/Finite-Bags
nmvdw/replaceMin
nmvdw/SetHITs
nmvdw/UniMath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
nmvdw/agda-stdlib
The Agda standard library
nmvdw/dutchcats.github.io
Website of the Dutch Categories And Types Seminar
nmvdw/encode-decode
nmvdw/EnrichedCats
nmvdw/EUTYPESPubs
Publications by EUTYPES members
nmvdw/FinitaryFunctors
nmvdw/FormalTheoryOfMonadsUnivalently
nmvdw/HoTT
Homotopy type theory
nmvdw/IEF-PartB
LaTeX template for Marie Sklodowska-Curie Individual Fellowships application (H2020-MSCA-IF-2014)
nmvdw/inductive_types_in_hott
nmvdw/Integers
nmvdw/InternalLanguageUnivCats
nmvdw/Nijn
nmvdw/TypeTheory
The mathematical study of type theories, in univalent foundations