aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/HoTT_coq_053.v
blob: 263dec4857cf9cde86c94a16ac49fa384482fd3b (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
(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *)
Set Printing Universes.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Universe Polymorphism.

Inductive Unit : Type :=
    tt : Unit.

Inductive Bool : Type :=
  | true : Bool
  | false : Bool.

Inductive paths {A : Type} (a : A) : A -> Type :=
  idpath : paths a a.

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

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

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

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

Definition NatCategory' (n : nat) :=
  match n with
    | 0 => (fun X => @Build_PreCategory X
                         (fun _ _ => Unit : Set)) Unit
    | _ => DiscreteCategory Bool
  end.

Definition NatCategory'' (n : nat) :=
  match n with
    | 0 => IndiscreteCategory Unit
    | _ => DiscreteCategory Bool
  end.