Closed favonia closed 5 years ago
BTW, this works in this PR:
def lemma0
(A : [i] type [])
(B : [i] type [i=0 → A 0])
(C : [i] type [i=0 → A 1])
: type
= [i] (comp 0 1 (A i) [i=0 → B | i=1 → C]) []
def lemma1
(A : [i] type [])
(B : [i] type [i=0 → A 0])
(C : [i] type [i=0 → A 1])
(b : B 1)
(c : C 1)
(a : [i] A i [i = 0 → coe 1 0 b in B | i = 1 → coe 1 0 c in C])
: lemma0 A B C
= λ i → box (a i) [b | c]
def lemma2
(A : [i] type [])
(B : [i] type [i=0 → A 0])
(C : [i] type [i=0 → A 1])
(b : B 1)
(c : C 1)
(a : [i] A i [i = 0 → coe 1 0 b in B | i = 1 → coe 1 0 c in C])
: [i] A i []
= λ i → lemma1 A B C b c a i .cap
Close #410, mostly.