HoTT-Intro / Agda
Licence: gpl-3.0
Agda formalisation of the Introduction to Homotopy Type Theory
Stars: ✭ 50
Labels
Projects that are alternatives of or similar to Agda
Analysissummary
Vorlesung Analysis für Informatiker WS16/17 an der TUM
Stars: ✭ 10 (-80%)
Mutual labels: mathematics
Algorithms mathmodels
【国赛】【美赛】数学建模相关算法 MATLAB实现(2018年初整理)
Stars: ✭ 968 (+1836%)
Mutual labels: mathematics
Sudokus Colored
An experiment in R to color overimposed sudokus
Stars: ✭ 22 (-56%)
Mutual labels: mathematics
Bfgs Neldermead Trustregion
Python implementation of some numerical (optimization) methods
Stars: ✭ 8 (-84%)
Mutual labels: mathematics
Casadi
CasADi is a symbolic framework for numeric optimization implementing automatic differentiation in forward and reverse modes on sparse matrix-valued computational graphs. It supports self-contained C-code generation and interfaces state-of-the-art codes such as SUNDIALS, IPOPT etc. It can be used from C++, Python or Matlab/Octave.
Stars: ✭ 714 (+1328%)
Mutual labels: mathematics
Math Advanced Data Structures And Algorithms
Math, Advanced Data Structures & Algorithms - Please check before use
Stars: ✭ 40 (-20%)
Mutual labels: mathematics
Awesome Ai Books
Some awesome AI related books and pdfs for learning and downloading, also apply some playground models for learning
Stars: ✭ 855 (+1610%)
Mutual labels: mathematics
Imagine Old
Modeling and simulations using computational graphs
Stars: ✭ 25 (-50%)
Mutual labels: mathematics
Mathos Parser
A mathematical expression parser and evaluation library.
Stars: ✭ 26 (-48%)
Mutual labels: mathematics
Math Notes
Apuntes de las asignaturas de matemáticas en la UGR
Stars: ✭ 14 (-72%)
Mutual labels: mathematics
Cocalc
CoCalc: Collaborative Calculation in the Cloud
Stars: ✭ 888 (+1676%)
Mutual labels: mathematics
Awesome Streamlit
The purpose of this project is to share knowledge on how awesome Streamlit is and can be
Stars: ✭ 769 (+1438%)
Mutual labels: mathematics
Bacomathiques
Bacomathiques est un petit site web qui contient tout ce dont vous avez besoin pour réviser vos maths en toute tranquillité de la Première à la Terminale ! Que vous cherchiez à passer votre BAC ou que vous souhaitiez simplement réviser votre cours : tout est possible et tout est gratuit.
Stars: ✭ 12 (-76%)
Mutual labels: mathematics
Deep Learning Book Chapter Summaries
Attempting to make the Deep Learning Book easier to understand.
Stars: ✭ 952 (+1804%)
Mutual labels: mathematics
Agda
This repository contains an Agda formalisation of the Introduction to Homotopy Type Theory book by Egbert Rijke.
Discussion
Organisation
There is one file per section in the book, and the formalization follows the book in a linear fashion. As far as we can, we make sure that numbering in the book of definitions, lemmas, theorems, etc, corresponds to numbering in the formal development.
Naming conventions
- Most commonly, we use all lowercase names where words are separated by hyphens.
- Structure on the natural numbers has
ℕ
at the end of its name. For example, we havezero-ℕ
,one-ℕ
,succ-ℕ
,add-ℕ
,mul-ℕ
. We only useℕ
once at the end of a name. For instance, the fact that multiplication distributes from the left over addition is calledleft-distributive-mul-add-ℕ
. Similar for structure on the integers, the finite sets, the rationals, and so on. - The identity type is called
Id
, and we don't use infix notation for it. The only correct infix notation would be=
, but this symbol is taken up by the core Agda program. - Capitalization is used at the end of a name if we want to specify the category in which we are working. For example
hom-Group
is the type of group homomorphisms between any two groups, andℤ-Group
is the objectℤ
seen as a group. - In the naming scheme, the conclusion comes first, followed by the assumptions. For example,
is-contr-map-is-equiv
is the theorem that concludes that a map is contractible if it is an equivalence. Another example,type-Group
is the underlying type of a group.
Note that the project description data, including the texts, logos, images, and/or trademarks,
for each open source project belongs to its rightful owner.
If you wish to add or remove any projects, please contact us at [email protected].