HoTT/coq's universe inconsistencies do not respect delta (polyproj) (maybe?)

[JasonGross]

(* File reduced by coq-bug-finder from original input, then from 8249 lines to 907 lines, then from 843 lines to 357 lines, then from\
 351 lines to 260 lines, then from 208 lines to 162 lines, then from 167 lines to 154 lines *)
Set Universe Polymorphism.
Generalizable All Variables.
Reserved Notation "g 'o' f" (at level 40, left associativity).
Inductive paths {A : Type} (a : A) : A -> Type :=
  idpath : paths a a.
Arguments idpath {A a} , [A] a.
Notation "x = y" := (@paths _ x y) : type_scope.

Class IsEquiv {A B : Type} (f : A -> B) := {}.

Class Contr_internal (A : Type) := BuildContr {
                                       center : A ;
                                       contr : (forall y : A, center = y)
                                     }.

Inductive trunc_index : Type :=
| minus_two : trunc_index
| trunc_S : trunc_index -> trunc_index.

Fixpoint nat_to_trunc_index (n : nat) : trunc_index
  := match n with
       | 0 => trunc_S (trunc_S minus_two)
       | S n' => trunc_S (nat_to_trunc_index n')
     end.

Coercion nat_to_trunc_index : nat >-> trunc_index.

Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
  match n with
    | minus_two => Contr_internal A
    | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y)
  end.

Notation minus_one:=(trunc_S minus_two).

Class IsTrunc (n : trunc_index) (A : Type) : Type := Trunc_is_trunc : IsTrunc_internal n A.

Notation Contr := (IsTrunc minus_two).
Notation IsHProp := (IsTrunc minus_one).
Notation IsHSet := (IsTrunc 0).

Class Funext := {}.
Inductive Unit : Set := tt.

Instance contr_unit : Contr Unit | 0 := let x := {|
                                              center := tt;
                                              contr := fun t : Unit => match t with tt => idpath end
                                            |} in x.
Instance trunc_succ `{IsTrunc n A} : IsTrunc (trunc_S n) A | 1000.
admit.
Defined.
Record hProp := hp { hproptype :> Type ; isp : IsHProp hproptype}.
Definition Unit_hp:hProp:=(hp Unit _).
Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}.
Canonical Structure default_HSet:= fun T P => (@BuildhSet T P).
Definition ismono {X Y} (f : X -> Y)
  := forall Z : hSet,
     forall g h : Z -> X, (fun x => f (g x)) = (fun x => f (h x)) -> g = h.

Delimit Scope morphism_scope with morphism.
Delimit Scope category_scope with category.
Delimit Scope object_scope with object.
Record PreCategory :=
  Build_PreCategory {
      object :> Type;
      morphism : object -> object -> Type;
      compose : forall s d d', morphism d d' -> morphism s d -> morphism s d'
    }.
Arguments compose [!C s d d'] m1 m2 : rename.

Infix "o" := compose : morphism_scope.
Local Open Scope morphism_scope.

Class IsEpimorphism {C} {x y} (m : morphism C x y) :=
  is_epimorphism : forall z (m1 m2 : morphism C y z),
                     m1 o m = m2 o m
                     -> m1 = m2.

Class IsMonomorphism {C} {x y} (m : morphism C x y) :=
  is_monomorphism : forall z (m1 m2 : morphism C z x),
                      m o m1 = m o m2
                      -> m1 = m2.
Class Univalence := {}.
Global Instance isset_hProp `{Funext} : IsHSet hProp | 0. Admitted.

Definition set_cat : PreCategory
  := @Build_PreCategory hSet
                        (fun x y => forall _ : x, y)%core
                        (fun _ _ _ f g x => f (g x))%core.
