blob: cc5ed862664cc3d92f0abc373b4b3fcf680113b1 (
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
|
Set Implicit Arguments.
Generalizable All Variables.
Polymorphic Record Category (obj : Type) :=.
Polymorphic Record Functor objC (C : Category objC) objD (D : Category objD) :=.
Polymorphic Definition ComposeFunctors objC C objD D objE E (G : @Functor objD D objE E) (F : @Functor objC C objD D) : Functor C E.
Admitted.
Polymorphic Definition ProductCategory objC (C : Category objC) objD (D : Category objD) : @Category (objC * objD)%type.
Admitted.
Polymorphic Definition Cat0 : Category Empty_set.
Admitted.
Set Printing Universes.
Lemma ProductLaw0 objC (C : Category objC) (F : Functor (ProductCategory C Cat0) Cat0) (G : Functor Cat0 (ProductCategory C Cat0)) x y :
ComposeFunctors F G = x /\
ComposeFunctors G F = y.
Proof.
split. (* Error: Refiner was given an argument "(objC * 0)%type" of type "Type" instead of "Set". *)
Abort.
|
