In languages such as Agda, Idris, or Haskell with type extensions, there is a = type sort of like the following
data a :~: b where
Refl :: a :~: a
a :~: b means that a and b are the same.
Can such a type be defined in the calculus of constructions or Morte (which is programming language based on the calculus of construction)?
id : \/a : *. a -> a
id = \a : *. \x : a. x
eqn : \/a : *. a -> a -> *
eqn = \a : *. \x : a. \y : a. \/p : (a -> *). p x -> p y
refl : \/a : *. \/x : a. eqn a x x
refl = \a : *. \x : a. \p : (a -> *). id (p x)
where \/ is the pi-constructor and \is the lambda-constructor.
I think that the idea of Church-Scott Encoding is to define a type as its elimination rule and its constructors as its introduction rules.
either is a good example:
either : * -> * -> *
either = \a : *. \b : *. \/r : *. (a -> r) -> (b -> r) -> r
left : \/a : *. \/b : *. a -> either a b
left = \a : *. \b : *. \x : a. \r : *. \left1 : (a -> r). \right1 : (b -> r). left1 x
right : \/a : *. \/b : *. b -> either a b
right = \a : *. \b : *. \y : b. \r : *. \left1 : (a -> r). \right1 : (b -> r). right1 y
either is defined as the elimination rule of disjunction.
By this idea, eqn a x y must be defined as the liebniz rule \/p : (a -> *). p x -> p y, because the elimination rule of equation is the liebniz rule.
+) a proof of 1 != 0:
bottom : *
bottom = \/r : *. r
nat : *
nat = \/r : *. r -> (r -> r) -> r
zero : nat
zero = \r : *. \z : r. \s : (r -> r). z
succ : nat -> nat
succ = \n : nat. \r : *. \z : r. \s : (r -> r). s (n r z s)
id : \/a : *. a -> a
id = \a : *. \x : a. x
eqn : \/a : *. a -> a -> *
eqn = \a : *. \x : a. \y : a. \/p : (a -> *). p x -> p y
refl : \/a : *. \/x : a. eqn a x x
refl = \a : *. \x : a. \p : (a -> *). id (p x)
goal : eqn nat (succ zero) zero -> bottom
goal = \one_is_zero : (\/p : (nat -> *). p (succ zero) -> p zero). \r : *. one_is_zero (\n : nat. n * r (\a : *. r -> a)) (id r)