aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/HoTT_coq_007.v
blob: 844ff8756607d6cca64a281c7654591e907108cc (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
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
Unset Strict Universe Declaration.
Require Import TestSuite.admit.
Module Comment1.
  Set Implicit Arguments.

  Polymorphic Record Category (obj : Type) :=
    {
      Morphism : obj -> obj -> Type;
      Identity : forall o, Morphism o o
    }.

  Polymorphic Record Functor objC (C :Category objC) objD (D : Category objD) :=
    {
      ObjectOf :> objC -> objD;
      MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d);
      FIdentityOf : forall o, MorphismOf _ _ (C.(Identity) o) = D.(Identity) (ObjectOf o)
    }.

  Create HintDb functor discriminated.

  Hint Rewrite @FIdentityOf : functor.

  Polymorphic Definition ComposeFunctors objC C objD D objE E (G : @Functor objD D objE E) (F : @Functor objC C objD D) : Functor C E.
  refine {| ObjectOf := (fun c => G (F c));
            MorphismOf := (fun _ _ m => G.(MorphismOf) _ _ (F.(MorphismOf) _ _ m))
         |};
    intros; autorewrite with functor; reflexivity.
  Defined.

  Definition Cat0 : Category@{i j} Empty_set.
    refine {|
        Morphism := fun s d : Empty_set => s = d;
        Identity := fun o : Empty_set => eq_refl
      |};
    admit.
  Defined.

  Set Printing All.
  Set Printing Universes.

  Lemma foo objC (C : @Category objC) (C0 : Category (Functor Cat0 C)) (x : Functor Cat0 Cat0) 
  : forall (y : Functor C0 Cat0) z, (ComposeFunctors y z = x). 
    intro. intro.
    unfold ComposeFunctors.     
  Abort.
End Comment1.

Module Comment2.
  Set Implicit Arguments.

  Polymorphic Record Category (obj : Type) :=
    {
      Morphism : obj -> obj -> Type;

      Identity : forall o, Morphism o o;
      Compose : forall s d d2, Morphism d d2 -> Morphism s d -> Morphism s d2;

      LeftIdentity : forall a b (f : Morphism a b), Compose (Identity b) f = f
    }.

  Polymorphic Record Functor objC (C : Category objC) objD (D : Category objD) :=
    {
      ObjectOf : objC -> objD;
      MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d)
    }.

  Create HintDb morphism discriminated.

  Polymorphic Hint Resolve @LeftIdentity : morphism.

  Polymorphic Definition ProductCategory objC (C : Category objC) objD (D : Category objD) : @Category (objC * objD)%type.
  refine {|
      Morphism := (fun s d => (C.(Morphism) (fst s) (fst d) * D.(Morphism) (snd s) (snd d))%type);
      Identity := (fun o => (Identity _ (fst o), Identity _ (snd o)));
      Compose := (fun (s d d2 : (objC * objD)%type) m2 m1 => (C.(Compose) _ _ _ (fst m2) (fst m1), D.(Compose) _ _ _ (snd m2) (snd m1)))
    |};
    intros; apply injective_projections; simpl; auto with morphism. (* Replacing [auto with morphism] with [apply @LeftIdentity] removes the error *)
  Defined.

  Polymorphic Definition Cat0 : Category Empty_set.
  refine {|
      Morphism := fun s d : Empty_set => s = d;
      Identity := fun o : Empty_set => eq_refl;
      Compose := fun s d d2 m0 m1 => eq_trans m1 m0
    |};
    admit.
  Defined.

  Set Printing All.
  Set Printing Universes.
  Polymorphic Definition ProductLaw0Functor (objC : Type) (C : Category objC) : Functor (ProductCategory C Cat0) Cat0.
  refine (Build_Functor (ProductCategory C Cat0) Cat0 _ _). (* Toplevel input, characters 15-71:
Error: Refiner was given an argument
 "prod (* Top.2289 Top.2289 *) objC Empty_set" of type
"Type (* Top.2289 *)" instead of "Set". *)
  Abort.
  Polymorphic Definition ProductLaw0Functor (objC : Type) (C : Category objC) : Functor (ProductCategory C Cat0) Cat0.
  econstructor. (* Toplevel input, characters 0-12:
Error: No applicable tactic.
                 *)
  Abort.
End Comment2.


Module Comment3.
  Polymorphic Lemma foo {obj : Type} : 1 = 1.
  trivial.
  Qed.

  Polymorphic Hint Resolve foo. (* success *)
  Polymorphic Hint Rewrite @foo. (* Success *)
  Polymorphic Hint Resolve @foo. (* Error: @foo is a term and cannot be made a polymorphic hint, only global references can be polymorphic hints. *)
  Fail Polymorphic Hint Rewrite foo. (* Error: Cannot infer the implicit parameter obj of foo. *)
End Comment3.