Misc lemmas

[clayrat]

Since it looks like I'm stuck in #457 without a box tactic, here are some helper lemmas I've written along the way.

[jonsterling]

Sorry it's taken a little while to review this ,we'll get to it shortly!

[ecavallo]

For now, it is possible to indirectly write a box with a composition:

def boxlike
  (A : 𝕀 → type) (B0 : [j] type [j=0 → A 0]) (B1 : [j] type [j=0 → A 1])
  (a : (i : 𝕀) → A i) (b0 : [j] B0 j [j=0 → a 0]) (b1 : [j] B1 j [j=0 → a 1])
  (i : 𝕀)
  : comp 0 1 (A i) [i=0 → B0 | i=1 → B1]
  =
  comp 0 1 (a i) in λ j → comp 0 j (A i) [i=0 → B0 | i=1 → B1] [
  | i=0 → b0
  | i=1 → b1
  ]

[ecavallo]

nice work!

[jonsterling]

great!