diff --git a/GeneralizedAlgebra.lean b/GeneralizedAlgebra.lean
index 369c3a0..a1c9d55 100644
--- a/GeneralizedAlgebra.lean
+++ b/GeneralizedAlgebra.lean
@@ -5,102 +5,104 @@ import GeneralizedAlgebra.signatures.set
 import GeneralizedAlgebra.signatures.pointed
 import GeneralizedAlgebra.signatures.bipointed
 import GeneralizedAlgebra.signatures.nat
-import GeneralizedAlgebra.signatures.evenodd
-import GeneralizedAlgebra.signatures.quiver
-import GeneralizedAlgebra.signatures.refl_quiver
-import GeneralizedAlgebra.signatures.monoid
-import GeneralizedAlgebra.signatures.group
-import GeneralizedAlgebra.signatures.preorder
-import GeneralizedAlgebra.signatures.setoid
-import GeneralizedAlgebra.signatures.category
-import GeneralizedAlgebra.signatures.groupoid
-import GeneralizedAlgebra.signatures.CwF
-import GeneralizedAlgebra.signatures.PCwF
+-- import GeneralizedAlgebra.signatures.evenodd
+-- import GeneralizedAlgebra.signatures.quiver
+-- import GeneralizedAlgebra.signatures.refl_quiver
+-- import GeneralizedAlgebra.signatures.monoid
+-- import GeneralizedAlgebra.signatures.group
+-- import GeneralizedAlgebra.signatures.preorder
+-- import GeneralizedAlgebra.signatures.setoid
+-- import GeneralizedAlgebra.signatures.category
+-- import GeneralizedAlgebra.signatures.groupoid
+-- import GeneralizedAlgebra.signatures.CwF
+-- import GeneralizedAlgebra.signatures.PCwF
 
 
 /-
 ## Basic structures
 -/
--- Sets
-#eval 𝔖𝔢𝔱
-#eval Alg 𝔖𝔢𝔱
-#eval DAlg 𝔖𝔢𝔱 none ["P"]
-#eval DAlg 𝔖𝔢𝔱 (some "𝔖𝔢𝔱") ["P"]
-
--- Pointed sets
-#eval 𝔓
-#eval Alg 𝔓
-#eval DAlg 𝔓 none ["P"]
-#eval DAlg 𝔓 (some "𝔓") ["P","p₀"] ["X","x₀"]
-
--- Bipointed sets
-#eval 𝔅
-#eval Alg 𝔅
-#eval DAlg 𝔅 none ["P"]
-#eval DAlg 𝔅 (some "𝔅") ["P","p₀","p₁"]
-
--- Natural numbers
 #eval 𝔑
-#eval Alg 𝔑
-#eval DAlg 𝔑 none ["P","n"] ["N","z","s"]
-#eval DAlg 𝔑 (some "𝔑") ["P","base_case","n","ind_step"]
-
--- Even/Odd Natural Numbers
-#eval 𝔈𝔒
-#eval Alg 𝔈𝔒
-#eval DAlg 𝔈𝔒 none ["Pe","Po","n","m"]
-#eval DAlg 𝔈𝔒 (some "𝔑") ["Pe", "Po", "bc","n","ih","m","ih'"]
-
--- Monoids
-#eval 𝔐𝔬𝔫
--- #eval Alg 𝔐𝔬𝔫 none
-#eval Alg 𝔐𝔬𝔫 (some "𝔐𝔬𝔫")
-
--- Groups
-#eval 𝔊𝔯𝔭
--- #eval Alg 𝔊𝔯𝔭 none
-#eval Alg 𝔊𝔯𝔭 (some "𝔊𝔯𝔭")
-
-/-
-## Quiver-like structures
--/
--- Quivers
-#eval 𝔔𝔲𝔦𝔳
-#eval Alg 𝔔𝔲𝔦𝔳
-
--- -- Reflexive quivers
-#eval 𝔯𝔔𝔲𝔦𝔳
-#eval Alg 𝔯𝔔𝔲𝔦𝔳
+#eval 𝔑.elim AlgStr
+-- Sets
+-- #eval 𝔖𝔢𝔱
+-- #eval Alg 𝔖𝔢𝔱
+-- #eval DAlg 𝔖𝔢𝔱 none ["P"]
+-- #eval DAlg 𝔖𝔢𝔱 (some "𝔖𝔢𝔱") ["P"]
+
+-- -- Pointed sets
+-- #eval 𝔓
+-- #eval Alg 𝔓
+-- #eval DAlg 𝔓 none ["P"]
+-- #eval DAlg 𝔓 (some "𝔓") ["P","p₀"] ["X","x₀"]
+
+-- -- Bipointed sets
+-- #eval 𝔅
+-- #eval Alg 𝔅
+-- #eval DAlg 𝔅 none ["P"]
+-- #eval DAlg 𝔅 (some "𝔅") ["P","p₀","p₁"]
+
+-- -- Natural numbers
+-- #eval 𝔑
+-- #eval Alg 𝔑
+-- #eval DAlg 𝔑 none ["P","n"] ["N","z","s"]
+-- #eval DAlg 𝔑 (some "𝔑") ["P","base_case","n","ind_step"]
+
+-- -- Even/Odd Natural Numbers
+-- #eval 𝔈𝔒
+-- #eval Alg 𝔈𝔒
+-- #eval DAlg 𝔈𝔒 none ["Pe","Po","n","m"]
+-- #eval DAlg 𝔈𝔒 (some "𝔑") ["Pe", "Po", "bc","n","ih","m","ih'"]
 
 -- -- Monoids
-#eval 𝔐𝔬𝔫
-#eval Alg 𝔐𝔬𝔫 (some "𝔐𝔬𝔫")
-
--- -- Preorders
-#eval 𝔓𝔯𝔢𝔒𝔯𝔡
-#eval Alg 𝔓𝔯𝔢𝔒𝔯𝔡 (some "𝔓𝔯𝔢𝔒𝔯𝔡")
-
--- -- Setoids
-#eval 𝔖𝔢𝔱𝔬𝔦𝔡
-#eval Alg 𝔖𝔢𝔱𝔬𝔦𝔡 (some "𝔖𝔢𝔱𝔬𝔦𝔡")
-
--- -- Categories
-#eval ℭ𝔞𝔱
-#eval Alg ℭ𝔞𝔱 (some "ℭ𝔞𝔱")
-
--- -- Groupoids
-#eval 𝔊𝔯𝔭𝔡
-#eval Alg 𝔊𝔯𝔭𝔡 (some "𝔊𝔯𝔭𝔡")
-
-
-/-
-## Models of Type Theory
--/
--- Categories with Families
-#eval ℭ𝔴𝔉
-#eval Alg ℭ𝔴𝔉 (some "ℭ𝔴𝔉")
-#eval Alg ℭ𝔴𝔉 none CwF_inlinenames
-
--- -- Polarized Categories with Families
-#eval 𝔓ℭ𝔴𝔉
-#eval Alg 𝔓ℭ𝔴𝔉 (some "𝔓ℭ𝔴𝔉")
+-- #eval 𝔐𝔬𝔫
+-- -- #eval Alg 𝔐𝔬𝔫 none
+-- #eval Alg 𝔐𝔬𝔫 (some "𝔐𝔬𝔫")
+
+-- -- Groups
+-- #eval 𝔊𝔯𝔭
+-- -- #eval Alg 𝔊𝔯𝔭 none
+-- #eval Alg 𝔊𝔯𝔭 (some "𝔊𝔯𝔭")
+
+-- /-
+-- ## Quiver-like structures
+-- -/
+-- -- Quivers
+-- #eval 𝔔𝔲𝔦𝔳
+-- #eval Alg 𝔔𝔲𝔦𝔳
+
+-- -- -- Reflexive quivers
+-- #eval 𝔯𝔔𝔲𝔦𝔳
+-- #eval Alg 𝔯𝔔𝔲𝔦𝔳
+
+-- -- -- Monoids
+-- #eval 𝔐𝔬𝔫
+-- #eval Alg 𝔐𝔬𝔫 (some "𝔐𝔬𝔫")
+
+-- -- -- Preorders
+-- #eval 𝔓𝔯𝔢𝔒𝔯𝔡
+-- #eval Alg 𝔓𝔯𝔢𝔒𝔯𝔡 (some "𝔓𝔯𝔢𝔒𝔯𝔡")
+
+-- -- -- Setoids
+-- #eval 𝔖𝔢𝔱𝔬𝔦𝔡
+-- #eval Alg 𝔖𝔢𝔱𝔬𝔦𝔡 (some "𝔖𝔢𝔱𝔬𝔦𝔡")
+
+-- -- -- Categories
+-- #eval ℭ𝔞𝔱
+-- #eval Alg ℭ𝔞𝔱 (some "ℭ𝔞𝔱")
+
+-- -- -- Groupoids
+-- #eval 𝔊𝔯𝔭𝔡
+-- #eval Alg 𝔊𝔯𝔭𝔡 (some "𝔊𝔯𝔭𝔡")
+
+
+-- /-
+-- ## Models of Type Theory
+-- -/
+-- -- Categories with Families
+-- #eval ℭ𝔴𝔉
+-- #eval Alg ℭ𝔴𝔉 (some "ℭ𝔴𝔉")
+-- #eval Alg ℭ𝔴𝔉 none CwF_inlinenames
+
+-- -- -- Polarized Categories with Families
+-- #eval 𝔓ℭ𝔴𝔉
+-- #eval Alg 𝔓ℭ𝔴𝔉 (some "𝔓ℭ𝔴𝔉")
diff --git a/GeneralizedAlgebra/AlgPrinting.lean b/GeneralizedAlgebra/AlgPrinting.lean
index ace8a8b..1c7824f 100644
--- a/GeneralizedAlgebra/AlgPrinting.lean
+++ b/GeneralizedAlgebra/AlgPrinting.lean
@@ -1,192 +1,38 @@
 import GeneralizedAlgebra.signature
 
 open Nat
