namespace http://cds.omdoc.org/examples❚
theory DepSumChurch : http://cds.omdoc.org/urtheories?LF =
tp : type ❙
tm : tp ⟶ type ❘ # tm 1 prec -5❙
equal : {A} tm A ⟶ tm A ⟶ type ❘ # 2 = 3 ❘ role Eq❙
Sigma : {A} (tm A ⟶ tp) ⟶ tp ❘ # Σ 2 ❙
pair : {A, B: tm A ⟶ tp} {x} tm (B x) ⟶ tm Σ [x] B x ❘ # pair 3 4❙
pi1 : {A, B: tm A ⟶ tp} tm (Σ [x] B x) ⟶ tm A ❘ # pi1 3 ❙
pi2 : {A, B: tm A ⟶ tp} {u:tm (Σ [x] B x)} tm (B (pi1 u)) ❘ # pi2 3 ❙
prod : tp ⟶ tp ⟶ tp ❘
= [A,B] Σ [x: tm A] B ❘
# 1 × 2 prec 3❙
conv_pair : {A, B: tm A ⟶ tp, u: tm Σ [x] B x} u = pair (pi1 u) (pi2 u) ❙
conv_pi1 : {A, B: tm A ⟶ tp, X, Y: tm (B X)} pi1 (pair A B X Y) = X ❘ role Simplify ❙
// Note that conv_pi2 only type-checks because conv_pi1 is used as a simplification rule. ❙
conv_pi2 : {A, B: tm A ⟶ tp, X, Y: tm (B X)} pi2 (pair A B X Y) = Y ❘ role Simplify❙
❚
theory DepSumLF : http://cds.omdoc.org/urtheories?DHOL =
Sigma : {A:type} (A ⟶ type) ⟶ type ❘ # Σ 2 ❙
pair : {A : type, B: A ⟶ type, a : A } B a ⟶ Σ B ❘ # pair 3 4 ❙
pi1 : {A : type, B: A ⟶ type} Σ B ⟶ A ❘ # pi1 3 ❙
pi2 : {A : type, B: A ⟶ type} {p : Σ B} B (pi1 p) ❘ # pi2 3❙
conv_pair : {A: type, B: A ⟶ type, u: Σ B} DED u EQ (pair (pi1 u) (pi2 u)) ❙
conv_pi1 : {A : type, B: A ⟶ type}{a : A, b: B a} DED (pi1 (pair A B a b)) EQ a ❘ role Simplify ❙
// Note that conv_pi2 only type-checks because conv_pi1 is used as a simplification rule. ❙
conv_pi2 : {A : type, B: A ⟶ type}{a : A, b: B a} DED (pi2 (pair A B a b)) EQ b ❘ role Simplify ❙
❚