Error: Universe inconsistency (cannot enforce Set <= Prop). #50

Closed
JasonGross opened this Issue Jul 23, 2013 · 1 comment

2 participants

@JasonGross

Coq should be smart enough to figure out that there's a consistent assignment of universes which makes the following work (in particular, replacing the Type in the type of Morphism with Set makes the code go through).

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). *)

Is there some fundamental trouble with dealing with Set and Prop?

@mattam82
Homotopy Type Theory member

No, I think it´s an inference issue in pattern-matching, it should take the max of Prop and Set as the type of the match.

@JasonGross JasonGross referenced this issue in HoTT/HoTT Jul 23, 2013
Merged

Make Unit a Set #154

@mattam82 mattam82 closed this in 1bd42a6 Jul 23, 2013
@peterlefanulumsdaine peterlefanulumsdaine pushed a commit to peterlefanulumsdaine/HoTT that referenced this issue Nov 12, 2013
@JasonGross JasonGross Make Unit a Set
Having Unit in Prop causing issues and universe inconsistencies, such as
HoTT/coq#50.
5826cf6
@peterlefanulumsdaine peterlefanulumsdaine pushed a commit to peterlefanulumsdaine/HoTT that referenced this issue Nov 12, 2013
@JasonGross JasonGross Make Unit a Set
Having Unit in Prop causing issues and universe inconsistencies, such as
HoTT/coq#50.
7ede357
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment