AndrasKovacs

{-
Inductive-recursive universes, indexed by levels which are below an arbitrary type-theoretic ordinal number (see HoTT book 10.3). This includes all kinds of transfinite levels as well.

Checked with: Agda 2.6.1, stdlib 1.3

My original motivation was to give inductive-recursive (or equivalently: large inductive)
semantics to to Jon Sterling's cumulative algebraic TT paper:

AndrasKovacs

{-# language
  TypeInType, GADTs, RankNTypes, TypeFamilies,
  TypeOperators, TypeApplications,
  UnicodeSyntax, UndecidableInstances
#-}

import Data.Kind
import Data.Proxy

data Nat = Z | S Nat

AndrasKovacs

{-# language GADTs #-}

-- https://www.reddit.com/r/haskell/comments/9uz2f5/code_challenge_welltyped_tree_node_order/

data Tree a where
  OneT :: a -> Tree a
  Ap   :: (a -> b -> c) -> Tree a -> Tree b -> Tree c

data FunList a where

AndrasKovacs

-- https://stackoverflow.com/questions/52244800/how-to-normalize-rewrite-rules-that-always-decrease-the-inputs-size/52246261#52246261

open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Relation.Nullary
open import Data.Empty
open import Data.Star

data AB : Set where
  A : AB -> AB

AndrasKovacs

{-# language
  TypeInType, ScopedTypeVariables, RankNTypes,
  GADTs, TypeOperators, TypeApplications, BangPatterns
#-}

-- requires ghc-typelits-natnormalise
{-# options_ghc -fplugin GHC.TypeLits.Normalise #-}

{-|
Tested with ghc-8.4.3

AndrasKovacs

data Ty : Set where
  ι   : Ty
  _⇒_ : Ty → Ty → Ty
infixr 3 _⇒_

data Con : Set where
  ∙   : Con
  _▶_ : Con → Ty → Con
infixl 3 _▶_

AndrasKovacs

{-# language OverloadedStrings, UnicodeSyntax, LambdaCase,
             ViewPatterns, NoMonomorphismRestriction #-}
{-# options_ghc -fwarn-incomplete-patterns #-}

{- Minimal bidirectional dependent type checker with type-in-type. Related to Coquand's
   algorithm. #-}

import Prelude hiding (all)

AndrasKovacs

{-# language ScopedTypeVariables, RankNTypes, TypeFamilies,
             UndecidableInstances, GADTs, TypeOperators,
             TypeApplications, AllowAmbiguousTypes, TypeInType,
             StandaloneDeriving #-}

import Data.Kind

-- singletons
--------------------------------------------------------------------------------

AndrasKovacs

{-# language TemplateHaskell, ScopedTypeVariables, RankNTypes,
             TypeFamilies, UndecidableInstances, DeriveFunctor, GADTs,
             TypeOperators, TypeApplications, AllowAmbiguousTypes,
             TypeInType, StandaloneDeriving #-}

import Data.Singletons.TH -- singletons 2.4.1
import Data.Kind

-- some standard stuff for later examples' sake

AndrasKovacs

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

{-
Below is an example of proving *everything* about the substitution calculus of a
simple TT with Bool.

The more challenging solution:
  - If substitutions are defined as lists of terms, then if you manage to
    prove that substitutions form a category, almost certainly you're done,
    since you can only prove this is you have all relevant lemmas.