aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/HoTT_coq_050.v
blob: ce9b6b29712dc3d551b4e363bcb72824cc73a50f (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
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Universe Polymorphism.
Set Printing Universes.

Set Printing All.

Record PreCategory :=
  {
    Object :> Type;
    Morphism : Object -> Object -> Type
  }.

Inductive paths A (x : A) : A -> Type := idpath : @paths A x x.
Inductive Unit : Prop := tt. (* Changing this to [Set] fixes things *)
Inductive Bool : Set := true | false.

Definition DiscreteCategory X : PreCategory
  := @Build_PreCategory X
                        (@paths X).

Definition IndiscreteCategory X : PreCategory
  := @Build_PreCategory X
                        (fun _ _ => Unit).

Check (IndiscreteCategory Unit).
Check (DiscreteCategory Bool).
Definition NatCategory (n : nat) :=
  match n with
    | 0 => IndiscreteCategory Unit
    | _ => DiscreteCategory Bool
  end. (* Error: Universe inconsistency (cannot enforce Set <= Prop). *)