From ba755a9c4b95d2b7afa804354a9248fbf99a3497 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Tue, 2 May 2023 23:08:49 +0200 Subject: [PATCH] haha oops i made this change to check an error and checked it in by accident --- examples/misc.quox | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/misc.quox b/examples/misc.quox index 5ae7e76..f6ba7d9 100644 --- a/examples/misc.quox +++ b/examples/misc.quox @@ -33,4 +33,4 @@ def sym : 0.(A : ★₀) → 0.(x y : A) → 1.(x ≡ y : A) → y ≡ x : A = def trans : 0.(A : ★₀) → 0.(x y z : A) → ω.(x ≡ y : A) → ω.(y ≡ z : A) → x ≡ z : A = λ A x y z eq1 eq2 ⇒ δ 𝑖 ⇒ - comp [A] @0 @1 (eq1 @𝑖) @𝑖 { 0 _ ⇒ eq1 @0; 1 𝑗 ⇒ eq2 @0 }; + comp [A] @0 @1 (eq1 @𝑖) @𝑖 { 0 _ ⇒ eq1 @0; 1 𝑗 ⇒ eq2 @𝑗 };