quox/tests/Tests/Typechecker.idr

485 lines
19 KiB
Idris
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

module Tests.Typechecker
import Quox.Syntax
import Quox.Typechecker as Lib
import public TypingImpls
import TAP
import Quox.EffExtra
data Error'
= TCError Typing.Error
| WrongInfer (Term d n) (Term d n)
| WrongQOut (QOutput n) (QOutput n)
export
ToInfo Error' where
toInfo (TCError e) = toInfo e
toInfo (WrongInfer good bad) =
[("type", "WrongInfer"),
("wanted", prettyStr True good),
("got", prettyStr True bad)]
toInfo (WrongQOut good bad) =
[("type", "WrongQOut"),
("wanted", prettyStr True good),
("wanted", prettyStr True bad)]
0 M : Type -> Type
M = Eff [Except Error', DefsReader]
inj : TC a -> M a
inj = rethrow . mapFst TCError <=< lift . runExcept
reflTy : Term d n
reflTy =
Pi_ Zero "A" (TYPE 0) $
Pi_ One "x" (BVT 0) $
Eq0 (BVT 1) (BVT 0) (BVT 0)
reflDef : Term d n
reflDef = [< "A","x"] :\\ [< "i"] :\\% BVT 0
fstTy : Term d n
fstTy =
(Pi_ Zero "A" (TYPE 1) $
Pi_ Zero "B" (Arr Any (BVT 0) (TYPE 1)) $
Arr Any (Sig_ "x" (BVT 1) $ E $ BV 1 :@ BVT 0) (BVT 1))
fstDef : Term d n
fstDef =
([< "A","B","p"] :\\
E (CasePair Any (BV 0) (SN $ BVT 2) (SY [< "x","y"] $ BVT 1)))
sndTy : Term d n
sndTy =
(Pi_ Zero "A" (TYPE 1) $
Pi_ Zero "B" (Arr Any (BVT 0) (TYPE 1)) $
Pi_ Any "p" (Sig_ "x" (BVT 1) $ E $ BV 1 :@ BVT 0) $
E (BV 1 :@ E (F "fst" :@@ [BVT 2, BVT 1, BVT 0])))
sndDef : Term d n
sndDef =
([< "A","B","p"] :\\
E (CasePair Any (BV 0)
(SY [< "p"] $ E $ BV 2 :@ E (F "fst" :@@ [BVT 3, BVT 2, BVT 0]))
(SY [< "x","y"] $ BVT 0)))
defGlobals : Definitions
defGlobals = fromList
[("A", mkPostulate gzero $ TYPE 0),
("B", mkPostulate gzero $ TYPE 0),
("C", mkPostulate gzero $ TYPE 1),
("D", mkPostulate gzero $ TYPE 1),
("P", mkPostulate gzero $ Arr Any (FT "A") (TYPE 0)),
("a", mkPostulate gany $ FT "A"),
("a'", mkPostulate gany $ FT "A"),
("b", mkPostulate gany $ FT "B"),
("f", mkPostulate gany $ Arr One (FT "A") (FT "A")),
("g", mkPostulate gany $ Arr One (FT "A") (FT "B")),
("f2", mkPostulate gany $ Arr One (FT "A") $ Arr One (FT "A") (FT "B")),
("p", mkPostulate gany $ Pi_ One "x" (FT "A") $ E $ F "P" :@ BVT 0),
("q", mkPostulate gany $ Pi_ One "x" (FT "A") $ E $ F "P" :@ BVT 0),
("refl", mkDef gany reflTy reflDef),
("fst", mkDef gany fstTy fstDef),
("snd", mkDef gany sndTy sndDef)]
parameters (label : String) (act : Lazy (M ()))
{default defGlobals globals : Definitions}
testTC : Test
testTC = test label {e = Error', a = ()} $
extract $ runExcept $ runReader globals act
testTCFail : Test
testTCFail = testThrows label (const True) $
(extract $ runExcept $ runReader globals act) $> "()"
anys : {n : Nat} -> QContext n
anys {n = 0} = [<]
anys {n = S n} = anys :< Any
ctx, ctx01 : {n : Nat} -> Context (\n => (BaseName, Term 0 n)) n ->
TyContext 0 n
ctx tel = let (ns, ts) = unzip tel in
MkTyContext new [<] ts ns anys
ctx01 tel = let (ns, ts) = unzip tel in
MkTyContext ZeroIsOne [<] ts ns anys
empty01 : TyContext 0 0
empty01 = eqDim (K Zero) (K One) empty
inferredTypeEq : TyContext d n -> (exp, got : Term d n) -> M ()
inferredTypeEq ctx exp got =
wrapErr (const $ WrongInfer exp got) $ inj $ equalType ctx exp got
qoutEq : (exp, got : QOutput n) -> M ()
qoutEq qout res = unless (qout == res) $ throw $ WrongQOut qout res
inferAs : TyContext d n -> (sg : SQty) -> Elim d n -> Term d n -> M ()
inferAs ctx@(MkTyContext {dctx, _}) sg e ty = do
case !(inj $ infer ctx sg e) of
Just res => inferredTypeEq ctx ty res.type
Nothing => pure ()
inferAsQ : TyContext d n -> (sg : SQty) ->
Elim d n -> Term d n -> QOutput n -> M ()
inferAsQ ctx@(MkTyContext {dctx, _}) sg e ty qout = do
case !(inj $ infer ctx sg e) of
Just res => do
inferredTypeEq ctx ty res.type
qoutEq qout res.qout
Nothing => pure ()
infer_ : TyContext d n -> (sg : SQty) -> Elim d n -> M ()
infer_ ctx sg e = ignore $ inj $ infer ctx sg e
checkQ : TyContext d n -> SQty ->
Term d n -> Term d n -> QOutput n -> M ()
checkQ ctx@(MkTyContext {dctx, _}) sg s ty qout = do
case !(inj $ check ctx sg s ty) of
Just res => qoutEq qout res
Nothing => pure ()
check_ : TyContext d n -> SQty -> Term d n -> Term d n -> M ()
check_ ctx sg s ty = ignore $ inj $ check ctx sg s ty
checkType_ : TyContext d n -> Term d n -> Maybe Universe -> M ()
checkType_ ctx s u = inj $ checkType ctx s u
export
tests : Test
tests = "typechecker" :- [
"universes" :- [
testTC "0 · ★₀ ⇐ ★₁ # by checkType" $
checkType_ empty (TYPE 0) (Just 1),
testTC "0 · ★₀ ⇐ ★₁ # by check" $
check_ empty szero (TYPE 0) (TYPE 1),
testTC "0 · ★₀ ⇐ ★₂" $
checkType_ empty (TYPE 0) (Just 2),
testTC "0 · ★₀ ⇐ ★_" $
checkType_ empty (TYPE 0) Nothing,
testTCFail "0 · ★₁ ⇍ ★₀" $
checkType_ empty (TYPE 1) (Just 0),
testTCFail "0 · ★₀ ⇍ ★₀" $
checkType_ empty (TYPE 0) (Just 0),
testTC "0=1 ⊢ 0 · ★₁ ⇐ ★₀" $
checkType_ empty01 (TYPE 1) (Just 0),
testTCFail "1 · ★₀ ⇍ ★₁ # by check" $
check_ empty sone (TYPE 0) (TYPE 1)
],
"function types" :- [
note "A, B : ★₀; C, D : ★₁; P : A ⇾ ★₀",
testTC "0 · A ⊸ B ⇐ ★₀" $
check_ empty szero (Arr One (FT "A") (FT "B")) (TYPE 0),
note "subtyping",
testTC "0 · A ⊸ B ⇐ ★₁" $
check_ empty szero (Arr One (FT "A") (FT "B")) (TYPE 1),
testTC "0 · C ⊸ D ⇐ ★₁" $
check_ empty szero (Arr One (FT "C") (FT "D")) (TYPE 1),
testTCFail "0 · C ⊸ D ⇍ ★₀" $
check_ empty szero (Arr One (FT "C") (FT "D")) (TYPE 0),
testTC "0 · (1·x : A) → P x ⇐ ★₀" $
check_ empty szero
(Pi_ One "x" (FT "A") $ E $ F "P" :@ BVT 0)
(TYPE 0),
testTCFail "0 · A ⊸ P ⇍ ★₀" $
check_ empty szero (Arr One (FT "A") $ FT "P") (TYPE 0),
testTC "0=1 ⊢ 0 · A ⊸ P ⇐ ★₀" $
check_ empty01 szero (Arr One (FT "A") $ FT "P") (TYPE 0)
],
"pair types" :- [
note #""A × B" for "(_ : A) × B""#,
testTC "0 · A × A ⇐ ★₀" $
check_ empty szero (FT "A" `And` FT "A") (TYPE 0),
testTCFail "0 · A × P ⇍ ★₀" $
check_ empty szero (FT "A" `And` FT "P") (TYPE 0),
testTC "0 · (x : A) × P x ⇐ ★₀" $
check_ empty szero
(Sig_ "x" (FT "A") $ E $ F "P" :@ BVT 0) (TYPE 0),
testTC "0 · (x : A) × P x ⇐ ★₁" $
check_ empty szero
(Sig_ "x" (FT "A") $ E $ F "P" :@ BVT 0) (TYPE 1),
testTC "0 · (A : ★₀) × A ⇐ ★₁" $
check_ empty szero (Sig_ "A" (TYPE 0) $ BVT 0) (TYPE 1),
testTCFail "0 · (A : ★₀) × A ⇍ ★₀" $
check_ empty szero (Sig_ "A" (TYPE 0) $ BVT 0) (TYPE 0),
testTCFail "1 · A × A ⇍ ★₀" $
check_ empty sone (FT "A" `And` FT "A") (TYPE 0)
],
"enum types" :- [
testTC "0 · {} ⇐ ★₀" $ check_ empty szero (enum []) (TYPE 0),
testTC "0 · {} ⇐ ★₃" $ check_ empty szero (enum []) (TYPE 3),
testTC "0 · {a,b,c} ⇐ ★₀" $
check_ empty szero (enum ["a", "b", "c"]) (TYPE 0),
testTC "0 · {a,b,c} ⇐ ★₃" $
check_ empty szero (enum ["a", "b", "c"]) (TYPE 3),
testTCFail "1 · {} ⇍ ★₀" $ check_ empty sone (enum []) (TYPE 0),
testTC "0=1 ⊢ 1 · {} ⇐ ★₀" $ check_ empty01 sone (enum []) (TYPE 0)
],
"free vars" :- [
note "A : ★₀",
testTC "0 · A ⇒ ★₀" $
inferAs empty szero (F "A") (TYPE 0),
testTC "0 · [A] ⇐ ★₀" $
check_ empty szero (FT "A") (TYPE 0),
note "subtyping",
testTC "0 · [A] ⇐ ★₁" $
check_ empty szero (FT "A") (TYPE 1),
note "(fail) runtime-relevant type",
testTCFail "1 · A ⇏ ★₀" $
infer_ empty sone (F "A"),
note "refl : (0·A : ★₀) → (1·x : A) → (x ≡ x : A) ≔ (λ A x ⇒ δ _ ⇒ x)",
testTC "1 · refl ⇒ ⋯" $ inferAs empty sone (F "refl") reflTy,
testTC "1 · [refl] ⇐ ⋯" $ check_ empty sone (FT "refl") reflTy
],
"bound vars" :- [
testTC "x : A ⊢ 1 · x ⇒ A ⊳ 1·x" $
inferAsQ {n = 1} (ctx [< ("x", FT "A")]) sone
(BV 0) (FT "A") [< One],
testTC "x : A ⊢ 1 · [x] ⇐ A ⊳ 1·x" $
checkQ {n = 1} (ctx [< ("x", FT "A")]) sone (BVT 0) (FT "A") [< One],
note "f2 : A ⊸ A ⊸ B",
testTC "x : A ⊢ 1 · f2 [x] [x] ⇒ B ⊳ ω·x" $
inferAsQ {n = 1} (ctx [< ("x", FT "A")]) sone
(F "f2" :@@ [BVT 0, BVT 0]) (FT "B") [< Any]
],
"lambda" :- [
note "linear & unrestricted identity",
testTC "1 · (λ x ⇒ x) ⇐ A ⊸ A" $
check_ empty sone ([< "x"] :\\ BVT 0) (Arr One (FT "A") (FT "A")),
testTC "1 · (λ x ⇒ x) ⇐ A → A" $
check_ empty sone ([< "x"] :\\ BVT 0) (Arr Any (FT "A") (FT "A")),
note "(fail) zero binding used relevantly",
testTCFail "1 · (λ x ⇒ x) ⇍ A ⇾ A" $
check_ empty sone ([< "x"] :\\ BVT 0) (Arr Zero (FT "A") (FT "A")),
note "(but ok in overall erased context)",
testTC "0 · (λ x ⇒ x) ⇐ A ⇾ A" $
check_ empty szero ([< "x"] :\\ BVT 0) (Arr Zero (FT "A") (FT "A")),
testTC "1 · (λ A x ⇒ refl A x) ⇐ ⋯ # (type of refl)" $
check_ empty sone
([< "A", "x"] :\\ E (F "refl" :@@ [BVT 1, BVT 0]))
reflTy,
testTC "1 · (λ A x ⇒ δ i ⇒ x) ⇐ ⋯ # (def. and type of refl)" $
check_ empty sone reflDef reflTy
],
"pairs" :- [
testTC "1 · (a, a) ⇐ A × A" $
check_ empty sone (Pair (FT "a") (FT "a")) (FT "A" `And` FT "A"),
testTC "x : A ⊢ 1 · (x, x) ⇐ A × A ⊳ ω·x" $
checkQ (ctx [< ("x", FT "A")]) sone
(Pair (BVT 0) (BVT 0)) (FT "A" `And` FT "A") [< Any],
testTC "1 · (a, δ i ⇒ a) ⇐ (x : A) × (x ≡ a)" $
check_ empty sone
(Pair (FT "a") ([< "i"] :\\% FT "a"))
(Sig_ "x" (FT "A") $ Eq0 (FT "A") (BVT 0) (FT "a"))
],
"unpairing" :- [
testTC "x : A × A ⊢ 1 · (case1 x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ 1·x" $
inferAsQ (ctx [< ("x", FT "A" `And` FT "A")]) sone
(CasePair One (BV 0) (SN $ FT "B")
(SY [< "l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0]))
(FT "B") [< One],
testTC "x : A × A ⊢ 1 · (caseω x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ ω·x" $
inferAsQ (ctx [< ("x", FT "A" `And` FT "A")]) sone
(CasePair Any (BV 0) (SN $ FT "B")
(SY [< "l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0]))
(FT "B") [< Any],
testTC "x : A × A ⊢ 0 · (caseω x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ 0·x" $
inferAsQ (ctx [< ("x", FT "A" `And` FT "A")]) szero
(CasePair Any (BV 0) (SN $ FT "B")
(SY [< "l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0]))
(FT "B") [< Zero],
testTCFail "x : A × A ⊢ 1 · (case0 x return B of (l,r) ⇒ f2 l r) ⇏" $
infer_ (ctx [< ("x", FT "A" `And` FT "A")]) sone
(CasePair Zero (BV 0) (SN $ FT "B")
(SY [< "l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0])),
testTC "x : A × B ⊢ 1 · (caseω x return A of (l,r) ⇒ l) ⇒ A ⊳ ω·x" $
inferAsQ (ctx [< ("x", FT "A" `And` FT "B")]) sone
(CasePair Any (BV 0) (SN $ FT "A")
(SY [< "l", "r"] $ BVT 1))
(FT "A") [< Any],
testTC "x : A × B ⊢ 0 · (case1 x return A of (l,r) ⇒ l) ⇒ A ⊳ 0·x" $
inferAsQ (ctx [< ("x", FT "A" `And` FT "B")]) szero
(CasePair One (BV 0) (SN $ FT "A")
(SY [< "l", "r"] $ BVT 1))
(FT "A") [< Zero],
testTCFail "x : A × B ⊢ 1 · (case1 x return A of (l,r) ⇒ l) ⇏" $
infer_ (ctx [< ("x", FT "A" `And` FT "B")]) sone
(CasePair One (BV 0) (SN $ FT "A")
(SY [< "l", "r"] $ BVT 1)),
note "fst : (0·A : ★₁) → (0·B : A ↠ ★₁) → ((x : A) × B x) ↠ A",
note " ≔ (λ A B p ⇒ caseω p return A of (x, y) ⇒ x)",
testTC "0 · type of fst ⇐ ★₂" $
check_ empty szero fstTy (TYPE 2),
testTC "1 · def of fsttype of fst" $
check_ empty sone fstDef fstTy,
note "snd : (0·A : ★₁) → (0·B : A ↠ ★₁) → (ω·p : (x : A) × B x) → B (fst A B p)",
note " ≔ (λ A B p ⇒ caseω p return p ⇒ B (fst A B p) of (x, y) ⇒ y)",
testTC "0 · type of snd ⇐ ★₂" $
check_ empty szero sndTy (TYPE 2),
testTC "1 · def of sndtype of snd" $
check_ empty sone sndDef sndTy,
testTC "0 · snd ★₀ (λ x ⇒ x) ⇒ (ω·p : (A : ★₀) × A) → fst ★₀ (λ x ⇒ x) p" $
inferAs empty szero
(F "snd" :@@ [TYPE 0, [< "x"] :\\ BVT 0])
(Pi_ Any "A" (Sig_ "A" (TYPE 0) $ BVT 0) $
(E $ F "fst" :@@ [TYPE 0, [< "x"] :\\ BVT 0, BVT 0]))
],
"enums" :- [
testTC "1 · 'a ⇐ {a}" $
check_ empty sone (Tag "a") (enum ["a"]),
testTC "1 · 'a ⇐ {a, b, c}" $
check_ empty sone (Tag "a") (enum ["a", "b", "c"]),
testTCFail "1 · 'a ⇍ {b, c}" $
check_ empty sone (Tag "a") (enum ["b", "c"]),
testTC "0=1 ⊢ 1 · 'a ⇐ {b, c}" $
check_ empty01 sone (Tag "a") (enum ["b", "c"])
],
"enum matching" :- [
testTC "ω.x : {tt} ⊢ 1 · case1 x return {tt} of { 'tt ⇒ 'tt } ⇒ {tt}" $
inferAs (ctx [< ("x", enum ["tt"])]) sone
(CaseEnum One (BV 0) (SN (enum ["tt"])) $
singleton "tt" (Tag "tt"))
(enum ["tt"]),
testTCFail "ω.x : {tt} ⊢ 1 · case1 x return {tt} of { 'ff ⇒ 'tt } ⇏" $
infer_ (ctx [< ("x", enum ["tt"])]) sone
(CaseEnum One (BV 0) (SN (enum ["tt"])) $
singleton "ff" (Tag "tt"))
],
"equality types" :- [
testTC "0 · : ★₀ ⇐ Type" $
checkType_ empty (Eq0 (TYPE 0) Nat Nat) Nothing,
testTC "0 · : ★₀ ⇐ ★₁" $
check_ empty szero (Eq0 (TYPE 0) Nat Nat) (TYPE 1),
testTCFail "1 · : ★₀ ⇍ ★₁" $
check_ empty sone (Eq0 (TYPE 0) Nat Nat) (TYPE 1),
testTC "0 · : ★₀ ⇐ ★₂" $
check_ empty szero (Eq0 (TYPE 0) Nat Nat) (TYPE 2),
testTC "0 · : ★₁ ⇐ ★₂" $
check_ empty szero (Eq0 (TYPE 1) Nat Nat) (TYPE 2),
testTCFail "0 · : ★₁ ⇍ ★₁" $
check_ empty szero (Eq0 (TYPE 1) Nat Nat) (TYPE 1),
testTCFail "0 ≡ 'beep : {beep} ⇍ Type" $
checkType_ empty (Eq0 (enum ["beep"]) Zero (Tag "beep")) Nothing,
testTC "ab : A ≡ B : ★₀, x : A, y : B ⊢ 0 · Eq [i ⇒ ab i] x y ⇐ ★₀" $
check_ (ctx [< ("ab", Eq0 (TYPE 0) (FT "A") (FT "B")),
("x", FT "A"), ("y", FT "B")]) szero
(Eq (SY [< "i"] $ E $ BV 2 :% BV 0) (BVT 1) (BVT 0))
(TYPE 0),
testTCFail "ab : A ≡ B : ★₀, x : A, y : B ⊢ Eq [i ⇒ ab i] y x ⇍ Type" $
checkType_ (ctx [< ("ab", Eq0 (TYPE 0) (FT "A") (FT "B")),
("x", FT "A"), ("y", FT "B")])
(Eq (SY [< "i"] $ E $ BV 2 :% BV 0) (BVT 0) (BVT 1))
Nothing
],
"equalities" :- [
testTC "1 · (δ i ⇒ a) ⇐ a ≡ a" $
check_ empty sone (DLam $ SN $ FT "a")
(Eq0 (FT "A") (FT "a") (FT "a")),
testTC "0 · (λ p q ⇒ δ i ⇒ p) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
check_ empty szero
([< "p","q"] :\\ [< "i"] :\\% BVT 1)
(Pi_ Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $
Pi_ Any "q" (Eq0 (FT "A") (FT "a") (FT "a")) $
Eq0 (Eq0 (FT "A") (FT "a") (FT "a")) (BVT 1) (BVT 0)),
testTC "0 · (λ p q ⇒ δ i ⇒ q) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
check_ empty szero
([< "p","q"] :\\ [< "i"] :\\% BVT 0)
(Pi_ Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $
Pi_ Any "q" (Eq0 (FT "A") (FT "a") (FT "a")) $
Eq0 (Eq0 (FT "A") (FT "a") (FT "a")) (BVT 1) (BVT 0))
],
"natural numbers" :- [
testTC "0 · ⇐ ★₀" $ check_ empty szero Nat (TYPE 0),
testTC "0 · ⇐ ★₇" $ check_ empty szero Nat (TYPE 7),
testTCFail "1 · ⇍ ★₀" $ check_ empty sone Nat (TYPE 0),
testTC "1 · zero ⇐ " $ check_ empty sone Zero Nat,
testTCFail "1 · zero ⇍ ×" $ check_ empty sone Zero (Nat `And` Nat),
testTC "ω·n : ⊢ 1 · succ n ⇐ " $
check_ (ctx [< ("n", Nat)]) sone (Succ (BVT 0)) Nat,
testTC "1 · λ n ⇒ succ n ⇐ 1." $
check_ empty sone ([< "n"] :\\ Succ (BVT 0)) (Arr One Nat Nat),
todo "nat elim"
],
"natural elim" :- [
note "1 · λ n ⇒ case1 n return of { zero ⇒ 0; succ n ⇒ n }",
note " ⇐ 1.",
testTC "pred" $
check_ empty sone
([< "n"] :\\ E (CaseNat One Zero (BV 0) (SN Nat)
Zero (SY [< "n", Unused] $ BVT 1)))
(Arr One Nat Nat),
note "1 · λ m n ⇒ case1 m return of { zero ⇒ n; succ _, 1.p ⇒ succ p }",
note " ⇐ 1. → 1. → 1.",
testTC "plus" $
check_ empty sone
([< "m", "n"] :\\ E (CaseNat One One (BV 1) (SN Nat)
(BVT 0) (SY [< Unused, "p"] $ Succ $ BVT 0)))
(Arr One Nat $ Arr One Nat Nat)
],
"box types" :- [
testTC "0 · [0.] ⇐ ★₀" $
check_ empty szero (BOX Zero Nat) (TYPE 0),
testTC "0 · [0.★₀] ⇐ ★₁" $
check_ empty szero (BOX Zero (TYPE 0)) (TYPE 1),
testTCFail "0 · [0.★₀] ⇍ ★₀" $
check_ empty szero (BOX Zero (TYPE 0)) (TYPE 0)
],
todo "box values",
todo "box elim",
"misc" :- [
note "0·A : Type, 0·P : A → Type, ω·p : (1·x : A) → P x",
note "",
note "1 · λ x y xy ⇒ δ i ⇒ p (xy i)",
note " ⇐ (0·x y : A) → (1·xy : x ≡ y) → Eq [i ⇒ P (xy i)] (p x) (p y)",
testTC "cong" $
check_ empty sone
([< "x", "y", "xy"] :\\ [< "i"] :\\% E (F "p" :@ E (BV 0 :% BV 0)))
(Pi_ Zero "x" (FT "A") $
Pi_ Zero "y" (FT "A") $
Pi_ One "xy" (Eq0 (FT "A") (BVT 1) (BVT 0)) $
Eq_ "i" (E $ F "P" :@ E (BV 0 :% BV 0))
(E $ F "p" :@ BVT 2) (E $ F "p" :@ BVT 1)),
note "0·A : Type, 0·P : ω·A → Type,",
note "ω·p q : (1·x : A) → P x",
note "",
note "1 · λ eq ⇒ δ i ⇒ λ x ⇒ eq x i",
note " ⇐ (1·eq : (1·x : A) → p x ≡ q x) → p ≡ q",
testTC "funext" $
check_ empty sone
([< "eq"] :\\ [< "i"] :\\% [< "x"] :\\ E (BV 1 :@ BVT 0 :% BV 0))
(Pi_ One "eq"
(Pi_ One "x" (FT "A")
(Eq0 (E $ F "P" :@ BVT 0)
(E $ F "p" :@ BVT 0) (E $ F "q" :@ BVT 0)))
(Eq0 (Pi_ Any "x" (FT "A") $ E $ F "P" :@ BVT 0) (FT "p") (FT "q"))),
todo "absurd (when coerce is in)"
-- absurd : (`true ≡ `false : {true, false}) ⇾ (0·A : ★₀) → A ≔
-- λ e ⇒
-- case coerce [i ⇒ case e @i return ★₀ of {`true ⇒ {tt}; `false ⇒ {}}]
-- @0 @1 `tt
-- return A
-- of { }
]
]