Pinned Repositories
birmingham-theory
The web page for the Birmingham theoretical computer science research group
book
A textbook on informal homotopy type theory
coqdoc-overlay
CT4P
Foundations
Development of the univalent foundations of mathematics in Coq
HoTT_Cohomology
Cohomology in HoTT
logical_verification_2021
monads
Coq code accompanying several articles on semantics of functional programming languages
rezk_completion
Rezk completion
UniMath
A unified approach to formalization of mathematical knowledge based on Univalent Foundations.
benediktahrens's Repositories
benediktahrens/CT4P
benediktahrens/monads
Coq code accompanying several articles on semantics of functional programming languages
benediktahrens/rezk_completion
Rezk completion
benediktahrens/UniMath
A unified approach to formalization of mathematical knowledge based on Univalent Foundations.
benediktahrens/Foundations
Development of the univalent foundations of mathematics in Coq
benediktahrens/logical_verification_2021
benediktahrens/birmingham-theory
The web page for the Birmingham theoretical computer science research group
benediktahrens/book
A textbook on informal homotopy type theory
benediktahrens/coqdoc-overlay
benediktahrens/EUProofInfra
European e-Infrastructure on Formal Proofs
benediktahrens/europroofnet.github.io
Sources of the EuroProofNet web site.
benediktahrens/gruppentheorie
benediktahrens/hollight_experiments
Experiments in HOL Light implementing syntax and category theory
benediktahrens/Ktheory
formalization of theorems of higher algebraic K-theory
benediktahrens/largecatmodules
Large category of modules over monads on top of UniMaths and Display category
benediktahrens/logic_and_proof
CMU Undergrad Course
benediktahrens/M-types
A formalization of M-types in Agda
benediktahrens/MGS-domain-theory
Lecture notes and exercises for the introductory course on domain theory and denotational semantics at the Midlands Graduate School (MGS) 2023
benediktahrens/milewski-ctfp-pdf
Bartosz Milewski's 'Category Theory for Programmers' unofficial PDF and LaTeX source
benediktahrens/omega_categories
Formalisation of strict omega categories and the homotopy hypothesis in type theory, using coinduction
benediktahrens/paigenorth.github.io
benediktahrens/Ross-Notes-2019
Ross Notes from 2019
benediktahrens/Schools
benediktahrens/SetHITs
benediktahrens/theorie-des-jeux
Course material for an introduction to game theory---in french
benediktahrens/Theory
Papers on aspects of Generalised Algebraic Theories, Contextual Categories and Mathematical Theory Of Data
benediktahrens/Triangles
Triangles
benediktahrens/TypeTheory
benediktahrens/VV-C-system-from-a-monad
This repository contains various versions of Voevodsky's paper "C-system of a module over a Jf-relative monad"
benediktahrens/VV-paths-Csystems-univ