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

//   polymorphic equality (essentially identity types) ❚
theory Equality : http://cds.omdoc.org/urtheories?PLF =
  equal : {a:type} a ⟶ a ⟶ type❘# 2 = 3 prec 50❙
  refl  : {a,x:a} x = x   ❘# refl 2❙
  cong  : {a,b,x,y} x = y ⟶ {f: a ⟶ b} (f x) = (f y)❘# cong 5 6❙
  cast  : {a: type, A: a ⟶ type, x:a, y:a} x = y ⟶ A x ⟶ A y❙

  sym   : {a,x:a,y} x = y ⟶ y = x❘
        = [a,x,y][p] cast a ([u] u = x) x y p (refl x)❙
  trans : {a,x:a,y,z} x = y ⟶ y = z ⟶ x = z❘
        = [a,x,y,z,p,q] cast a ([u] x = u) y z q p❙
❚

//   polymorphic lists ❚
 theory Lists : http://cds.omdoc.org/urtheories?PLF =
  include ?Equality❙
  list  : type ⟶ type❙
  nil   : {a} list a❘ # nil %I1❙
  cons  : {a} a ⟶ list a ⟶ list a❘ # 2 , 3 prec 75❙

  append : {a} list a ⟶ list a ⟶ list a❘ # 2 + 3 prec 75❙
  append_nil  : {a, m: list a} nil + m = m❙
  append_cons : {a, x: a, l: list a, m: list a} (x, l) + m = x , (l + m)❙
❚