Record cFunctor := CFunctor {
cFunctor_car : ofeT -> ofeT;
cFunctor_map : forall A : ofeT, cFunctor_car A;
}.
Definition iprod {A} (B : A -> ofeT) := forall x, B x.
Canonical Structure iprodC A (B : A -> ofeT) : ofeT := OfeT (iprod B).
Definition iprodC_map {A} {B : A -> ofeT} (f : forall x, B x) : iprodC A B := f.
Axiom iprodC_map_ne : forall {A} {B : A -> ofeT} x, dist (@iprodC_map A B x).
Definition iprodCF {C} (F : cFunctor) : cFunctor := {|
cFunctor_car := fun B => iprodC C (fun c => cFunctor_car F B);
cFunctor_map := fun B => iprodC_map (fun c => cFunctor_map F B)
|}.
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