-open Con Subst Ty Tm
-open GAT
-
-
-mutual
-inductive Argument : Type where
-|  NonDep : List Token → Argument
-|  Dep : List Token → Argument
-inductive Token : Type where
-| printArg : Nat → Token
-| printVarName : Nat → Token
-| printStr : String → Token
-| printConstrSplit : Token
-| printArrow : Token
-| BREAK : Token
-end
-open Argument Token
-
-def newVar ( ty : List Token) : StateT (List Argument) Option Nat := do
-  let vars ← get
-  let new := NonDep ty
-  set $ vars++[new]
-  pure $ List.length vars
-
-def countDepends : List Argument → Nat
-| [] => 0
-| (Dep _)::rest => 1 + countDepends rest
-| (NonDep _)::rest => countDepends rest
-
-def getDepends : List Argument → Nat → Option (Bool × Nat × List Token)
-| [] , _ => none
-| (Dep ts)::_, 0 => return (true,0,ts)
-| (NonDep ts)::_, 0 => return (false,0,ts)
-| (Dep _)::rest, succ n => do
-    let (bit,res,ts) ← getDepends rest n
-    return (bit,succ res,ts)
-| (NonDep _)::rest, succ n => getDepends rest n
-
-def foldTokens_core (constrSplit : String) (varNames : List String) : Nat → List Argument → List Token → Option String
-| succ FUEL, args, printArrow::rest => do
-    let restStr ← foldTokens_core constrSplit varNames FUEL args rest
-    return (" → " ++ restStr)
-| succ FUEL, args, printConstrSplit::rest => do
-    let restStr ← foldTokens_core constrSplit varNames FUEL args rest
-    return (constrSplit ++ restStr)
-| succ FUEL, args, (printStr s)::rest => do
-    let restStr ← foldTokens_core constrSplit varNames FUEL args rest
-    return (s ++ restStr)
-| succ FUEL, args, (printArg n)::rest => do
-    let (doPrint, index, ts) ← getDepends args n
-    let printRest ← foldTokens_core constrSplit varNames FUEL args rest
-    let argType ← foldTokens_core constrSplit varNames FUEL args ts
-    let varName ← nth index varNames
-    if doPrint
-    then return ("(" ++ varName ++ " : " ++ argType ++ ")" ++ printRest)
-    else return (argType ++ printRest)
-| succ FUEL, args, (printVarName n)::rest => do
-    let (_, index, _) ← getDepends args n
-    let printRest ← foldTokens_core constrSplit varNames FUEL args rest
-    let varName ← nth index varNames
-    return (varName ++ printRest)
-| _,_,[] => some ""
-| _,_, _ => none
-
-def foldTokens (constrSplit : String := " × ") (varNames : List String) (args : List Argument):=
-  foldTokens_core constrSplit varNames 1000 args
-
-def genVarNames_core (REPR : Nat → String) (varLetter : String) : Nat → List String → Nat → List String
-| 0, varNames,_ => varNames
-| succ n, varNames,index => genVarNames_core REPR varLetter n (varNames ++ [varLetter ++ REPR index]) (succ index)
-
-def genVarNames (n : Nat) (starterNames : List String) (varLetter := "X_"): List String :=
-  genVarNames_core (if n < 10 then twoRepr else threeRepr) varLetter (n - List.length starterNames) (List.take n starterNames) 0
-
-def pingNth_core : List Argument → Nat → Option (List Argument)
-| [],_ => none
-| (NonDep ts)::rest,0 => some ((Dep ts)::rest)
-| x::rest,succ n => do
-  let res ← pingNth_core rest n
-  return (x::res)
-| L,_ => some L
-
-def pingNth (n :Nat) : StateT (List Argument) Option Unit := do
-  let current ← get
-  let new ← StateT.lift $ pingNth_core current n
-  set new
-
-mutual
-  def Alg_Con : Con → StateT (List Argument) Option (List Nat × List Token)
-  | EMPTY => pure $ ([],[printStr "⊤"])
-  | EMPTY ▷ UU => do
-      let theVar ← newVar [printStr "Set"]
-      pure ([theVar],[printArg theVar])
-  | Γ ▷ A => do
-    let (tel,res) ← Alg_Con Γ
-    let As ← Alg_Ty A tel
-    let theVar ← newVar As
-    pure (tel++[theVar],res ++ [printConstrSplit, printStr "(", printArg theVar, printStr ")"])
-  def Alg_Ty : Ty → List Nat → StateT (List Argument) Option (List Token)
-  | UU,_ => pure [printStr "Set"]
-  | EL X, tel => Alg_Tm X tel
-  | PI X Y, tel => do
-      let Xs ← Alg_Tm X tel
-      let Xvar ← newVar Xs
-      let Ys ← Alg_Ty Y (tel++[Xvar])
-      pure $ [printArg Xvar, printArrow] ++ Ys
-  | EQ t t',tel => do
-      let ts ← Alg_Tm t tel
-      let t's ← Alg_Tm t' tel
-      pure $ ts ++ [printStr " = "] ++ t's
-
-  | _,_ => StateT.lift none
-  def Alg_Tm (t : Tm) (tel : List Nat) : StateT (List Argument) Option (List Token) :=
-  match t,deBruijn t with
-    | _,some n => do
-        let glob_n ← StateT.lift (nthBackwards n tel)
-        pingNth glob_n
-        pure $ [printVarName glob_n]
-    | (APP f) [ PAIR (ID _) t ]t,_ => do
-        let fs ← Alg_Tm f tel
-        let ts ← Alg_Tm t tel
-        pure $ fs ++ [printStr " ("] ++ ts ++ [printStr ")"]
-    | _,_ => none
-end
-
-def Alg (𝔊 : GAT) (recordName : Option String := none) (comp_names : List String := []) : Option String := do
-  let ((tel,res),vars) ← StateT.run (Alg_Con (GAT.con 𝔊)) ([])
-  let vars' ← if recordName.isSome then List.foldlM pingNth_core vars tel else some vars
-  let compSep := if recordName.isSome then " \n    " else " × "
-  let comp_names := if comp_names.isEmpty then GAT.subnames 𝔊 else comp_names
-  let varNames := genVarNames (List.length vars') comp_names
-  let algStr ← foldTokens compSep varNames vars' res
-  match recordName with
-  | (some name) => return "record " ++ name ++ "-Alg where\n    " ++ algStr
-  | none => return algStr
-
-mutual
-  def DAlg_Con : List String → Con → StateT (List Argument) Option (List Nat × List Token)
-  | _,EMPTY => pure $ ([],[printStr "⊤"])
-  | carrier::_,EMPTY ▷ UU => do
-      let theVar ← newVar [printStr carrier,printArrow,printStr "Set"]
-      pure ([theVar],[printArg theVar])
-  | alg_comp::Alg_comp,Γ ▷ A => do
-    let (tel,res) ← DAlg_Con Alg_comp Γ
-    let As ← DAlg_Ty tel ([printStr alg_comp]::(List.map (λ x => [printStr x]) Alg_comp)) A
-    let theVar ← newVar As
-    pure (tel++[theVar],res ++ [printConstrSplit, printStr "(", printArg theVar, printStr ")"])
-  | _,_ => none
-  def DAlg_Ty : List Nat → List (List Token) → Ty → StateT (List Argument) Option (List Token)
-  | _,carrier::_,UU => pure $ carrier ++ [printArrow,printStr "Set"]
-  | tel,alg_elt::_,EL X => DAlg_Tm tel alg_elt X
-  | tel,alg_fn::alg_rest,PI X Y => do
-      let Atype ← (deBruijn X >>= λ n => nth n alg_rest) <|> some [printStr "?"]
-      let alpha ← newVar Atype
-      pingNth alpha
-      let Xs ← DAlg_Tm tel [printVarName alpha] X
-      let Xvar ← newVar Xs
-      let Ys ← DAlg_Ty (tel++[Xvar]) (([printStr "("]++alg_fn++[printStr " ",printVarName alpha,printStr ")"])::alg_rest) Y
-      pure $ [printArg alpha, printStr " → ",printArg Xvar, printStr " → "] ++ Ys
-  -- | EQ t t',tel => do
-  --     let ts ← DAlg_Tm t tel
-  --     let t's ← DAlg_Tm t' tel
-  --     pure $ ts ++ [printStr " = "] ++ t's
-
-  | _,_,_ => StateT.lift none
-  def DAlg_Tm (tel : List Nat) (alg_elt : List Token) (t : Tm) : StateT (List Argument) Option (List Token) :=
-  match t,deBruijn t with
-    | _,some n => do
-        let glob_n ← StateT.lift (nthBackwards n tel)
-        pingNth glob_n
-        pure $ [printVarName glob_n,printStr " "]++alg_elt
-  --   | (APP f) [ PAIR (ID _) t ]t,_ => do
-  --       let fs ← DAlg_Tm f tel
-  --       let ts ← DAlg_Tm t tel
-  --       pure $ fs ++ [printStr " "] ++ ts
-    | _,_ => none
-end
-
-def DAlg (𝔊 : GAT) (recordName : Option String := none) (comp_names : List String := []) (Alg_comp_names : List String := []) : Option String := do
-  let Alg_comp_names := if Alg_comp_names.isEmpty then 𝔊.topnames else Alg_comp_names
-  let Alg_comp := genVarNames (len 𝔊.con) Alg_comp_names "Y_"
-  let ((tel,res),vars) ← StateT.run (DAlg_Con (List.reverse Alg_comp) 𝔊.con) ([])
-  let vars' ← if recordName.isSome then List.foldlM pingNth_core vars tel else some vars
-  let compSep := if recordName.isSome then "\n    " else " × "
-  let varNames := genVarNames (List.length vars') comp_names
-  let algStr ← foldTokens compSep varNames vars' res
-  match recordName with
-  | (some name) => return "record " ++ name ++ "-DAlg " ++ collapse Alg_comp ++ " where\n    " ++ algStr
-  | none => return algStr
+open Ty Tm
+
+
+
+
+
+instance AlgStr : indData where
+  Con_D := λ _ => String
+  Ty_D := λ _ _ _ => String
+  Tm_D := λ _ _ _ _ _ => String
+  nil_D := "⋄"
+  cons_D := λ 𝔊 𝔊s A As => 𝔊s ++ " × " ++ As
+  UU_D := λ _ _ => "Set"
+  EL_D := λ _ 𝔊s _ Xs => 𝔊s ++ "-" ++ Xs
+  PI_D := λ _ _ _ _ _ _ => "w"
+  EQ_D := λ _ _ _ _ _ _ _ _ => "v"
+  VAR0_D := λ _ 𝔊s _ As A's => "(" ++ As ++ "|" ++ A's ++ ")"
+  VARSUCC_D := λ _ _ _ _ _ _ _ _ _ => "t"
+  APP_D := λ _ _ _ _ _ _ _ _ _ _ _ => "s"
+  TRANSP_D := λ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ => "r"
+
+-- instance Alg : indData where
+--   Con_D := λ _ => Type 1
+--   Ty_D := λ _ Γ _ => Γ → Type 1
+--   Tm_D := λ _ Γ _ A _ => (γ : Γ) → A γ
+--   nil_D := PUnit
+--   cons_D := λ 𝔊 Γ _ A => Sigma (λ γ => A γ)
+--   UU_D := λ _ _ _ => Type
+--   EL_D := λ _ 𝔊s _ Xs γ => Xs γ
+  -- PI_D := λ _ _ _ _ _ _ => "w"
+  -- EQ_D := λ _ _ _ _ _ _ _ _ => "v"
+  -- VAR0_D := λ _ 𝔊s _ As A's => "(" ++ As ++ "|" ++ A's ++ ")"
+  -- VARSUCC_D := λ _ _ _ _ _ _ _ _ _ => "t"
+  -- APP_D := λ _ _ _ _ _ _ _ _ _ _ _ => "s"
+  -- TRANSP_D := λ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ => "r"
diff --git a/GeneralizedAlgebra/ConPrinting.lean b/GeneralizedAlgebra/ConPrinting.lean
index 04d8fb9..6ba08f8 100644
--- a/GeneralizedAlgebra/ConPrinting.lean
+++ b/GeneralizedAlgebra/ConPrinting.lean
@@ -1,36 +1,60 @@
 import GeneralizedAlgebra.signature
 
 open Nat
-open Con Subst Ty Tm
+open Ty Tm
 
-mutual
-  def Con_toString : Con → String
-  | EMPTY => "⋄"
-  | Γ ▷ A => (Con_toString Γ) ++ " ▷ " ++ (Ty_toString A)
-  def Ty_toString : Ty → String
-  | UU => "U"
-  | EL X => "El " ++ paren (Tm_toString X)
-  | PI X UU => "Π " ++ paren (Tm_toString X) ++ " U"
-  | PI X Y => "Π " ++ paren (Tm_toString X) ++ " " ++ paren (Ty_toString Y)
-  | EQ t t' => "Eq " ++ paren (Tm_toString t) ++ " " ++ paren (Tm_toString t')
-  | SUBST_Ty σ T => (Ty_toString T) ++ " [ " ++ (Subst_toString σ) ++ " ]T"
+-- mutual
+--   def Con_toString : Con → String
+--   | EMPTY => "⋄"
+--   | Γ ▷ A => (Con_toString Γ) ++ " ▷ " ++ (Ty_toString A)
+--   def Ty_toString : Ty → String
+--   | UU => "U"
+--   | EL X => "El " ++ paren (Tm_toString X)
+--   | PI X UU => "Π " ++ paren (Tm_toString X) ++ " U"
+--   | PI X Y => "Π " ++ paren (Tm_toString X) ++ " " ++ paren (Ty_toString Y)
+--   | EQ t t' => "Eq " ++ paren (Tm_toString t) ++ " " ++ paren (Tm_toString t')
+--   | SUBST_Ty σ T => (Ty_toString T) ++ " [ " ++ (Subst_toString σ) ++ " ]T"
 
