Class hasPt (T : Type) := Pt { pt_ : T }.
Structure ptType := Pointed {
sort :> Type; class : hasPt sort
}.
Definition pt (T : ptType) := @pt_ T (class T).
Canonical nat_ptType := Pointed nat (Pt nat 0).
Canonical forall_ptType (T : Type) (U : T -> ptType) :=
Pointed (forall t, U t) (Pt (forall t, U t) (fun t => pt (U t))).
Definition constant {T U : Type} (f : T -> U) := forall (x y : T), f x = f y. Definition cst (T U : Type) (y : U) := fun _ : T => y. Lemma constant_cst (T U : Type) (y : U) : constant (cst T U y). Proof. intros x x'; reflexivity. Qed.
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.
