A

Agda

Learn abstract math with agda 🚀

Exercises for the Type theory course held at the University of Padua for the master degree in Computer Science

Project for the type theory course held at the University of Padua. This project implements an implementation and proof for the merge sort algorithm

Lessons code for the Agda mini course held in Verona

Experiments in Binary numbers in Agda

In this work we will define a superset of integers (the complete integers), which contains the dual of integers along parity (e.g. the odd zero, the even one, ...). Then we will see how they form a ring and how they can be used as exponents for real numbers powers, in order to write functions which have a discontinuity in zero (the function itself or one of its derivates), as for example the absolute value and the sign function.

Documentation: https://ualib.gitlab.io . New version: https://github.com/ualib/agda-algebras

Notes based on Martin Escardo's 2019 MGS course on HoTT/UF in Agda