module TT.README where

-- This is the formalisation of the paper "The Groupoid-syntax of Type Theory is a Set"

-- typechecked using Agda version 2.8.0 and the Cubical Agda library
-- version 0.8 (avaiable at https://github.com/agda/cubical)

-- Section III. Variants of the syntax and the set interpretation

import TT.Wild.Syntax
import TT.Wild.Examples
import TT.Wild.TypeInterp
import TT.Wild.NotSet

import TT.Set.Syntax
import TT.Set.ConPath

import TT.Groupoid.Syntax
import TT.Groupoid.SetInterp
import TT.Groupoid.ToSet

-- Section IV. α-normalisation for the groupoid-syntax

import TT.Groupoid.NTy

-- Section V. Reaping the fruits

import TT.Groupoid.IsoSet
import TT.Set.SetInterp

import TT.Groupoid.CwF