T

resizing-reflection

public

1 stars

0 forks

0 issues

Commits

List of commits on branch master.

Unverified

2bdd9313501d116c9efb4bd8c79f3343ead5e810

Update README.md

TTheoWinterhalter committed 7 years ago

Unverified

fb620f6b7d70d185c913c6154abdd2538b3220d1

Failure at proving equivalence is transitive

TTheoWinterhalter committed 8 years ago

Unverified

43de5e35e2d1956ebdd1d4e52272655552e52923

Partial λ case.

TTheoWinterhalter committed 8 years ago

Unverified

3ae229e41cc5792a2ec82732f8d5da9d32a94acc

Proof of Π translation

TTheoWinterhalter committed 8 years ago

Unverified

84c427a5e3e3c3ea78a963c9e50a3019720b9621

Deal with equivalence of sorts

TTheoWinterhalter committed 8 years ago

Unverified

d69c0e23b15bf10b061da107978f5360a43bfbae

Translation of context extension

TTheoWinterhalter committed 8 years ago

README

The README file for this repository.

Master Thesis with Nicolas Tabareau

Structure

quotient: My own implementation of quotient with resizing rules as axioms
rapport: Master Thesis (may be wrong)
reform: Formalization of the translation between MLTT + reflection and MLTT + axioms (given up)