|
Module FirstIssue.
Set Implicit Arguments.
Record Cat (obj : Type) := {}.
Record Functor objC (C : Cat objC) objD (D : Cat objD) :=
{
ObjectOf' : objC -> objD
}.
Definition TypeCat : Cat Type. constructor. Defined.
Definition PropCat : Cat Prop. constructor. Defined.
Definition FunctorFrom_Type2Prop objC (C : Cat objC) (F : Functor TypeCat C) : Functor PropCat C.
Set Printing All.
Set Printing Universes.
Check F. (* F : @Functor Type (* Top.1201 *) TypeCat objC C *)
exact (Build_Functor PropCat C (ObjectOf' F)).
Show Proof. (* (fun (objC : Type (* Top.1194 *)) (C : Cat objC)
(F : @Functor Prop TypeCat objC C) =>
@Build_Functor Prop PropCat objC C
(@ObjectOf' Prop TypeCat objC C F)) *)
Defined.
(* Error: Illegal application (Type Error):
The term "Functor" of type
"forall (objC : Type (* Top.1194 *)
(objD : Type (* Top.1194 *)) (_ : Cat objD),
Type (* Top.1194 *)"
cannot be applied to the terms
"Prop" : "Type (* (Set)+1 *)"
"TypeCat" : "Cat Type (* Top.1201 *)"
"objC" : "Type (* Top.1194 *)"
"C" : "Cat objC"
The 2nd term has type "Cat Type (* Top.1201 *)"
which should be coercible to "Cat Prop". *)
End FirstIssue.
Module SecondIssue.
Set Implicit Arguments.
Set Printing Universes.
Polymorphic Record Cat (obj : Type) :=
{
Object :> _ := obj;
Morphism' : obj -> obj -> Type
}.
Polymorphic Record Functor objC (C : Cat objC) objD (D : Cat objD) :=
{
ObjectOf' : objC -> objD;
MorphismOf' : forall s d, C.(Morphism') s d -> D.(Morphism') (ObjectOf' s) (ObjectOf' d)
}.
Definition SetCat : Cat Set := @Build_Cat Set (fun x y => x -> y).
Definition PropCat : Cat Prop := @Build_Cat Prop (fun x y => x -> y).
Set Printing All.
Definition FunctorFrom_Set2Prop objC (C : Cat objC) (F : Functor SetCat C) : Functor PropCat C.
exact (Build_Functor PropCat C
(ObjectOf' F)
(MorphismOf' F)
).
Defined. (* Error: Illegal application (Type Error):
The term "Build_Functor (* Top.748 Prop Top.808 Top.809 *)
"forall (objC : Type (* Top.748 *)) (C : Cat (* Top.748 Prop *) objC)
(objD : Type (* Top.808 *)) (D : Cat (* Top.808 Top.809 *) objD)
(ObjectOf' : forall _ : objC, objD)
(_ : forall (s d : objC) (_ : @Morphism' (* Top.748 Prop *) objC C s d),
@Morphism' (* Top.808 Top.809 *) objD D (ObjectOf' s) (ObjectOf' d)),
@Functor (* Top.748 Prop Top.808 Top.809 *) objC C objD D"
cannot be applied to the terms
"Prop" : "Type (* (Set)+1 *)"
"PropCat" : "Cat (* Top.748 Prop *) Prop"
"objC" : "Type (* Top.808 *)"
"C" : "Cat (* Top.808 Top.809 *) objC"
"fun x : Prop =>
@ObjectOf' (* Top.744 Prop Top.808 Top.809 *) Set SetCat objC C F x"
: "forall _ : Prop, objC"
"@MorphismOf' (* Top.744 Prop Top.808 Top.809 *) Set SetCat objC C F"
: "forall (s d : Set) (_ : @Morphism' (* Top.744 Prop *) Set SetCat s d),
@Morphism' (* Top.808 Top.809 *) objC C
(@ObjectOf' (* Top.744 Prop Top.808 Top.809 *) Set SetCat objC C F s)
(@ObjectOf' (* Top.744 Prop Top.808 Top.809 *) Set SetCat objC C F d)"
The 6th term has type
"forall (s d : Set) (_ : @Morphism' (* Top.744 Prop *) Set SetCat s d),
@Morphism' (* Top.808 Top.809 *) objC C
(@ObjectOf' (* Top.744 Prop Top.808 Top.809 *) Set SetCat objC C F s)
(@ObjectOf' (* Top.744 Prop Top.808 Top.809 *) Set SetCat objC C F d)"
which should be coercible to
"forall (s d : Prop) (_ : @Morphism' (* Top.748 Prop *) Prop PropCat s d),
@Morphism' (* Top.808 Top.809 *) objC C
((fun x : Prop =>
@ObjectOf' (* Top.744 Prop Top.808 Top.809 *) Set SetCat objC C F x) s)
((fun x : Prop =>
@ObjectOf' (* Top.744 Prop Top.808 Top.809 *) Set SetCat objC C F x) d)".
*)
End SecondIssue.
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
|
