{-# OPTIONS --without-K --safe #-}

-- The Everything module of undecidability analysis
-- In Agda, we use first order de Bruijn indices to represent variables, that is, the
-- natural numbers.
module Everything where

-- Subtyping problems of all following calculi are undecidable.  In this technical
-- work, our reduction proofs stop at F<: deterministic (F<:ᵈ), the undecidability of
-- which is justified by Pierce92.

-- F<: F<:⁻ F<:ᵈ
import FsubMinus

-- D<:
-- 
-- The examination of D<: is composed of the following files:
import DsubDef -- defines the syntax of D<:.
import Dsub -- defines the simplified subtyping judgment per Lemma 2 in the paper.
import DsubFull -- defines the original definition of D<:.
import DsubEquivSimpler -- defines D<: normal form and shows that D<: subtyping is undecidable.
import DsubNoTrans -- shows that D<: subtyping without transitivity remains undecidable.
import DsubTermUndec -- shows that D<: term typing is also undecidable.

-- other things

-- properties of F<:⁻
import FsubMinus2