Local Inductive minus1Trunc (A :Type) : Type := min1 : A -> minus1Trunc A.
Instance minus1Trunc_is_prop {A : Type} : IsHProp (minus1Trunc A) | 0. Admitted.
Definition hexists {X} (P:X->Type):Type:= minus1Trunc (sigT  P).
Definition isepi {X Y} `(f:X->Y) := forall Z: hSet,
                                    forall g h: Y -> Z, (fun x => g (f x)) = (fun x => h (f x)) -> g = h.
Definition issurj {X Y} (f:X->Y) := forall y:Y , hexists (fun x => (f x) = y).
Lemma isepi_issurj `{fs:Funext} `{ua:Univalence} `{fs' : Funext} {X Y} (f:X->Y): isepi f -> issurj f.
Proof.
  intros epif y.
  set (g :=fun _:Y => Unit_hp).
  set (h:=(fun y:Y => (hp (hexists (fun _ : Unit => {x:X & y = (f x)})) _ ))).
  clear fs'.
  hnf in epif.
  specialize (epif (BuildhSet hProp _) g h).
  admit.
Defined.
Definition isequiv_isepi_ismono `{Univalence, fs0 : Funext} (X Y : hSet) (f : X -> Y) (epif : isepi f) (monof : ismono f)
: IsEquiv f.
Proof.
  pose proof (@isepi_issurj _ _ _ _ _ f epif) as surjf.
  admit.
Defined.
Section fully_faithful_helpers.
  Context `{fs0 : Funext}.
  Variables x y : hSet.
  Variable m : x -> y.

  Let isequiv_isepi_ismono_helper ua := (@isequiv_isepi_ismono ua fs0 x y m : isepi m -> ismono m -> IsEquiv m).

  Goal True.
  set (isequiv_isepimorphism_ismonomorphism
       := fun `{Univalence}
              (Hepi : IsEpimorphism (m : morphism set_cat x y))
              (Hmono : IsMonomorphism (m : morphism set_cat x y))
          => (@isequiv_isepi_ismono_helper _ Hepi Hmono : @IsEquiv _ _ m)).
  admit.
  Undo.
  set (isequiv_isepimorphism_ismonomorphism'
       := fun `{Univalence}
              (Hepi : IsEpimorphism (m : morphism set_cat x y))
              (Hmono : IsMonomorphism (m : morphism set_cat x y))
          => ((let _ := @isequiv_isepimorphism_ismonomorphism _ Hepi Hmono in @isequiv_isepi_ismono _ fs0 x y m Hepi Hmono)
              : @IsEquiv _ _ m)).
  Set Printing Universes.
  admit. (* Error: Universe inconsistency (cannot enforce Top.235 <= Set because Set
< Top.235). *)

In trunk-polyproj, the Defined of isepi_issurj gives me an unsatisfied constraints error, and lists universe constraints, so I can't test if this bug is still open in trunk-polyproj.

[mattam82]

This one is very tricky. From what I gathered (after half an afternoon of debugging direcly in HoTT, I hadn't seen this nice simplified version), the problem looks serious. In isepiissurj, the level of the codomain binder of the [isepi f] proof is raised to something (say i) strictly larger than Set due to the use of (BuildhSet hProp ). Then then @paths terms in that lemma take equalities at levels larger or equal to this i, and this might make the inconsistency appear when trying to use it with equalities at lower levels (coming from the IsEpi/IsMono definitions). Does this make some sense?

[JasonGross]

It makes a tiny bit of sense, but I don't have a good idea about how to construct a smaller test case, nor a really good understanding of what's happening here, nor why. My current impression is "some universes are raised to above Set, then paths tries to use things larger than that universe, and things go wrong somewhere".

[mattam82]

Well, I'm wondering if the proof can even go through at all. From a deeper understanding, the first obstacle is that in isepi_issurj we're using the isepi hypothesis at an hset stricly higher than that of X, Y while the IsEpimorphism definition assumes X, Y and Z live in and hset at the same level, so there's no way we can unify those two.

[mattam82]

It seems to me resizing of the hProp for the hexists in h would be needed. If I put the minus1Trunc in Prop and use some clever lifting I can make it go through... Is there a reference to the book for this proof?

[JasonGross]

I'm not sure... I bet @mikeshulman would know (or would know who to ask).

[JasonGross]

I'm trying to do this with as few universes as possible. Could you tell me where Top.440 comes from in the following? It doesn't seem to be in the context, and doesn't show up in Show Universes. (Perhaps another bug?)

(* -*- coq-prog-args: ("-emacs" "-indices-matter") -*- *)
(* File reduced by coq-bug-finder from original input, then from 8249 lines to 907 lines, then from 843 lines to 357 lines, then from 351 lines to 260 lines, then from 208 lines to 162 lines, then from 167 lines to 154 lines *)
Set Universe Polymorphism.
Set Printing Universes.
Generalizable All Variables.
Reserved Notation "g 'o' f" (at level 40, left associativity).
Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
Arguments idpath {A a} , [A] a.
Class IsEquiv {A B : Type} (f : A -> B) := {}.
Class Contr_internal (A : Type) := { center : A ; contr : (forall y : A, center = y) }.
Inductive trunc_index : Type := minus_two | trunc_S (x : trunc_index).
Fixpoint nat_to_trunc_index (n : nat) : trunc_index
  := match n with
       | 0 => trunc_S (trunc_S minus_two)
       | S n' => trunc_S (nat_to_trunc_index n')
     end.
Coercion nat_to_trunc_index : nat >-> trunc_index.
Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
  match n with
    | minus_two => Contr_internal A
    | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y)
  end.
