namespace http://cds.omdoc.org/examples❚

//   theory ObjectLevelInstances : http://cds.omdoc.org/urtheories?LF =
  tp    : type❙
  tm    : type❙
  equal : tm ⟶ tm ⟶ tm  ❘# 1 = 2❙
  of    : tm ⟶ tp ⟶ type❘# 1 # 2❙

  const : tp ⟶ THY❘ = [a] {|
    c  : tm,
    of : c # a
  |}❙
  
  nat  : tp❙
  zero : const nat❙
  
  // alsozero : const nat ❘= [|c : zero/c, of : zero/of|]❙
❚

//  theory MetaLevelInstances : http://cds.omdoc.org/urtheories?LF =
  tp    : type❙
  tm    : type❙
  equal : tm ⟶ tm ⟶ tm  ❘# 1 = 2❙
  of    : tm ⟶ tp ⟶ type❘# 1 # 2❙

  theory const > {|a: tp|}❘ =
    c  : tm❙
    of : c # a❙
  ❚

//  nat : tp❙
  // structure zero : const nat❙
  
  // alsozero : const nat ❘= [|c : zero/c, of : zero/of|]❙
❚