Identity : forall x, Morphism x x;
Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d';
LeftIdentity : forall a b (f : Morphism a b), Compose (Identity b) f = f
}.
Section DiscreteAdjoints.
Let C := {|
Morphism := (fun X Y : Type => X -> Y);
Identity := (fun X : Type => (fun x : X => x));
Compose := (fun _ _ _ f g => (fun x => f (g x)));
LeftIdentity := (fun X Y p => @eq_refl _ p : (fun x : X => p x) = p)
|}. Variable ObjectFunctor : C = C.
Goal True. Proof.
subst C.
revert ObjectFunctor. intro ObjectFunctor. simpl in ObjectFunctor.
revert ObjectFunctor. Abort.
End DiscreteAdjoints.
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤
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.