Notation minus_one:=(trunc_S minus_two).
Class IsTrunc (n : trunc_index) (A : Type) := Trunc_is_trunc : IsTrunc_internal n A.
Notation Contr := (IsTrunc minus_two).
Notation IsHProp := (IsTrunc minus_one).
Notation IsHSet := (IsTrunc 0).
Inductive Unit : Set := tt.
Instance contr_unit : IsTrunc@{i} minus_two Unit | 0 := {| center := tt;
                                                           contr := fun t : Unit => match t with tt => idpath end |}.
Instance trunc_succ `{IsTrunc n A} : IsTrunc (trunc_S n) A | 1000.
Admitted.
Record hProp := hp { hproptype :> Type ; isp : IsHProp hproptype}.
Definition Unit_hp:hProp@{i}:=(hp Unit _).
Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}.
Canonical Structure default_HSet:= fun T P => (@BuildhSet T P).
Definition ismono {X Y : Type@{i}} (f : X -> Y)
  := forall Z : hSet@{i},
     forall g h : Z -> X, (fun x => f (g x)) = (fun x => f (h x)) -> g = h.
Delimit Scope morphism_scope with morphism.
Delimit Scope category_scope with category.
Delimit Scope object_scope with object.
Record PreCategory :=
  { object :> Type;
    morphism : object -> object -> Type;
    compose : forall s d d', morphism d d' -> morphism s d -> morphism s d' }.
Infix "o" := (@compose _ _ _ _) : morphism_scope.
Local Open Scope morphism_scope.
Class IsEpimorphism {C} {x y} (m : morphism C x y) :=
  is_epimorphism : forall z (m1 m2 : morphism C y z),
                     m1 o m = m2 o m
                     -> m1 = m2.
Class IsMonomorphism {C} {x y} (m : morphism C x y) :=
  is_monomorphism : forall z (m1 m2 : morphism C z x),
                      m o m1 = m o m2
                      -> m1 = m2.
Global Instance isset_hProp : IsHSet hProp | 0. Admitted.

Definition set_cat : PreCategory
  := @Build_PreCategory hSet
                        (fun x y => forall _ : x, y)%core
                        (fun _ _ _ f g x => f (g x))%core.
Local Inductive minus1Trunc (A :Type) := min1 : A -> minus1Trunc A.
Instance minus1Trunc_is_prop {A : Type} : IsHProp (minus1Trunc A) | 0. Admitted.
Definition hexists {X} (P:X->Type):Type:= minus1Trunc (sigT  P).
Definition isepi {X Y : Type@{i}} `(f:X->Y) := forall Z: hSet@{i},
                                    forall g h: Y -> Z, (fun x => g (f x)) = (fun x => h (f x)) -> g = h.
Definition issurj {X Y : Type@{i}} (f:X->Y) := forall y:Y , hexists (fun x => (f x) = y).
Lemma isepi_issurj {X Y : Type@{i}} (f:X->Y): isepi@{i} f -> issurj@{i} f.
Proof.
  intros epif y.
  set (g :=fun _:Y => Unit_hp).
  set (h:=(fun y:Y => (hp (hexists (fun _ : Unit => {x:X & y = (f x)})) _ ))).
  hnf in epif.
  specialize (epif (BuildhSet hProp _) g).
  compute in *.
  Set Printing All.
  Show Universes.
  specialize (epif h).
  (* Toplevel input, characters 24-25:
Error:
In environment
X : Type@{Top.431}
Y : Type@{Top.431}
f : forall _ : X, Y
g := fun _ : Y =>
     hp@{Top.432} Unit
       (@trunc_succ@{Top.432} minus_two Unit
          (Build_Contr_internal@{Top.432} Unit tt
             (fun t : Unit =>
              match t as t0 return (@paths@{Top.432} Unit tt t0) with
              | tt => @idpath@{Top.432} Unit tt
              end))) : forall _ : Y, hProp@{Top.432}
epif : forall (h : forall _ : Y, hProp@{Top.432})
         (_ : @paths@{Top.431} (forall _ : X, hProp@{Top.432})
                (fun _ : X =>
                 hp@{Top.432} Unit
                   (@trunc_succ@{Top.432} minus_two Unit
                      (Build_Contr_internal@{Top.432} Unit tt
                         (fun t : Unit =>
                          match
                            t as t0 return (@paths@{Top.432} Unit tt t0)
                          with
                          | tt => @idpath@{Top.432} Unit tt
                          end)))) (fun x : X => h (f x))),
       @paths@{Top.431} (forall _ : Y, hProp@{Top.432})
         (fun _ : Y =>
          hp@{Top.432} Unit
            (@trunc_succ@{Top.432} minus_two Unit
               (Build_Contr_internal@{Top.432} Unit tt
                  (fun t : Unit =>
                   match t as t0 return (@paths@{Top.432} Unit tt t0) with
                   | tt => @idpath@{Top.432} Unit tt
                   end)))) h
y : Y
h := fun y0 : Y =>
     hp@{Top.437}
       (minus1Trunc@{Top.437}
          (@sigT Unit
             (fun _ : Unit =>
              @sigT X (fun x : X => @paths@{Top.438} Y y0 (f x)))))
       (@minus1Trunc_is_prop@{Top.437}
          (@sigT Unit
             (fun _ : Unit =>
              @sigT X (fun x : X => @paths@{Top.438} Y y0 (f x)))))
  : forall _ : Y, hProp@{Top.437}
The term "h" has type "forall _ : Y, hProp@{Top.437}"
while it is expected to have type "forall _ : Y, hProp@{Top.432}"
(Universe inconsistency: Cannot enforce Top.437 = Top.432 because Top.432
< Top.440 <= Top.435 <= Top.437)).
 *)

