Inductive paths {A : Type} (a : A) : A -> Type :=
idpath : paths a a.
Record PreCategory :=
{
Object :> Type;
Morphism : Object -> Object -> Type
}.
Definition DiscreteCategory X : PreCategory
:= @Build_PreCategory X
(@paths X).
Definition IndiscreteCategory X : PreCategory
:= @Build_PreCategory X
(fun _ _ => Unit).
Definition NatCategory (n : nat) := match n with
| 0 => IndiscreteCategory Unit
| _ => DiscreteCategory Bool end. (* Error: Universe inconsistency (cannot enforce Set <= Prop).*)
Definition NatCategory' (n : nat) := match n with
| 0 => (fun X => @Build_PreCategory X
(fun _ _ => Unit : Set)) Unit
| _ => DiscreteCategory Bool end.
Definition NatCategory'' (n : nat) := match n with
| 0 => IndiscreteCategory Unit
| _ => DiscreteCategory Bool end.
¤ 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.0.3Bemerkung:
¤
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.
