Qu KonjacSource

Inductive-Recursive Types, Generally

I write about inductive-recursive types here. "Generally" means "higher inductive-inductive-recursive" or "quotient inductive-inductive-recursive". This may sound quite gnarly, but fortunately the specification of signatures can be given with just a few type formers in an appropriate framework.

In particular, we'll have a theory of signatures which includes Mike Shulman's higher IR example.

	{-# OPTIONS --type-in-type --with-K #-}

	open import Data.Product
	open import Relation.Binary.PropositionalEquality
	open import Relation.Nullary
	open import Data.Empty

	{-
	Russell's paradox can be encoded in MLTT + K + U:U, as formalised in
	https://github.com/KonjacSource/Russell-paradox-in-TT.