2016 (English)Other (Other academic)Text
The following is a formalisation of many of the proofs of arXiv:1610.08027 and arXiv:1612.05468 in Agda. Agda is a proof-checker and programming language based on dependent typetheory and pattern matching, which allow a very close correspondencebetween the style of proofs in the article and the formalised, machine-readable proof.
Place, publisher, year, edition, pages
2016. , 28 p.
agda, multisets, homotopy type theory
Research subject Mathematical Logic
IdentifiersURN: urn:nbn:se:su:diva-136903OAI: oai:DiVA.org:su-136903DiVA: diva2:1057544