-  def Tm_toString (theTerm : Tm) : String :=
-  match deBruijn theTerm with
-  | some n => Nat.repr n
-  | _ => match theTerm with
-    | (APP f) [ PAIR (ID _) t ]t => (Tm_toString f) ++ " @ " ++ paren (Tm_toString t)
-    | PROJ2 σ => "π₂ " ++ (Subst_toString σ)
-    | APP f => "App " ++ paren (Tm_toString f)
-    | t [ σ ]t => paren (Tm_toString t) ++ " [ " ++ (Subst_toString σ) ++ " ]t "
-  def Subst_toString : Subst → String
-  | PROJ1 (ID _) => "wk"
-  | PROJ1 σ => "π₁ " ++ (Subst_toString σ)
-  | PAIR σ t => (Subst_toString σ) ++ " , " ++ paren (Tm_toString t)
-  | EPSILON _ => "ε"
-  | COMP σ τ => (Subst_toString σ) ++ " ∘ " ++ (Subst_toString τ)
-  | (ID _) => "id"
-end
+--   def Tm_toString (theTerm : Tm) : String :=
+--   match deBruijn theTerm with
+--   | some n => Nat.repr n
+--   | _ => match theTerm with
+--     | (APP f) [ PAIR (ID _) t ]t => (Tm_toString f) ++ " @ " ++ paren (Tm_toString t)
+--     | PROJ2 σ => "π₂ " ++ (Subst_toString σ)
+--     | APP f => "App " ++ paren (Tm_toString f)
+--     | t [ σ ]t => paren (Tm_toString t) ++ " [ " ++ (Subst_toString σ) ++ " ]t "
+--   def Subst_toString : Subst → String
+--   | PROJ1 (ID _) => "wk"
+--   | PROJ1 σ => "π₁ " ++ (Subst_toString σ)
+--   | PAIR σ t => (Subst_toString σ) ++ " , " ++ paren (Tm_toString t)
+--   | EPSILON _ => "ε"
+--   | COMP σ τ => (Subst_toString σ) ++ " ∘ " ++ (Subst_toString τ)
+--   | (ID _) => "id"
+-- end
+
+def mkParen (s:String) : String :=
+  if s.isNat then s else
+  if s="U" then s else "("++s++")"
+
+def wkStr (s : String) : String :=
+match s.toNat? with
+| (some n) => Nat.repr (succ n)
+| _ => s ++ "[wk]"
+
+instance ConStr_method : indData where
+  Con_D := λ _ => String
+  Ty_D := λ _ _ _ => String
+  Tm_D := λ _ _ _ _ _ => String
+  nil_D := "⋄"
+  cons_D := λ _ 𝔊s _ As => 𝔊s ++ " ▷ " ++ As
+  UU_D := λ _ _ => "U"
+  EL_D := λ _ _ _ Xs => "El " ++ (mkParen Xs)
+  PI_D := λ _ _ _ Xs _ Ys => "Π " ++ (mkParen Xs) ++ " " ++ (mkParen Ys)
+  EQ_D := λ _ _ _ Xs _ ss _ ts => "Eq " ++ Xs ++ " " ++ ss ++ " " ++ ts
+  VAR0_D := λ _ _ _ _ _ => "0"
+  VARSUCC_D := λ _ _ _ _ _ ts _ _ _ => wkStr ts
+  APP_D := λ _ _ _ _ _ _ _ fs _ xs _ => fs ++ " @ " ++ xs
+  TRANSP_D := λ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ => "r"
 
 instance GATRepr : Repr GAT :=
