From 7c24f93efc05df33388342516385b1f5ab86ff09 Mon Sep 17 00:00:00 2001 From: depsterr Date: Thu, 28 Jul 2022 15:46:00 +0200 Subject: [PATCH] update readme --- README.md | 4 +++- tests/id.pi | 4 ++++ 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index fae0104..5405a98 100644 --- a/README.md +++ b/README.md @@ -24,11 +24,13 @@ A dependently typed system # TODO -* Universes +* Universes (a la tarksi) * Elaboration * Implicit arguments * Universe family application + * Syntax level russel universes + * Universe of all other universes? (universe polymorphism) * Inductives * Indexed inductives diff --git a/tests/id.pi b/tests/id.pi index 9d98d8d..16c40fd 100644 --- a/tests/id.pi +++ b/tests/id.pi @@ -5,3 +5,7 @@ let transport : Π (A : Type) Π (f : A → Type) Π (x : A) Π (y : A) let ap : Π (A : Type) Π (B : Type) Π (f : A → B) Π (x : A) Π (y : A) Id A x y → Id B (f x) (f y) ≔ λA.λB.λf.λx.λy. J A x y (λa.λb.λ_. Id B (f a) (f b)) (refl B (f x)) + +let cat : Π (A : Type) Π (x : A) Π (y : A) Π (z : A) + Id A x y → Id A y z → Id A x z + ≔ λA.λx.λy.λz.λp.λq. J A y z (λa.λb.λr. Id A x b) (refl A y) q