fact: Definition mkCohPainting_base {n} {C: νType n} {q r} {Hrq: r.+2 <= q.+2} {Hq: q.+2 <= n.+1} {ε ω: arity} {D} {E: (mkFrame n.+1).(frame) (♢ _) D -> HSet} (d: (mkFrame r).(frame) (↓ ↓ (Hrq ↕ Hq)) D) (c: mkpainting E d): rew [mkPaintingPrev.(painting'')] (mkFrame r).(cohFrame) (Hpr := ♢ _) d in mkPaintingPrev.(restrPainting') (Hpq := Hrq) Hq ε (mkRestrPainting (ε := ω) (Hpq := ♢ _) (Hq := ↓ (Hrq ↕ Hq)) E d c) = mkPaintingPrev.(restrPainting') (Hpq := ♢ _) (Hrq ↕ Hq) ω (mkRestrPainting (ε := ε) (Hpq := ↓ Hrq) (Hq := Hq) E d c).
imports: Logic.FunctionalExtensionality Bonak(Notation) Bonak(RewLemmas) Bonak(HSet) Bonak(LeYoneda)