Pinned Repositories
alg
Alg is a program that generates all finite models of a first-order theory. It is optimized for equational theories.
CategoryTheory_Course
Documents for the course on Category theory
CMU
This repository contains projects (presentations, notes, etc...) that I do for my PhD
EPIT-2020
EPIT 2020 - Spring School on Homotopy Type Theory
GraphModel
We formalize aspects of the graph model of type theory
HoTT-Intro
An introductory course to Homotopy Type Theory
hott_cmu80818
Companion code to CMU course on Homotopy Type Theory
OEIS-A000001
sequential_colimits
agda-unimath
The agda-unimath library
EgbertRijke's Repositories
EgbertRijke/HoTT-Intro
An introductory course to Homotopy Type Theory
EgbertRijke/GraphModel
We formalize aspects of the graph model of type theory
EgbertRijke/OEIS-A000001
EgbertRijke/sequential_colimits
EgbertRijke/CMU
This repository contains projects (presentations, notes, etc...) that I do for my PhD
EgbertRijke/EPIT-2020
EPIT 2020 - Spring School on Homotopy Type Theory
EgbertRijke/hott_cmu80818
Companion code to CMU course on Homotopy Type Theory
EgbertRijke/alg
Alg is a program that generates all finite models of a first-order theory. It is optimized for equational theories.
EgbertRijke/book
A textbook on informal homotopy type theory
EgbertRijke/cubical
An experimental library for Cubical Agda
EgbertRijke/formally_etale
EgbertRijke/K-theory
This project is about formalizing some results in K-theory in homotopy type theory.
EgbertRijke/notes-cubical
Notes on cubical sets
EgbertRijke/agda-stdlib
The Agda standard library
EgbertRijke/agda-unimath
Univalent mathematics in Agda
EgbertRijke/dissertation
EgbertRijke/e-systems
E-systems
EgbertRijke/egbertrijke.github.io
Academic webpage for Egbert Rijke
EgbertRijke/formaltt
Formalization of type theory
EgbertRijke/HoTT
Homotopy type theory
EgbertRijke/HoTT_Lean
EgbertRijke/lean2
Lean theorem prover version 0.2 (it supports standard and HoTT modes)
EgbertRijke/leansnippets
Miscellaneous Lean code which doesn't belong in the standard library
EgbertRijke/lists-in-lean
A tutotrial on lists in lean
EgbertRijke/mathematics_in_lean
The user home repository for the Mathematics in Lean tutorial.
EgbertRijke/stlc
This aims to be the most pretentious implementation of stlc in existence
EgbertRijke/SymmetryBook
This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.
EgbertRijke/UniMath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
EgbertRijke/unimath-esystems
unimath-esystems
EgbertRijke/yoneda
comparative formalizations of the Yoneda lemma for 1-categories and infinity-categories