identity_type.m31

require eq ;;

rule Id (A type) (a : A) (b : A) type
;;

rule refl (A type) (a : A) : Id A a a
;;

rule J
  (A type)
  ({x y : A} {p : Id A x y} C type)
  ({x : A} c : C{x, x, refl A x})
  (a : A)
  (b : A)
  (q : Id A a b)
  : C{a, b, q}
;;

rule J_β
  (A type)
  ({x y : A} {p : Id A x y} C type)
  ({x : A} c : C{x, x, refl A x})
  (a : A)
  : J A C c a a (refl A a) ≡ c{a} : C{a, a, refl A a}
;;

eq.add_rule J_β
;;