aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/HoTT_coq_105.v
blob: 86001d26eb2da9440b5f575044acfbdf2cebcf58 (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
Set Primitive Projections.
Set Implicit Arguments.
Set Universe Polymorphism.
Set Asymmetric Patterns.

Inductive sum A B := inl : A -> sum A B | inr : B -> sum A B.
Inductive Empty :=.

Record category :=
  { ob :> Type;
    hom : ob -> ob -> Type
  }.
Set Printing All.
Definition sum_category (C D : category) : category :=
  {|
    ob := sum (ob C) (ob D);
    hom x y := match x, y with
                 | inl x, inl y => @hom _ x y (* Toplevel input, characters 177-178:
Error:
In environment
C : category
D : category
x : sum (ob C) (ob D)
y : sum (ob C) (ob D)
x0 : ob C
y0 : ob C
The term "x0" has type "ob C" while it is expected to have type
"ob ?6" (unable to find a well-typed instantiation for
"?6": cannot unify"Type" and "category"). *)
                 | inr x, inr y => @hom _ x y
                 | _, _ => Empty
               end |}.