{-# OPTIONS
  --without-K
  --prop
  --rewriting
  --confluence-check
#-}

{-
This is the formalisaton for the paper

  Type theory in type theory with single substitutions

by Ambrus Kaposi and Szumi Xie.

It is available here: https://github.com/szumixie/single-subst

We typechecked it using Agda version 2.7.0.1. No library is needed.
-}

module TT.index where

import TT.CwF.Syntax       -- CwF-based syntax for a theory with Π and Coquand universe
import TT.CwF.Standard     -- its standard model

import TT.SSC.Syntax       -- the single substitution syntax for the same theory
import TT.SSC.Standard     -- its standard model
import TT.SSC.AlphaNorm    -- notion of α-normal forms (terms without explicit substitutions)
import TT.SSC.Lift         -- admissible equations
import TT.SSC.Parallel     -- all the CwF rules hold in the single substitution syntax

import TT.Isomorphism      -- the single substitution and CwF-based syntaxes are isomorphic