-⟨ λ 𝔊 _ => Con_toString 𝔊.con⟩
+⟨ λ 𝔊 _ => 𝔊.elim ConStr_method ⟩
diff --git a/GeneralizedAlgebra/nouGAT.lean b/GeneralizedAlgebra/nouGAT.lean
index 9298fdc..9afafc1 100644
--- a/GeneralizedAlgebra/nouGAT.lean
+++ b/GeneralizedAlgebra/nouGAT.lean
@@ -2,7 +2,7 @@ import GeneralizedAlgebra.signature
 import Lean
 
 open Lean Elab Meta
-open Con Subst Ty Tm
+open Ty Tm
 
 declare_syntax_cat gat_ty
 syntax "U"       : gat_ty
@@ -80,15 +80,17 @@ structure varTel (VV : varStruct) where
 def varLookup (VV : varStruct) (key : String) : MetaM Expr
 := VV.f key
 
+#check mkNatLit
+
 def varExtend (VV : varStruct) (key : String) (ctx : Expr) (newType : Expr) (newCtx : Expr) (newTelescope : List metaArg) (resT : Expr): varStruct :=
 ⟨ λ s =>
     if s=key
-    then mkAppM ``V0 #[ ctx , newType ]
+    then mkAppM ``VAR #[ mkNatLit 0 ]
     else do
       let old ← varLookup VV s
-      let ID ← mkAppM ``ID #[newCtx]
-      let p ← mkAppM ``PROJ1 #[ID]
-      mkAppM ``SUBST_Tm #[ p , old],
+      -- let ID ← mkAppM ``ID #[newCtx]
+      -- let p ← mkAppM ``PROJ1 #[ID]
+      mkAppM ``WkTm #[ old ],
   VV.topnames ++ [key],
   VV.telescopes ++ [(newTelescope,resT)],
   λ s => if s=key then return newTelescope else VV.getArgs s
@@ -106,12 +108,10 @@ def varTelLookup {VV : varStruct} (TT : varTel VV) (key : String) : MetaM (Expr
 def varTelExtend {VV : varStruct} (TT : varTel VV) (newArg : metaArg) (ctx : Expr)  (newCtx : Expr) : varTel VV :=
 ⟨ λ s =>
     if argMatch s newArg
-    then mkAppM ``V0 #[ ctx , extractMetaTy newArg ]
+    then mkAppM ``VAR #[ mkNatLit 0 ]
     else do
       let (old,_) ← varTelLookup TT s
-      let ID ← mkAppM ``ID #[newCtx]
-      let p ← mkAppM ``PROJ1 #[ID]
-      mkAppM ``SUBST_Tm #[ p , old],
+      mkAppM ``WkTm #[ old ],
   TT.args ++ [newArg],
 ⟩
 
@@ -132,19 +132,20 @@ partial def elabGATTm {vars : varStruct} (ctx : Expr) (TT : varTel vars) : Synta
 | `(gat_tm| $g1:gat_tm $g2:gat_tm ) => do
       let (t1,args1) ← elabGATTm ctx TT g1
       let (A,args1') ← splitArgList "Too many args #0" args1
-        -- TODO: Check the type of A against the type of t2
-      let Appt1 ← mkAppM ``APP #[t1]
+      let domain := extractMetaTy A
+--         -- TODO: Check the type of A against the type of t2
+      -- let Appt1 ← mkAppM ``APP #[t1]
       let (t2,args2)← elabGATTm ctx TT g2
       failIfExplicitArgs "Insufficient Args #0" args2
-      -- let actualT2 ← reduce t2
-      -- let expectedT2 ← reduce (extractMetaTy A)
-      -- let tyMatch ← isDefEq actualT2 expectedT2
-      -- if (not tyMatch) then
-      --   throwError "X"
-      -- else do
-      let ID ← mkAppM ``ID #[ctx]
-      let substt2 ← mkAppM ``PAIR #[ID,t2]
-      let resT ← mkAppM ``SUBST_Tm #[substt2,Appt1]
+--       -- let actualT2 ← reduce t2
+--       -- let expectedT2 ← reduce (extractMetaTy A)
+--       -- let tyMatch ← isDefEq actualT2 expectedT2
+--       -- if (not tyMatch) then
+--       --   throwError "X"
+--       -- else do
+--       let ID ← mkAppM ``ID #[ctx]
+--       let substt2 ← mkAppM ``PAIR #[ID,t2]
+      let resT ← mkAppM ``APP #[t1,domain,t1,t2]
       return (resT,args1')
 | `(gat_tm| $i:ident ) => do
       varTelLookup TT i.getId.toString
@@ -174,7 +175,7 @@ partial def elabGATArg {vars : varStruct} (ctx : Expr) (TT : varTel vars) : Synt
 
 
 partial def elabGATTy {vars : varStruct} (ctx : Expr) (TT : varTel vars) : Syntax → MetaM (varTel vars × Expr × Expr)
-| `(gat_ty| ( $g:gat_ty ) ) => elabGATTy ctx TT g
+-- | `(gat_ty| ( $g:gat_ty ) ) => elabGATTy ctx TT g
 | `(gat_ty| U ) => return (TT, .const ``UU [], .const ``UU [])
 | `(gat_ty| $x:gat_tm ) => do
   let t ← elabClosedGATTm ctx TT x
@@ -213,9 +214,9 @@ partial def elabGATCon_core (ctx : Expr) (vars : varStruct) : Syntax → MetaM (
   return (newCtx, newVars)
 | `(con_inner| $d:gat_decl ) => do
   let (i,TT,T,resT) ← elabGATdecl ctx vars d
-  let newCtx ← mkAppM ``EXTEND #[ctx, T]
+  let newCtx ← mkAppM ``EXTEND #[ctx,T]
   let newVars := varExtend vars i ctx T newCtx TT.args resT
-  let res ← mkAppM ``EXTEND #[ctx, T]
+  let res ← mkAppM ``EXTEND #[ctx,T]
   return (res, newVars)
 -- | `(gat_con| include $g:ident as ( $is:ident_list ); $rest:gat_con ) => do
 --   let (newCon,newVars) ← elab_ident_list ctx (.const g.getId []) vars is
@@ -256,12 +257,12 @@ partial def elabGATCon : Syntax → MetaM Expr
 | `(con_outer| ⦃  ⦄ ) => do
   let emptyStrList ← mkListStrLit []
   let emptyLArgList ← mkListListArgLit []
-  mkAppM ``GAT.mk  #[.const ``EMPTY [],emptyStrList,emptyLArgList]
+  mkAppM ``GATdata.mk  #[.const ``EMPTY [],emptyStrList,emptyLArgList]
 | `(con_outer| ⦃ $s:con_inner  ⦄ ) => do
   let (resCon,VV) ← elabGATCon_core (.const ``EMPTY []) varEmpty s
   let topList ← mkListStrLit VV.topnames
   let telescopes ← mkListListArgLit VV.telescopes
-  mkAppM ``GAT.mk #[resCon,topList,telescopes]
+  mkAppM ``GATdata.mk #[resCon,topList,telescopes]
 | _ => throwError "ConFail"
 
 
diff --git a/GeneralizedAlgebra/signature.lean b/GeneralizedAlgebra/signature.lean
index c88217b..2b7e2cd 100644
--- a/GeneralizedAlgebra/signature.lean
+++ b/GeneralizedAlgebra/signature.lean
@@ -1,53 +1,270 @@
 import GeneralizedAlgebra.helper
 
-
 open Nat
 
 mutual
-  inductive Con : Type where
-  | EMPTY : Con
-  | EXTEND : Con → Ty → Con
-
-  inductive Subst : Type where
-  | EPSILON : Con → Subst
-  | ID : Con → Subst
-  | COMP : Subst → Subst → Subst
-  | PAIR : Subst → Tm → Subst
-  | PROJ1 : Subst → Subst
+  inductive Tm : Type where
+  | VAR : Nat → Tm
+  | APP : Tm → Ty → Tm → Tm → Tm
+  | TRANSP : Tm → Tm → Tm → Ty → Tm → Tm → Tm
 
   inductive Ty : Type where
-  | SUBST_Ty : Subst → Ty → Ty
   | UU : Ty
   | EL : Tm → Ty
   | PI : Tm → Ty → Ty
-  | EQ : Tm → Tm → Ty
+  | EQ : Tm → Tm → Tm → Ty
+end
+open Tm Ty
 
-  inductive Tm : Type where
-  | SUBST_Tm : Subst → Tm → Tm
-  | PROJ2 : Subst → Tm
-  | APP : Tm → Tm
+-- Written backwards!
+def Con : Type := List Ty
+instance : GetElem Con Nat Ty fun (Γ : Con) (i : Nat) => i < Γ.length := List.instGetElemNatLtLength
+def EXTEND (Γ : Con) (A : Ty) := A :: Γ
+def EMPTY : Con := []
+
+mutual
+  def WkArrTy : Ty → Nat → Ty
+  | UU, _ => UU
+  | EL X, a => EL (WkArrTm X a)
+  | PI X Y, a => PI (WkArrTm X a) (WkArrTy Y (succ a))
+  | EQ A t t', a => EQ (WkArrTm A a) (WkArrTm t a) (WkArrTm t' a)
+  def WkArrTm : Tm → Nat → Tm
+  | VAR n, a => if n ≥ a then VAR (succ n) else VAR n
+  | APP X Y f t, a => APP (WkArrTm X a) (WkArrTy Y (succ a)) (WkArrTm f a) (WkArrTm t a)
+  | TRANSP X s s' Y eq t, a => TRANSP (WkArrTm X a) (WkArrTm s a) (WkArrTm s' a) (WkArrTy Y a) (WkArrTm eq a) (WkArrTm t a)
+end
+
+def WknTy : (Γ : Con) → (n : Nat) → n < Γ.length → Ty
+| Γ,0,h => WkArrTy (Γ[0]'h) 0
+| _::Γ,succ n,h => WkArrTy (WknTy Γ n (lt_of_succ_lt_succ h)) 0
+
+mutual
+  def WkTy : Ty → Ty
+  | UU => UU
+  | EL X => EL (WkTm X)
+  | EQ A t t' => EQ (WkTm A) (WkTm t) (WkTm t')
+  | T =>  WkArrTy T 0
+  def WkTm : Tm →  Tm
+  | VAR n => VAR (succ n)
+  | TRANSP X s s' Y eq t => TRANSP (WkTm X) (WkTm s) (WkTm s') (WkTy Y) (WkTm eq) (WkTm t)
+  | t => WkArrTm t 0
+end
+
+inductive order where
+| LESS : order
+| EQUAL : order
+| GREATER : Nat → order
+open order
+def GRsucc : order → order
+| LESS => LESS
+| EQUAL => EQUAL
+| GREATER m => GREATER (succ m)
+
+def comparePred : Nat → Nat → order
+| 0, 0 => EQUAL
+| 0, succ _ => LESS
+| succ m, 0 => GREATER m
+| succ m, succ n => GRsucc $ comparePred m n
+
+mutual
+  def SubstArrTy : Ty → Tm → Nat → Ty
+  | UU, _,_ => UU
+  | EL X, z, a => EL (SubstArrTm X z a)
+  | PI X Y, z, a => PI (SubstArrTm X z a) (SubstArrTy Y z (succ a))
+  | EQ A t t', z, a => EQ (SubstArrTm A z a) (SubstArrTm t z a) (SubstArrTm t' z a)
+  def SubstArrTm : Tm → Tm → Nat → Tm
+  | VAR m, z, a =>
+    if m < a then VAR m else
+    if m = a then z
+             else VAR (pred m)
+  -- match comparePred m a with
+  --   | LESS => VAR m
+  --   | EQUAL => z
+  --   | GREATER m' => VAR m'
+  | APP X Y f t, z, a => APP (SubstArrTm X z a) (SubstArrTy Y z (succ a)) (SubstArrTm f z a) (SubstArrTm t z a)
+  | TRANSP X s s' Y eq t, z, a => TRANSP (SubstArrTm X z a) (SubstArrTm s z a) (SubstArrTm s' z a) (SubstArrTy Y z (succ a)) (SubstArrTm eq z a) (SubstArrTm t z a)
 end
 
