An experimental library for Cubical Agda

The agda-unimath library

A work-in-progress core language for Agda, in Agda

Denotational semantics based on graph and filter models

I'm putting Palmgren's Constructive Sheaf Semantics into Agda. Defines sheaves via Grothendieck pretopologies.

A Logical Relation for Martin-Löf Type Theory in Agda