Library Library





Definition
 TRUE
 := Prod
 (Srt
 prop
) (Prod
 (Ref
 0) (Ref
 1)).




Definition
 FALSE
 := Prod
 (Srt
 prop
) (Ref
 0).




Definition
 NAT
 :=

  Prod
 (Srt
 prop
)

 (Prod
 (Ref
 0)

 (Prod
 (Prod
 (Ref
 1) (Ref
 2))

  (Ref
 2))).




Definition
 EM
 :=

  Prod
 (Srt
 prop
) (Prod
 (Prod
 (Prod
 (Ref
 0) FALSE
) FALSE
) (Ref
 1)).




Definition
 EQ
 A
 x
 y
 :=

  Prod
 (Prod
 A
 (Srt
 prop
))

    (Prod
 (App
 (Ref
 0) (lift
 1 x
)) (App
 (Ref
 1) (lift
 2 y
))).




Definition
 PI
 :=

  Prod
 (Srt
 prop
) (Prod
 (Ref
 0) (Prod
 (Ref
 1)

     (EQ
 (Ref
 2) (Ref
 1) (Ref
 0)))).




Definition
 EXT
 s1
 s2
 :=

  Prod
 (Srt
 s1
) (Prod
 (Prod
 (Ref
 0) (Srt
 s2
))

    (Prod
 (Prod
 (Ref
 1) (App
 (Ref
 1) (Ref
 0)))

    (Prod
 (Prod
 (Ref
 2) (App
 (Ref
 2) (Ref
 0)))

    (Prod
 (Prod
 (Ref
 3)

             (EQ
 (App
 (Ref
 3) (Ref
 0))

               (App
 (Ref
 2) (Ref
 0)) (App
 (Ref
 1) (Ref
 0))))

    (EQ
 (Prod
 (Ref
 4) (App
 (Ref
 4) (Ref
 0))) (Ref
 2) (Ref
 1)))))).