For this definition
def comp3
(A : type)
(b : (j0 j1: π) β A)
(k0 : [j1 k] A [ k = 0 β b 0 j1])
(l0 : [j1 k] A [ k = 0 β b 1 j1])
(k1 : [j0 k] A [ k = 0 β b j0 0
| j0 = 0 β k0 0 k
| j0 = 1 β l0 0 k])
(l1 : [j0 k] A [ k = 0 β b j0 1
| j0 = 0 β k0 1 k
| j0 = 1 β l0 1 k])
(j0 j1 k : π) : A =
comp 0 k (b j0 j1) [
| j0 = 0 k β k0 j1 k
| j0 = 1 k β l0 j1 k
| j1 = 0 k β k1 j0 k
| j1 = 1 k β l1 j0 k
]
If I understand correctly j0 = 0 k β k0 j1 k can be written as j0 = 0 β k0 j1. However if I do so the type won't check.
For the definition below one can just use currying like
def comp2
(A : type)
(b : (j0: π) β A)
(k0 : [ k] A [ k = 0 β b 0])
(l0 : [ k] A [ k = 0 β b 1])
(j0 k : π) : A =
comp 0 k (b j0) [
| j0 = 0 β k0
| j0 = 1 β l0
]
For this definition
If I understand correctly
j0 = 0 k β k0 j1 kcan be written asj0 = 0 β k0 j1. However if I do so the type won't check.For the definition below one can just use currying like