example.dtt 848 B

123456789101112131415161718192021222324252627282930313233
  1. inductive Nat : Type of {
  2. Z : Nat; S : Nat -> Nat
  3. }.
  4. inductive Foo : Type of {
  5. Bar : Foo
  6. }.
  7. inductive Eq : (x: Type) -> x -> x -> Type of {
  8. Refl : (α: Type) -> (a: α) -> Eq α a a
  9. }.
  10. inductive Pair : Type -> Type -> Type of {
  11. MkPair : (α, β: Type) -> α -> β -> Pair α β
  12. }.
  13. postulate Commutative : (α: Type) -> (a, b: α)
  14. -> Eq α a b -> Eq α b a.
  15. define Commutative := /\α. \(a, b: α) (pa: Eq α a b). Refl α b.
  16. postulate Transitive : (α: Type) -> (a, b, c: α)
  17. -> Eq α a b -> Eq α b c -> Eq α a c.
  18. define Transitive := /\α.
  19. \(a, b, c: α)
  20. (pa: Eq α a b)
  21. (pb: Eq α b c). Refl α a.
  22. let pair = MkPair Nat Nat Z (S Z);
  23. let tp = case pair of {
  24. (MkPair α β a b) -> Eq β b b
  25. };
  26. (Refl Nat (S Z) : tp)