…-by-file-type-in-type

…-by-file-type-in-type

... so it includes -type-in-type only for the file Resizing2.v

On branch file-by-file-type-in-type

On branch file-by-file-type-in-type

and remove an unneeded axiom

On branch file-by-file-type-in-type

On branch file-by-file-type-in-type

On branch file-by-file-type-in-type

…-by-file-type-in-type

…-by-file-type-in-type

everything up to MoreFoundations/Subtypes.v compiles

... so we can make more progress on universe polymorphism

Build and you will see this:

    subtypeInjectivity_prop@{} =
    fun (A : Type@{i}) (B : forall _ : A, hProp)
      (x : total2@{i} (fun x : A => hProptoType (B x)))
      (y : total2@{i} (fun x0 : A => hProptoType (B x0))) =>
    subtypeInjectivity@{i i} (fun x0 : A => hProptoType (B x0))
      (fun x0 : A => propproperty (B x0)) x y
	 : forall (A : Type@{i}) (B : forall _ : A, hProp)
	     (x : total2@{i} (fun x : A => hProptoType (B x)))
	     (y : total2@{i} (fun x0 : A => hProptoType (B x0))),
	   weq@{i} (paths@{i} x y) (paths@{i} (pr1 x) (pr1 y))
    (*  |= i < UniMath.Foundations.Preamble.12
	   i <= uu1
	   i = uu0
	    *)

    subtypeInjectivity_prop is universe polymorphic
    Argument A is implicit and maximally inserted
    Argument scopes are [type_scope function_scope _ _]
    File "./UniMath/Foundations/Propositions.v", line 144, characters 34-35:
    Error:
    In environment
    X : Type@{uu1}
    The term "X" has type "Type@{uu1}" while it is expected to have type
     "Type@{i}" (universe inconsistency: Cannot enforce uu1 <= i because i
    < uu1).

The constraint i=uu0 is invalid and should have signalled a universe
inconsistency during the definition of subtypeInjectivity_prop.

packages working: Foundations, MoreFoundations

…-by-file-type-in-type

…-by-file-type-in-type

…-by-file-type-in-type

we've upgraded to the latest Coq from SkySkimmer/univ-cumul, but we
don't get as far, stopping with a new error in HLevels.v.  I've added
some comments temporarily at the point where it stops (line 185).

advanced further on branch SkySkimmer/univ-cumul
started using his new option Global Unset Cumulativity Use ULub.

…-by-file-type-in-type