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