Currying inside systems

[3abc]

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
  ]

[jonsterling]

@3abc I believe the issue has to do with the fact that we do not yet fully support partial application of an n-ary extension type. I would have to check the code to see if that is indeed what is happening -- I have been stuck in paper-writing land for some months and haven't been able to work on this.