[mikeshulman]

The proof that epis are surjective is 10.1.4 in the book.

[JasonGross]

@mikeshulman, do you happen to know if it requires hpropositional resizing?

[mikeshulman]

I didn't think it did, but I haven't had time to re-read the proof to verify since seeing this discussion. @spitters might remember.

On Tue, Jun 17, 2014 at 4:54 PM, Jason Gross notifications@github.com wrote:

@mikeshulman https://github.com/mikeshulman, do you happen to know if it requires hpropositional resizing?

— Reply to this email directly or view it on GitHub https://github.com/HoTT/coq/issues/120#issuecomment-46380840.

[mattam82]

I guess @spitters knows indeed. Looking at the proofs in the book and the paper (Sets in HoTT), they both go through a pushout argument which seems to be missing from the formalization. However they point out the fact that making this predicative is tricky and refer to a paper by Wilander for a predicative proof. During the proof they do use the fact that hProp is an hSet (and recall latter on that is a “large” one indeed) but it’s in a slightly different manner than in the formalized proof. I think this might rely on the fact that the higher-inductive type encoding of pushouts avoids this size issue. — Matthieu

On 18 juin 2014, at 02:33, Mike Shulman notifications@github.com wrote:

I didn't think it did, but I haven't had time to re-read the proof to verify since seeing this discussion. @spitters might remember.

On Tue, Jun 17, 2014 at 4:54 PM, Jason Gross notifications@github.com wrote:

@mikeshulman https://github.com/mikeshulman, do you happen to know if it requires hpropositional resizing?

— Reply to this email directly or view it on GitHub https://github.com/HoTT/coq/issues/120#issuecomment-46380840.

— Reply to this email directly or view it on GitHub.

[spitters]

@mattam82 Indeed, as we say in the paper there are two proofs: one using a polymorphic Omega, the other using the mapping cone. The former one is formalized in Coq.

[spitters]

@mattam82 Indeed, there are two proofs. One using a polymorphic Omega, one using the mapping cone. The former is the one that I formalized.

[spitters]

After talking to @mattam82 yesterday, I think we now understand what is going on. The equivalence epis are surjective can be proved in regular categories. Regular categories are categories with a truncation/squash operator. We have truncation, and in fact it is small in the current implementation. In my proof I was using the universe polymorphic Omega. If we use the smallness of HITs, we can make it fit with the polmorphic theory of categories Jason is developing. The proof using the mapping cone does that.

On Wed, Jun 18, 2014 at 11:08 AM, Matthieu Sozeau notifications@github.com wrote:

I guess @spitters knows indeed. Looking at the proofs in the book and the paper (Sets in HoTT), they both go through a pushout argument which seems to be missing from the formalization. However they point out the fact that making this predicative is tricky and refer to a paper by Wilander for a predicative proof. During the proof they do use the fact that hProp is an hSet (and recall latter on that is a “large” one indeed) but it’s in a slightly different manner than in the formalized proof. I think this might rely on the fact that the higher-inductive type encoding of pushouts avoids this size issue. — Matthieu

On 18 juin 2014, at 02:33, Mike Shulman notifications@github.com wrote:

I didn't think it did, but I haven't had time to re-read the proof to verify since seeing this discussion. @spitters might remember.

On Tue, Jun 17, 2014 at 4:54 PM, Jason Gross notifications@github.com wrote:

@mikeshulman https://github.com/mikeshulman, do you happen to know if it requires hpropositional resizing?

— Reply to this email directly or view it on GitHub https://github.com/HoTT/coq/issues/120#issuecomment-46380840.

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub https://github.com/HoTT/coq/issues/120#issuecomment-46412115.