Overview

HTTPS SSH

This repository contains (among other things), the source and formalisations for the paper

  • A Syntax for Higher Inductive-Inductive Types

by Ambrus Kaposi and András Kovács.

Materials related to this paper:

filename description
fscd sources and pdf of paper
haskell/elims-demo Haskell implementation
agda/HIITSyntaxPaper Formalisation in Agda