fact: Definition mkCohLayer {n} {C: νType n} {p q r} {Hpr: p.+3 <= r.+3} {Hrq: r.+3 <= q.+3} {Hq: q.+3 <= n.+1} {ε ω: arity} {Frame: FrameBlock n.+1 p mkprefix mkFramePrev} {D} {d: Frame.(frame) (↓ ↓ ↓ (Hpr ↕ Hrq ↕ Hq)) D} (l: mkLayer): let sl := C.(RestrLayer) (Hpq := ⇓ (Hpr ↕ Hrq)) ε (mkRestrLayer (Hpq := ⇓ Hpr) d l) in let sl' := C.(RestrLayer) (Hpq := ⇓ Hpr) ω (mkRestrLayer (Hpq := ↓ (Hpr ↕ Hrq)) d l) in rew [C.(Layer')] Frame.(cohFrame) (Hpr := ↓ Hpr) (Hrq := Hrq) (Hq := Hq) d in sl = sl'.
imports: Logic.FunctionalExtensionality Bonak(Notation) Bonak(RewLemmas) Bonak(HSet) Bonak(LeYoneda)