-open Con Subst Ty Tm
+-- def varElim {motive : Tm → Type} (m : Nat) (z : Tm) (mL : motive (VAR m)) (mE : motive z) (mG : (m' : Nat) → motive (VAR m')) (a : Nat) : motive (SubstArrTm (VAR m) z a) :=
+-- by
+--     cases (comparePred m a)
+--     dsimp[SubstArrTm]
+--     sorry
+--     sorry
+--     sorry
+
+
+
+def substAt : (Γ : Con) → (z : Tm) → (a : Nat) → (a < Γ.length) → Con
+| _::Γ,_,0,_ => Γ
+| A::Γ,z,succ a,h => SubstArrTy A z (a) :: substAt Γ z a (lt_of_succ_lt_succ h)
+
+def trunc : (Γ : Con) → (a : Nat) → (a < Γ.length) → Con
+| _::Γ,succ a',h => trunc Γ a' (lt_of_succ_lt_succ h)
+| _::Γ,0,_ => Γ
+
+def SubstTy := λ T t => SubstArrTy T t 0
+def SubstTm := λ t t' => SubstArrTm t t' 0
+
+-- mutual
+--   inductive goodCon : Con → Type where
+--   | goodNil : goodCon []
+--   | goodCons : ∀ {Γ : Con}{A : Ty}, goodTy Γ A → goodCon Γ → goodCon (A::Γ)
+
+--   inductive goodTy : Con → Ty → Type where
+--   | goodUU : ∀ {Γ : Con}, goodTy Γ UU
+--   | goodEL : ∀ {Γ : Con}{X : Tm}, goodTm Γ UU X → goodTy Γ (EL X)
+--   | goodPI : ∀ {Γ : Con}{X : Tm}{Y : Ty}, goodTm Γ UU X → goodTy (EL X::Γ) Y → goodTy Γ (PI X Y)
+--   | goodEQ : ∀ {Γ : Con}{X : Tm}{t t' : Tm}, goodTm Γ UU X → goodTm Γ (EL X) t → goodTm Γ (EL X) t' → goodTy Γ (EQ X t t')
+
+--   inductive goodTm : Con → Ty → Tm → Type where
+--   -- | goodVAR : ∀ {Γ : Con}(n : Nat), (h : n < Γ.length) → goodTm Γ (WknTy Γ n h) (VAR n)
+--   | goodVAR0 : ∀ {Γ : Con}{A : Ty}, goodTy Γ A → goodTm (A::Γ) (WkTy A) (VAR 0)
+--   | goodSUCC : ∀ {Γ : Con}{A : Ty}{B : Ty}{m : Nat}, goodTy Γ A → goodTm Γ A (VAR m) → goodTm (B::Γ) (WkTy A) (VAR (succ m))
+--   | goodAPP : ∀ {Γ : Con}{X : Tm}{Y : Ty}{f t : Tm}, goodTm Γ UU X → goodTy (EL X::Γ) Y → goodTm Γ (PI X Y) f → goodTm Γ (EL X) t → goodTm Γ (SubstTy Y t) (APP X Y f t)
+--   | goodTRANSP : ∀ {Γ : Con}{X : Tm}{s s' : Tm}{Y : Ty}{eq t : Tm},
+--       goodTm Γ UU X → goodTm Γ (EL X) s → goodTm Γ (EL X) s' → goodTy (EL X::Γ) Y → goodTm Γ (EQ X s s') eq → goodTm Γ (SubstTy Y s) t → goodTm Γ (SubstTy Y s') (TRANSP X s s' Y eq t)
+-- end
+
+
+-- open goodTm goodTy goodCon
 
+theorem UU_stable : UU = WkTy UU := Eq.refl _
 
-infixl:10 " ▷ " => EXTEND
-notation t " [ " σ " ]t " => SUBST_Tm σ t
+-- def good_Set : goodCon [UU] := by
+--   apply goodCons
+--   exact goodUU
+--   exact goodNil
 
-def len : Con → Nat
-| EMPTY => 0
-| Γ ▷ _ => succ (len Γ)
+-- def good_pointed : goodCon [EL (VAR 0),UU] := by
+--   apply goodCons
+--   apply goodEL
+--   apply goodVAR0
+--   apply goodUU
+--   exact good_Set
 
-def deBruijn : Tm → Option Nat
-| PROJ2 (ID _) => some 0
-| t [ PROJ1 (ID _) ]t => do let res ← deBruijn t; return (succ res)
-| _ => none
+-- def good_nat : goodCon [PI (VAR 1) (EL (VAR 2)),EL (VAR 0),UU] := by
+--   apply goodCons
+--   apply goodPI
+--   rw [UU_stable]
+--   apply goodSUCC
+--   apply goodUU
+--   rw [←UU_stable]
+--   apply goodVAR0
+--   apply goodUU
+--   apply goodEL
+--   rw [UU_stable]
+--   apply goodSUCC
+--   apply goodUU
+--   rw [UU_stable]
+--   apply goodSUCC
+--   apply goodUU
+--   rw [←UU_stable]
+--   rw [←UU_stable]
+--   apply goodVAR0
+--   apply goodUU
+--   exact good_pointed
 
-def wk (Γ : Con) (A : Ty) : Subst := PROJ1 (@ID (Γ ▷ A))
-def V0 (Γ : Con) (T0 : Ty) : Tm := PROJ2 (@ID (Γ ▷ T0))
 
 
--- namespace GAT
+
+
+-- mutual
+--   -- def SubstArrTy : Ty → Tm → Nat → Ty
+--   -- def SubstArrTm : Tm → Tm → Nat → Tm
+--   -- def WkArrTy : Ty → Nat → Ty
+--   -- | UU, _ => UU
+--   -- | EL X, a => EL (WkArrTm X a)
+--   -- | PI X Y, a => PI (WkArrTm X a) (WkArrTy Y (succ a))
+--   -- | EQ A t t', a => EQ (WkArrTm A a) (WkArrTm t a) (WkArrTm t' a)
+--   -- def WkArrTm : Tm → Nat → Tm
+--   -- | VAR n, a => if n ≥ a then VAR (succ n) else VAR n
+--   -- | APP X Y f t, a => APP (WkArrTm X a) (WkArrTy Y (succ a)) (WkArrTm f a) (WkArrTm t a)
+--   -- | TRANSP X s s' Y eq t, a => TRANSP (WkArrTm X a) (WkArrTm s a) (WkArrTm s' a) (WkArrTy Y a) (WkArrTm eq a) (WkArrTm t a)
+--   -- def goodWkArrTy {Γ : Con} : (A : Ty) → (a : Nat) → (h : a < Γ.length) → goodTy Γ A →
+
+--   -- def goodUntrunc {Γ : Con} (A : Ty) (z : Tm) : (a : Nat) → (h : a < Γ.length) → goodTm (trunc Γ a h) (Γ[a]'h) z → goodTm Γ (WknTy )
+
+--   def goodSubstArrTy  {Γ : Con} : (A : Ty) → (z : Tm) → (a : Nat) → (h : a < Γ.length) → goodTy Γ A → goodTm (trunc Γ a h) (Γ[a]'h) z → goodTy (substAt Γ z a h) (SubstArrTy A z a)
+--   | UU, _,_,_,_,_ => goodUU
+--   | EL X,z,a,h,goodEL gX,gz => goodEL (goodSubstArrTm X z a h goodUU gX gz)
+--   | EQ X t t',z,a,h,goodEQ gX gt gt',gz => goodEQ (goodSubstArrTm X z a h goodUU gX gz) (goodSubstArrTm t z a h (goodEL gX) gt gz) (goodSubstArrTm t' z a h (goodEL gX) gt' gz)
+--   | PI X Y, z,a,h,goodPI gX gY,gz => goodPI (goodSubstArrTm X z a h goodUU gX gz) (@goodSubstArrTy (EL X :: Γ) Y z (succ a) (succ_lt_succ h) gY gz)
+
+--   def goodSubstArrTm {Γ : Con}{A : Ty} : (t : Tm) → (z : Tm) → (a : Nat) → (h : a < Γ.length) → goodTy Γ A → goodTm Γ A t → goodTm (trunc Γ a h) (Γ[a]'h) z → goodTm (substAt Γ z a h) (SubstArrTy A z a) (SubstArrTm t z a)
+--   | APP X Y f t, z, a, h, _ , goodAPP gX gY gf gt,gz =>
+--         goodSubstArrTm _ _ _ _ (@goodSubstArrTy (EL X::Γ) Y t 0 (zero_lt_succ Γ.length) gY gt) (goodAPP gX gY gf gt) gz
+--   | TRANSP X s s' Y eq t, z, a, h, _, goodTRANSP gX gs gs' gY geq gt,gz =>
+--         goodSubstArrTm _ _ _ _ (@goodSubstArrTy (EL X::Γ) Y s' 0 (zero_lt_succ Γ.length) gY gs') (goodTRANSP gX gs gs' gY geq gt) gz
+--   | VAR m, z, a, h, gw, gv,gz =>
+--     if m < a then _ else
+--     if m = a then _ else
+--     _
+-- end
+
+-- def goodSubst {Γ : Con}{X : Tm}{s : Tm}{Y : Ty} (gs : goodTm Γ (EL X) s) (gY : goodTy (EL X::Γ) Y) : goodTy Γ (SubstTy Y s) :=
+--         @goodSubstArrTy (EL X :: Γ) Y s 0 (zero_lt_succ Γ.length) gY gs
+
+-- def extractGoodVar {Γ : Con}{A : Ty}{n : Nat} : goodTm Γ A (VAR n) →
+--   ∃ (h : n < Γ.length), A = WknTy Γ n h := sorry
+universe u v w
+
+structure indData where
+    (Con_D : Con → Type u)
+    (Ty_D : (Γ : Con) → Con_D Γ → Ty → Type v)
+    (Tm_D : (Γ : Con) → (Γ_D : Con_D Γ) → (A : Ty) → Ty_D Γ Γ_D A → Tm → Type w)
+    (nil_D : Con_D [])
+    (cons_D : (Γ : Con) → (Γ_D : Con_D Γ) → (A : Ty) → (A_D : Ty_D Γ Γ_D A) → Con_D (A::Γ))
+    -- (WkTy_D : (Γ : Con) → (Γ_D : Con_D Γ) →
+    --           (A : Ty) → (A_D : Ty_D Γ Γ_D A) →
+    --           (A' : Ty) → (A'_D : Ty_D Γ Γ_D A') →
+    --           Ty_D (A'::Γ) (cons_D Γ Γ_D A' A'_D) (WkTy A))
+    (UU_D : (Γ : Con) → (Γ_D : Con_D Γ) → Ty_D Γ Γ_D UU)
+    (EL_D : (Γ : Con) → (Γ_D : Con_D Γ) →
+            (X : Tm) → Tm_D Γ Γ_D UU (UU_D Γ Γ_D) X →
+            Ty_D Γ Γ_D (EL X))
+    (PI_D : (Γ : Con) → (Γ_D : Con_D Γ) →
+            (X : Tm) → (X_D : Tm_D Γ Γ_D UU (UU_D Γ Γ_D) X) →
+            (Y : Ty) → Ty_D (EL X :: Γ) (cons_D Γ Γ_D (EL X) (EL_D Γ Γ_D X X_D)) Y →
+            Ty_D Γ Γ_D (PI X Y))
+    (EQ_D : (Γ : Con) → (Γ_D : Con_D Γ) →
+            (X : Tm) → (X_D : Tm_D Γ Γ_D UU (UU_D Γ Γ_D) X) →
+            (s : Tm) → (s_D : Tm_D Γ Γ_D (EL X) (EL_D Γ Γ_D X X_D) s) →
+            (s' : Tm) → (s'_D : Tm_D Γ Γ_D (EL X) (EL_D Γ Γ_D X X_D) s') →
+            Ty_D Γ Γ_D (EQ X s s'))
+    -- (VAR_D :(Γ : Con) → (Γ_D : Con_D Γ) →
+    --         (n : Nat) → (h : n < List.length Γ) →
+    --         (A_D : Ty_D Γ Γ_D (WknTy Γ n h)) →
+    --         Tm_D Γ Γ_D (WknTy Γ n h) A_D (VAR n))
+    (VAR0_D : (Γ : Con) → (Γ_D : Con_D Γ) →
+            (A : Ty) → (A_D : Ty_D Γ Γ_D A) → (A'_D : Ty_D (A::Γ) (cons_D Γ Γ_D A A_D) (WkTy A)) →
+            Tm_D (A::Γ) (cons_D Γ Γ_D A A_D) (WkTy A) A'_D (VAR 0)
+            )
+    (VARSUCC_D : (Γ : Con) → (Γ_D : Con_D Γ) →
+            (A : Ty) → (A_D : Ty_D Γ Γ_D A) →
+            (t : Tm) → Tm_D Γ Γ_D A A_D t →
+            (A' : Ty) → (A'_D : Ty_D Γ Γ_D A') →
+            (WkA_D : Ty_D (A'::Γ) (cons_D Γ Γ_D A' A'_D) (WkTy A)) →
+            Tm_D (A'::Γ) (cons_D Γ Γ_D A' A'_D) (WkTy A) WkA_D (WkTm t))
+    (APP_D :(Γ : Con) → (Γ_D : Con_D Γ) →
+            (X : Tm) → (X_D : Tm_D Γ Γ_D UU (UU_D Γ Γ_D) X) →
+            (Y : Ty) → (Y_D : Ty_D (EL X :: Γ) (cons_D Γ Γ_D (EL X) (EL_D Γ Γ_D X X_D)) Y) →
+            (f : Tm) → (f_D : Tm_D Γ Γ_D (PI X Y) (PI_D Γ Γ_D X X_D Y Y_D) f) →
+            (t : Tm) → (t_D : Tm_D Γ Γ_D (EL X) (EL_D Γ Γ_D X X_D) t) →
+            (Yt_D : Ty_D Γ Γ_D (SubstTy Y t)) →
+            Tm_D Γ Γ_D (SubstTy Y t) Yt_D (APP X Y f t))
+    (TRANSP_D :(Γ : Con) → (Γ_D : Con_D Γ) →
+            (X : Tm) → (X_D : Tm_D Γ Γ_D UU (UU_D Γ Γ_D) X) →
+            (s : Tm) → (s_D : Tm_D Γ Γ_D (EL X) (EL_D Γ Γ_D X X_D) s) →
+            (s' : Tm) → (s'_D : Tm_D Γ Γ_D (EL X) (EL_D Γ Γ_D X X_D) s') →
+            (Y : Ty) → (Y_D : Ty_D (EL X :: Γ) (cons_D Γ Γ_D (EL X) (EL_D Γ Γ_D X X_D)) Y) →
+            (Ys_D : Ty_D Γ Γ_D (SubstTy Y s)) → (Ys'_D : Ty_D Γ Γ_D (SubstTy Y s')) →
+            (p : Tm) → (p_D : Tm_D Γ Γ_D (EQ X s s') (EQ_D Γ Γ_D X X_D s s_D s' s'_D) p) →
+            (k : Tm) → Tm_D Γ Γ_D (SubstTy Y s) Ys_D k →
+            Tm_D Γ Γ_D (SubstTy Y s') Ys'_D (TRANSP X s s' Y eq k))
+
+
+-- def VAR0_D {P : indData}
 
 inductive Arg : Type where
 | Impl : String → Ty → Arg
@@ -60,17 +277,94 @@ def getName : Arg → Option String
 | Expl i _ => some i
 | Anon _ => none
 
-structure GAT where
+mutual
+def Tmrepr : Tm → String
+| APP X Y f t => "APP (" ++ (Tmrepr X) ++ ") (" ++ (Tyrepr Y) ++ ") (" ++ (Tmrepr f) ++ ") (" ++ (Tmrepr t) ++ ")"
+| VAR n => Nat.repr n
+| TRANSP X s s' Y eq t => "transp " ++ (Tmrepr eq) ++ " " ++ (Tmrepr t)
+
+def Tyrepr : Ty → String
+| UU => "U"
+| EQ X s t => "Eq " ++ (Tmrepr X) ++ " " ++ (Tmrepr s)  ++ " " ++ (Tmrepr t)
+| EL X => "El (" ++ (Tmrepr X) ++ ")"
+| PI X Y => "Π (" ++ (Tmrepr X) ++ ") (" ++ (Tyrepr Y) ++ ")"
+end
+
+def Argrepr : Arg → String
+| Impl i T => "iArg(" ++ i ++ "," ++ Tyrepr T ++ ")"
+| Expl i T => "eArg(" ++ i ++ "," ++ Tyrepr T ++ ")"
+| Anon T =>  "aArg(" ++ Tyrepr T ++ ")"
+
+instance : Repr Tm where
+  reprPrec := λ t _ => Tmrepr t
+instance : Repr Ty where
+  reprPrec := λ t _ => Tyrepr t
+instance : Repr Arg where
+  reprPrec := λ A _ => Argrepr A
+
+structure GATdata where
   (con : Con)
   (topnames : List String)
   (telescopes : List (List Arg × Ty))
 
+structure GAT extends GATdata where
+  (elim : (P : indData) → P.Con_D con)
+
 -- #check Listappend
 def GAT.subnames (𝔊 : GAT) : List String :=
   List.join $
   List.map (λ (L,s) => L ++ [s]) $
   List.zip
-    (List.map ((mappartial getName) ∘ Prod.fst) (GAT.telescopes 𝔊))
-    (GAT.topnames 𝔊)
+    (List.map ((mappartial getName) ∘ Prod.fst) (𝔊.telescopes))
+    (𝔊.topnames)
+
+-- mutual
+--     def elim (P : indData) : (Γ : Con) → goodCon Γ → P.Con_D Γ
+--     | [],_ => P.nil_D
+--     | A::Γ,goodCons gA gΓ => P.cons_D _ (elim _ _ gΓ) _ (elimTy _ _ _ _ gΓ gA)
+
+--     -- def dispGetElem (P : indData) (Γ : Con) (n : Nat) (h : n < List.length Γ) :
+--     --     Σ (Γ_D : P.Con_D Γ), P.Ty_D Γ Γ_D (WknTy Γ n h) :=  ⟨elim _ _,elimTy _ _ _ _ _⟩
+
+--     -- def dispWknTy : (P : indData) →
+--     --     (Γ : Con) → (Γ_D : P.Con_D Γ) →
+--     --     (A : Ty) → (A_D : P.Ty_D Γ Γ_D A) →
+--     --     (n : Nat) → (h : n < List.length Γ) →
+--     --     P.Ty_D Γ Γ_D (WknTy Γ n h) →
+--     --     P.Ty_D (A::Γ) (P.cons_D _ Γ_D _ A_D) (WknTy (A::Γ) (succ n) (succ_lt_succ h)) := _
+--     def elimWknTy {P : indData} : (Γ : Con) → (Γ_D : P.Con_D Γ) → (n : Nat) → (h : n < Γ.length) → P.Ty_D Γ Γ_D (WknTy Γ n h)
+--     | A::Γ , _ , 0 , _ => _
+
+--     def elimTy (P : indData) (Γ : Con) (Γ_D : P.Con_D Γ) : (A : Ty) → goodCon Γ → goodTy Γ A → P.Ty_D Γ Γ_D A
+--     | UU,_,goodUU => P.UU_D Γ Γ_D
+--     | EL X,gΓ,goodEL gX => P.EL_D _ _ _ (elimTm _ _ _ _ _ _ gΓ goodUU gX)
+--     | PI X Y,gΓ,goodPI gX gY => P.PI_D _ _ _ (elimTm _ _ _ _ _ _ gΓ goodUU gX) _ (elimTy _ _ _ _ (goodCons (goodEL gX) gΓ) gY)
+--     | EQ X s s',gΓ,goodEQ gX gs gs' => P.EQ_D _ _ _ (elimTm _ _ _ _ _ _ gΓ goodUU gX) _ (elimTm _ _ _ _ _ _ gΓ (goodEL gX) gs) _ (elimTm _ _ _ _ _ _ gΓ (goodEL gX) gs')
+
+--     def elimTm (P : indData) (Γ : Con) (Γ_D : P.Con_D Γ) : (A : Ty) → (A_D : P.Ty_D Γ Γ_D A) → (t : Tm) → goodCon Γ → goodTy Γ A → goodTm Γ A t → P.Tm_D Γ Γ_D A A_D t
+--     | _,_,APP X Y f t,gΓ,_, @goodAPP _ _ _ _ _ gX gY gf gt => P.APP_D Γ Γ_D X (elimTm _ _ _ _ _ _ gΓ goodUU gX) _ (elimTy _ _ _ _ (goodCons (goodEL gX) gΓ) gY) _ (elimTm _ _ _ _ _ _ gΓ (goodPI gX gY) gf) _ (elimTm _ _ _ _ _ _ gΓ (goodEL gX) gt) _
+--     | _,_,TRANSP X s s' Y eq k,gΓ,_,goodTRANSP gX gs gs' gY geq gk => P.TRANSP_D Γ Γ_D _ (elimTm _ _ _ _ _ _ gΓ goodUU gX) _ (elimTm _ _ _ _ _ _ gΓ (goodEL gX) gs) _ (elimTm _ _ _ _ _ _ gΓ (goodEL gX) gs') _ (elimTy _ _ _ _ (goodCons (goodEL gX) gΓ) gY) (elimTy _ _ _ _ gΓ (goodSubst gs gY)) _ _ (elimTm _ _ _ _ _ _ gΓ (goodEQ gX gs gs') geq) _ (elimTm _ _ _ _ (elimTy _ _ _ _ _ _) _ gΓ (goodSubst gs gY) gk)
+--     | A,_,VAR n, gΓ,gA, gv => by
+--         let hh := @extractGoodVar _ _ _ gv
+--         let h := hh.1
+--         let p : A = WknTy Γ n h := hh.2
+--         rw [p]
+
+--         -- rw p
+
+--       -- P.VAR_D Γ Γ_D n h (elimWknTy Γ Γ_D n h)
+-- end
+
+-- def x := @APP P''' (SUCC $ SUCC ZERO) UU (SUCC ZERO) (ZERO)
+-- def Q := P'' ▷ PI (SUCC ZERO) (@EL P''' (@APP P''' _ _ _ _))
+-- #reduce P'''
 
--- end GAT
+-- #eval len
+--     ⋄ ▷ UU ▷ PI ZERO UU
+    -- ▷ PI (SUCC ZERO) (EL (@APP P''' (SUCC $ SUCC ZERO) UU (SUCC ZERO) (ZERO)))
+    --▷ (PI (SUCC ZERO) (EL (APP (SUCC ZERO) _ )))
+    -- ▷ (PI ZERO (PI (SUCC ZERO) (EL $ SUCC $ SUCC $ ZERO)))
+    -- ▷ (PI (SUCC ZERO) (EQ (SUCC $ SUCC ZERO) (APP (SUCC $ ZERO) (APP _ _)) ZERO))
+    -- ▷ (EL $ SUCC $ ZERO)
+    -- ▷ (PI (SUCC $ SUCC $ ZERO) (EQ (SUCC $ SUCC $ SUCC $ ZERO) ZERO (APP (APP (_) ZERO) (SUCC ZERO))))
+-- notation t " [ " σ " ]t " => SUBST_Tm σ t
diff --git a/GeneralizedAlgebra/signatures/bipointed.lean b/GeneralizedAlgebra/signatures/bipointed.lean
index ca6378b..6806132 100644
--- a/GeneralizedAlgebra/signatures/bipointed.lean
+++ b/GeneralizedAlgebra/signatures/bipointed.lean
@@ -1,3 +1,8 @@
-import GeneralizedAlgebra.nouGAT
+import GeneralizedAlgebra.signatures.pointed
 
-def 𝔅 : GAT := ⦃ X : U, x : X, x' : X ⦄
+#check indData.VARSUCC_D
+def 𝔅 : GAT := ⟨
+  ⦃ X : U, x : X, x' : X ⦄,
+  λ P => P.cons_D _ (𝔓.elim P) _ (P.EL_D _ _ _ (P.VARSUCC_D _ _ Ty.UU (P.UU_D _ _) (Tm.VAR 0) (P.VAR0_D _ _ _ _ _) _ _ _))
+  ⟩
+--
diff --git a/GeneralizedAlgebra/signatures/nat.lean b/GeneralizedAlgebra/signatures/nat.lean
index b265e4e..63f8b8a 100644
--- a/GeneralizedAlgebra/signatures/nat.lean
+++ b/GeneralizedAlgebra/signatures/nat.lean
@@ -1,7 +1,10 @@
-import GeneralizedAlgebra.nouGAT
+import GeneralizedAlgebra.signatures.pointed
 
-def 𝔑 : GAT := ⦃
+def 𝔑 : GAT := ⟨
+⦃
     Nat   : U,
     zero  : Nat,
     succ  : Nat ⇒ Nat
-⦄
+⦄,
+λ P => P.cons_D _ (𝔓.elim P) _ (P.PI_D _ _ _ (P.VARSUCC_D _ _ Ty.UU (P.UU_D _ _) (Tm.VAR 0) (P.VAR0_D _ _ _ _ _) _ _ _) _ (P.EL_D _ _ _ (P.VARSUCC_D _ _ Ty.UU (P.UU_D _ _) _ (P.VARSUCC_D _ _ Ty.UU (P.UU_D _ _) _ (P.VAR0_D _ _ _ _ _) _ _ _) _ _ _)))
+⟩
diff --git a/GeneralizedAlgebra/signatures/pointed.lean b/GeneralizedAlgebra/signatures/pointed.lean
index 3110289..1cfee01 100644
--- a/GeneralizedAlgebra/signatures/pointed.lean
+++ b/GeneralizedAlgebra/signatures/pointed.lean
@@ -1,4 +1,30 @@
-import GeneralizedAlgebra.nouGAT
+import GeneralizedAlgebra.signatures.set
 
-def 𝔓 : GAT := ⦃ X : U, x : X
-⦄
+
+-- def pointedLemma (P : indData) :
+--   P.Tm_D
+--     [Ty.UU]
+--     (P.cons_D [] P.nil_D Ty.UU (P.UU_D [] P.nil_D))
+--     (Ty.EL (Tm.VAR 0))
+--     (P.EL_D [Ty.UU] (P.cons_D [] P.nil_D Ty.UU (P.UU_D [] P.nil_D)) (Tm.VAR 0) (P.VAR0_D [] P.nil_D Ty.UU (P.UU_D [] P.nil_D) (P.UU_D [Ty.UU] (P.cons_D [] P.nil_D Ty.UU (P.UU_D [] P.nil_D)))))
+--     (Tm.VAR 0)
+--   := by
+
+--     have helper := P.VAR0_D EMPTY P.nil_D Ty.UU (P.UU_D _ _) (P.UU_D _ _)
+--     -- rw [WkTy] at helper
+--     sorry
+
+
+
+def 𝔓 : GAT := ⟨
+  ⦃ X : U, x : X ⦄,
+  λ P => P.cons_D _ (𝔖𝔢𝔱.elim P) _ (P.EL_D _ _ _ (P.VAR0_D _ _ _ _ _))
+  -- by
+  --   intro P
+  --   apply P.cons_D
+  --   apply P.EL_D
+  --   have helper := P.VAR0_D EMPTY P.nil_D Ty.UU (P.UU_D _ _)
+  --   rw [WkTy] at helper
+  --   apply helper
+  ⟩
+-- #reduce 𝔓.elim
diff --git a/GeneralizedAlgebra/signatures/quiver.lean b/GeneralizedAlgebra/signatures/quiver.lean
index 36b862d..cbfa2b9 100644
--- a/GeneralizedAlgebra/signatures/quiver.lean
+++ b/GeneralizedAlgebra/signatures/quiver.lean
@@ -1,6 +1,8 @@
-import GeneralizedAlgebra.nouGAT
+import GeneralizedAlgebra.signatures.set
 
-def 𝔔𝔲𝔦𝔳 : GAT := ⦃
+def 𝔔𝔲𝔦𝔳 : GAT := ⟨ ⦃
     V : U,
     E : V ⇒ V ⇒ U
-⦄
+⦄,
+λ P => P.cons_D _ (𝔖𝔢𝔱.elim P) _ (P.PI_D _ _ _ (P.VAR0_D _ _ _ _ _) _ (P.PI_D _ _ _ (P.VARSUCC_D _ _ Ty.UU (P.UU_D _ _) _ (P.VAR0_D _ _ _ _ _) _ _ _) _ (P.UU_D _ _)))
+⟩
diff --git a/GeneralizedAlgebra/signatures/refl_quiver.lean b/GeneralizedAlgebra/signatures/refl_quiver.lean
index 4d97944..6a29faa 100644
--- a/GeneralizedAlgebra/signatures/refl_quiver.lean
+++ b/GeneralizedAlgebra/signatures/refl_quiver.lean
@@ -1,7 +1,17 @@
-import GeneralizedAlgebra.nouGAT
+import GeneralizedAlgebra.signatures.quiver
 
-def 𝔯𝔔𝔲𝔦𝔳 : GAT := ⦃
+-- def 𝔯𝔔𝔲𝔦𝔳 : GAT := ⟨ ⦃
+--     V : U,
+--     E : V ⇒ V ⇒ U,
+--     r : (v : V) ⇒ E v v
+-- ⦄,
+-- λ P => _
+-- ⟩
+
+def foo := ⦃
     V : U,
-    E : V ⇒ V ⇒ U,
-    r : (v : V) ⇒ E v v
+    E : V ⇒ U,
+    r : (v : V) ⇒ E v
 ⦄
+
+#eval foo.telescopes
diff --git a/GeneralizedAlgebra/signatures/set.lean b/GeneralizedAlgebra/signatures/set.lean
index 9783762..dd9055c 100644
--- a/GeneralizedAlgebra/signatures/set.lean
+++ b/GeneralizedAlgebra/signatures/set.lean
@@ -1,3 +1,11 @@
 import GeneralizedAlgebra.nouGAT
 
-def 𝔖𝔢𝔱 : GAT := ⦃ X : U ⦄
+def 𝔖𝔢𝔱 : GAT := ⟨
+  ⦃ X : U ⦄,
+
+  by
+    intro P
+    apply P.cons_D
+    apply P.UU_D
+    apply P.nil_D
+  ⟩