search

RedPRL / redtt

"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
Apache License 2.0
204 stars 12 forks source link

Misc lemmas #465

Closed clayrat closed 5 years ago

clayrat commented 5 years ago

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 commented 5 years ago

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

ecavallo commented 5 years ago

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
  ]