blob: c7943b84084fed21c8d60837e7ae3e9f55e10998 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
|
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 *)) (_ : Cat objC)
(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 *)" of type
"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.
|
