hott / coq Goto Github PK

This project forked from coq/coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

Home Page: http://coq.inria.fr/

License: GNU Lesser General Public License v2.1

Emacs Lisp 0.04% Shell 0.06% OCaml 51.68% CSS 0.05% Coq 47.63% C 0.48% C++ 0.05% Verilog 0.01%

coq's Introduction

Homotopy Type Theory is an interpretation of Martin-Löf’s intensional type theory into abstract homotopy theory. Propositional equality is interpreted as homotopy and type isomorphism as homotopy equivalence. Logical constructions in type theory then correspond to homotopy-invariant constructions on spaces, while theorems and even proofs in the logical system inherit a homotopical meaning. As the natural logic of homotopy, type theory is also related to higher category theory as it is used e.g. in the notion of a higher topos.

The HoTT library is a development of homotopy-theoretic ideas in the Coq proof assistant. It draws many ideas from Vladimir Voevodsky's Foundations library (which has since been incorporated into the UniMath library) and also cross-pollinates with the HoTT-Agda library. See also: HoTT in Lean2, Spectral Sequences in Lean2, and Cubical Agda.

More information about this library can be found in:

The HoTT Library: A formalization of homotopy type theory in Coq, Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Mike Shulman, Matthieu Sozeau, Bas Spitters, 2016 arXiv CPP17

Other publications related to the library can be found here.

Installation

The HoTT library is part of the Coq Platform and can be installed using the installation instructions there.

More detailed installation instructions are provided in the file INSTALL.md.

Usage

The HoTT library can be used like any other Coq library. If you wish to use the HoTT library in your own project, make sure to put the following arguments in your _CoqProject file:

-arg -noinit
-arg -indices-matter

For more advanced use such as contribution see INSTALL.md.

We recommend the following text editors:

Emacs together with Proof General.
CoqIDE part of the Coq Proof Assistant.
Visual Studio Code together with VSCoq.

Other methods of developing in coq will work as long as the correct arguments are passed.

Contributing

Contributions to the HoTT library are very welcome! For style guidelines and further information, see the file STYLE.md.

Licensing

The library is released under the permissive BSD 2-clause license, see the file LICENSE.txt for further information. In brief, this means you can do whatever you like with it, as long as you preserve the Copyright messages. And of course, no warranty!

Wiki

More information can be found in the Wiki.

coq's People

Contributors

Stargazers

Watchers

Forkers

mdnahas solertis you13 kobi-prime wingsreal

coq's Issues

Type matching failure?

I have the following code

Set Implicit Arguments.

Generalizable All Variables.

Parameter SpecializedCategory : Type -> Type.
Parameter Object : forall obj, SpecializedCategory obj -> Type.

Section SpecializedFunctor.
  (* Variable objC : Type. *)
  Context `(C : SpecializedCategory objC).

  Polymorphic Record SpecializedFunctor := {
    ObjectOf' : objC -> Type;
    ObjectC : Object C
  }.
End SpecializedFunctor.

Section FunctorInterface.
  Variable objC : Type.
  Variable C : SpecializedCategory objC.
  Variable F : SpecializedFunctor C.

  Set Printing All.
  Set Printing Universes.
  Check @ObjectOf' objC C F.

The last line fails with

Toplevel input, characters 24-25:
Error:
In environment
objC : Type (* Top.515 *)
C : SpecializedCategory objC
F : @SpecializedFunctor (* Top.516 *) objC C
The term "F" has type "@SpecializedFunctor (* Top.516 *) objC C"
 while it is expected to have type
 "@SpecializedFunctor (* Top.519 Top.520 *) objC C".

If I uncomment out the first Variable objC : Type., or if I comment out the Polymorphic, or if I move the Context variable declaration to be a parameter of SpecializedFunctor (as in

Polymorphic Record SpecializedFunctor `(C : SpecializedCategory objC)

), then the Check goes through fine.

`split` fails with `Error: Refiner was given an argument "@SpecializedFunctor (* Set NaturalTransformation.283 Top.112 Top.113 ) (CardinalityRepresentative O) (NatCategory ( NaturalTransformation.283 ) O) objC C" of type "Type ( max(Set, Nat

This is in the following environment. I'll try to get a cleaner one soon, but I figured that the error message and environment might be enough to point you to the error

  objC : Type (* Top.112 *)
  C : SpecializedCategory (* Top.112 Top.113 *) objC
  ============================
   and
     (@eq
        (@SpecializedFunctor (* Set Functor.290 Set Functor.290 *)
           (CardinalityRepresentative (S O))
           (NatCategory (* Functor.290 *) (S O))
           (CardinalityRepresentative (S O))
           (NatCategory (* Functor.290 *) (S O)))
        (@ComposeFunctors (* Set Functor.290 Set Functor.290 Set
           Functor.290 *) (CardinalityRepresentative (S O))
           (NatCategory (* Functor.290 *) (S O))
           (@SpecializedFunctor (* Set NaturalTransformation.283 Top.112
              Top.113 *) (CardinalityRepresentative O)
              (NatCategory (* NaturalTransformation.283 *) O) objC C)
           (@FunctorCategory (* Set NaturalTransformation.283 Top.112 Top.113
              Set Functor.290 *) (CardinalityRepresentative O)
              (NatCategory (* NaturalTransformation.283 *) O) objC C)
           (CardinalityRepresentative (S O))
           (NatCategory (* Functor.290 *) (S O)) ExponentialLaw0Functor
           (* Set Functor.290 Functor.290 NaturalTransformation.283 *)
           ExponentialLaw0Functor_Inverse (* Functor.290 Set Functor.290
           NaturalTransformation.283 Set Set Top.244 *))
        (@IdentityFunctor (* Set Functor.290 *)
           (CardinalityRepresentative (S O))
           (NatCategory (* Functor.290 *) (S O))))
     (@eq
        (@SpecializedFunctor (* Set Functor.290 Set Functor.290 *)
           (@SpecializedFunctor (* Set NaturalTransformation.283 Top.112
              Top.113 *) (CardinalityRepresentative O)
              (NatCategory (* NaturalTransformation.283 *) O) objC C)
           (@FunctorCategory (* Set NaturalTransformation.283 Top.112 Top.113
              Set Functor.290 *) (CardinalityRepresentative O)
              (NatCategory (* NaturalTransformation.283 *) O) objC C)
           (@SpecializedFunctor (* Set NaturalTransformation.283 Top.112
              Top.113 *) (CardinalityRepresentative O)
              (NatCategory (* NaturalTransformation.283 *) O) objC C)
           (@FunctorCategory (* Set NaturalTransformation.283 Top.112 Top.113
              Set Functor.290 *) (CardinalityRepresentative O)
              (NatCategory (* NaturalTransformation.283 *) O) objC C))
        (@ComposeFunctors (* Set Functor.290 Set Functor.290 Set
           Functor.290 *)
           (@SpecializedFunctor (* Set NaturalTransformation.283 Top.112
              Top.113 *) (CardinalityRepresentative O)
              (NatCategory (* NaturalTransformation.283 *) O) objC C)
           (@FunctorCategory (* Set NaturalTransformation.283 Top.112 Top.113
              Set Functor.290 *) (CardinalityRepresentative O)
              (NatCategory (* NaturalTransformation.283 *) O) objC C)
           (CardinalityRepresentative (S O))
           (NatCategory (* Functor.290 *) (S O))
           (@SpecializedFunctor (* Set NaturalTransformation.283 Top.112
              Top.113 *) (CardinalityRepresentative O)
              (NatCategory (* NaturalTransformation.283 *) O) objC C)
           (@FunctorCategory (* Set NaturalTransformation.283 Top.112 Top.113
              Set Functor.290 *) (CardinalityRepresentative O)
              (NatCategory (* NaturalTransformation.283 *) O) objC C)
           ExponentialLaw0Functor_Inverse (* Functor.290 Set Functor.290
           NaturalTransformation.283 Set Set Top.259 *)
           ExponentialLaw0Functor (* Set Functor.290 Functor.290
           NaturalTransformation.283 *))
        (@IdentityFunctor (* Set Functor.290 *)
           (@SpecializedFunctor (* Set NaturalTransformation.283 Top.112
              Top.113 *) (CardinalityRepresentative O)
              (NatCategory (* NaturalTransformation.283 *) O) objC C)
           (@FunctorCategory (* Set NaturalTransformation.283 Top.112 Top.113
              Set Functor.290 *) (CardinalityRepresentative O)

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

The fix for #50 didn't fix my underlying problem, unfortunately. Although the code I gave there now compiles, the extended code doesn't. Here's a close-to-original version:

Require Import HoTT.HoTT.
Set Printing Universes.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Universe Polymorphism.

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

    Identity : forall x, Morphism x x;
    Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d' where "f 'o' g" := (Compose f g);

    Associativity : forall x1 x2 x3 x4
                           (m1 : Morphism x1 x2)
                           (m2 : Morphism x2 x3)
                           (m3 : Morphism x3 x4),
                      (m3 o m2) o m1 = m3 o (m2 o m1);

    LeftIdentity : forall a b (f : Morphism a b), (Identity b) o f = f;
    RightIdentity : forall a b (f : Morphism a b), f o (Identity a) = f;

    MorphismIsHSet : forall s d, IsHSet (Morphism s d)
  }.

Local Open Scope equiv_scope.

Section Groupoid.
  Variable X : Type.
  Context `{IsTrunc 0 X}.

  Local Notation Groupoid_Morphism := (@paths X).

  Definition Groupoid_Compose s d d' (m : Groupoid_Morphism d d') (m' : Groupoid_Morphism s d)
  : Groupoid_Morphism s d'
    := transitivity s d d' m' m.

  Definition Groupoid_Identity x : Groupoid_Morphism x x
    := reflexivity _.

  Global Arguments Groupoid_Compose [s d d'] m m' / .
  Global Arguments Groupoid_Identity x / .

  Definition DiscreteCategory : PreCategory.
    refine (@Build_PreCategory X
                               Groupoid_Morphism
                               Groupoid_Identity
                               Groupoid_Compose
                               _
                               _
                               _
                               _);
    admit. (*simpl; intros; path_induction; reflexivity.*)
  Defined.
End Groupoid.

Arguments DiscreteCategory _.

Definition IndiscreteCategory X : PreCategory
  := @Build_PreCategory X
                         (fun _ _ => Unit)
                         (fun _ => tt)
                         (fun _ _ _ _ _ => tt)
                         (fun _ _ _ _ _ _ _ => idpath)
                         (fun _ _ f => match f with tt => idpath end)
                         (fun _ _ f => match f with tt => idpath end)
                         _.

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

I'll attach a minimized version soon.

focusing problem

The proof below, based on the current github.com/HoTT/HoTT library, fails with this output from "hoqc" (compiled today from the latest sources):

$ hoqc IsEquivAp.v 
File "./IsEquivAp.v", line 29, characters 8-9:
Error: This proof is focused, but cannot be unfocused this way

Removing all the focusing bullets makes the proof work. Older versions of coq work.

Any ideas?

Require Import Overture PathGroupoids Equivalences.
Local Open Scope path_scope.
Local Open Scope equiv_scope.
Generalizable Variables A B e.

(* Redefine this tactic to be a bit fancier *)
Ltac path_via mid :=
  apply @concat with (y := mid); 
  repeat progress first [
  apply whiskerL
| apply whiskerR
| apply @ap
]; auto with path_hints.
Hint Resolve @ap_pp @ap_idmap : path_hints.

Instance isequiv_ap1 `{IsEquiv A B e} (x y : A)
  : IsEquiv (@ap A B e x y).
Proof.    
  apply isequiv_adjointify with
(fun p => (eissect e x)^ @ ap (e ^-1) p @ eissect e y);
  intro p.
  - path_via (ap e ((eissect e x) ^ @ ap e ^-1 p) @ ap e (eissect e y)).
path_via ((ap e (eissect e x) ^ @ ap e (ap e ^-1 p)) @ ap e (eissect e y)).  
path_via (ap e (eissect e x) ^ @ (ap e (ap e ^-1 p) @ ap e (eissect e y))).
path_via (ap e (eissect e x) ^ @ ((eisretr e (e x)) @ p)).
+ path_via (ap e (ap e ^-1 p) @ (eisretr e (e y))).
  * by apply symmetry, eisadj.
  * path_via (ap (compose e (e ^-1)) p @ (eisretr e (e y))).
    - by apply symmetry, (ap_compose (e ^-1) e p).
    - path_via (eisretr e (e x) @ (ap (idmap) p)).
      by apply (concat_Ap (eisretr e)).
+ path_via ((ap e (eissect e x) ^ @ eisretr e (e x)) @ p).
  path_via (1 @ p).
  path_via (ap e (eissect e x) ^ @ ap e (eissect e x)). 
  * by apply eisadj.
  * path_via (ap e ((eissect e x) ^ @ eissect e x)).
    change (idpath (e x)) with (ap e (idpath x)).
    by apply ap, concat_Vp.
  - destruct p. simpl.
path_via ((eissect e x)^ @ eissect e x).
apply concat_Vp.
Defined.

Anomaly: Mismatched instance and context when building universe substitution. Please report.

SearchAbout and. gives Anomaly: Mismatched instance and context when building universe substitution. Please report.

Anomaly: Evar was not declared. Please report

Example file in this repo.

`Polymorphic Coercion` and `Polymorphic Identity Coercion`?

Sometimes Polymorphic Coercion and Polymorphic Identity Coercion work fine. Other times, I get an Syntax error: '.' or '...' expected after [tactic:tactic] (in [proof_mode:subgoal_command]). error. Are Coercions supposed to take the Polymorphic flag? (If need be, I can try to get some code that reproduces each case, but I'm not hopeful, as the treatment of these seems to vary between coq runs.)

Type parameter becomes Prop

The following used to work in Coq 8.4, but fails to work in HoTT/coq:

Class Inhabited (A : Type) : Prop := populate { _ : A }.
Arguments populate {_} _.

Instance prod_inhabited {A B : Type} (iA : Inhabited A)
   (iB : Inhabited B) :   Inhabited (A * B) :=
  match iA, iB with
  | populate x, populate y => populate (x,y)
  end.

it yields the error

Error: In environment
A : Type
B : Type
iA : Inhabited A
iB : Inhabited B
The term "(A * B)%type" has type "Type" while it is expected to have type 
"Prop".

If I Print inhabited, it shows that the type parameter A, which should have type Type, has gotten type Prop

Query commands should not be inserted in scripts
Record Inhabited (A : Prop) : Prop := populate { _ : A }

For populate: Argument A is implicit and maximally inserted
For Inhabited: Argument scope is [type_scope]
For populate: Argument scopes are [type_scope _]

`make check` fails

$ make check
make --warn-undefined-variable --no-builtin-rules -f Makefile.build "check"
make[1]: Entering directory `/afs/csail.mit.edu/u/j/jgross/coq'
COQCHK <theories & plugins>
Failure: vo structure validation failed. Please report.
make[1]: *** [validate] Error 1
make[1]: Leaving directory `/afs/csail.mit.edu/u/j/jgross/coq'
make: *** [check] Error

-indices-matter causes universe inconsistency

The following proof script checks fine when indices-matter is disabled, but gives an error when it is turned on.

Inductive Empty : Type :=.

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

Notation "x = y :> A" := (@paths A x y) : type_scope.
Notation "x = y" := (x = y :>_) : type_scope.

Arguments idpath {A a} , [A] a.

Definition idmap {A : Type} : A -> A := fun x => x.

Definition path_sum {A B : Type} (z z' : A + B)
           (pq : match z, z' with
                   | inl z0, inl z'0 => z0 = z'0
                   | inr z0, inr z'0 => z0 = z'0
                   | _, _ => Empty
                 end)
: z = z'.
  destruct z, z', pq; exact idpath.
Defined.

Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
  := match p with idpath => idpath end.

Theorem ex2_8 {A B A' B' : Type} (g : A -> A') (h : B -> B') (x y : A + B)
              (* Fortunately, this unifies properly *)
              (pq : match (x, y) with (inl x', inl y') => x' = y' | (inr x', inr y') => x' = y' | _ => Empty end) :
  let f z := match z with inl z' => inl (g z') | inr z' => inr (h z') end in
  ap f (path_sum x y pq) = path_sum (f x) (f y)
     (* Coq appears to require *ALL* of the annotations *)
     ((match x as x return match (x, y) with
              (inl x', inl y') => x' = y'
            | (inr x', inr y') => x' = y'
            | _ => Empty
          end -> match (f x, f y) with
               | (inl x', inl y') => x' = y'
               | (inr x', inr y') => x' = y'
               | _ => Empty end with
           | inl x' => match y as y return match y with
                                               inl y' => x' = y'
                                             | _ => Empty
                                           end -> match f y with
                                                    | inl y' => g x' = y'
                                                    | _ => Empty end with
                         | inl y' => ap g
                         | inr y' => idmap
                       end
           | inr x' => match y as y return match y with
                                               inr y' => x' = y'
                                             | _ => Empty
                                           end -> match f y with
                                                    | inr y' => h x' = y'
                                                    | _ => Empty end with
                         | inl y' => idmap
                         | inr y' => ap h
                       end
       end) pq).
  destruct x; destruct y; destruct pq; reflexivity.
Qed.

The error is this:

Toplevel input, characters 1367-1374:
Error:
In environment
A : Type
B : Type
A' : Type
B' : Type
g : A -> A'
h : B -> B'
x : A + B
y : A + B
pq :
match x with
| inl x' => match y with
            | inl y' => x' = y'
            | inr _ => Empty
            end
| inr x' => match y with
            | inl _ => Empty
            | inr y' => x' = y'
            end
end
f :=
fun z : A + B =>
match z with
| inl z' => inl (g z')
| inr z' => inr (h z')
end : A + B -> A' + B'
x' : B
y0 : A + B
y' : B
The term "x' = y'" has type "Type" while it is expected to have type 
"Prop" (Universe inconsistency).

This bug might be related to #53 (comment)

`split` fails with `Error: Refiner was given an argument "(objC * 0)%type" of type "Type" instead of "Set".`

The code at https://gist.github.com/JasonGross/4956482 gives me a failure on split with Error: Refiner was given an argument "(objC * 0)%type" of type "Type" instead of "Set". I think this is different from issue #7 , since the split code there seems to work now. I'll try to trim this down shortly.

Unification algorithm does not work up to beta-convertibility

Both of the following definitions succeed in Coq 8.4. The second one fails in tip with

Toplevel input, characters 131-138:
Error:
In environment
s : Prop
d : Prop
The term
 "@eq_refl Set (forall _ : (fun x : Set => x) s, (fun x : Set => x) d)"
has type "@eq Set (forall _ : s, d) (forall _ : s, d)"
while it is expected to have type
 "@eq Set (forall _ : s, d) (forall _ : s, d)"
(cannot unify "forall _ : (fun x : Set => x) s, (fun x : Set => x) d" and
"forall _ : (fun x : Prop => x) s, (fun x : Prop => x) d").

Definition foo (s d : Prop)
 : ((s : Set) -> (d : Set)) = ((s : Prop) -> (d : Prop))
 := eq_refl. (* succeeds *)
Definition foo (s d : Prop)
 : ((fun x : Set => x) s -> (fun x : Set => x) d) = ((fun x : Prop => x) s -> (fun x : Prop => x) d)
 := eq_refl. (* fails *)

I can also get the error

The term "m" has type "Morphism PropCat s d"
while it is expected to have type "Morphism SetCat s d"
(cannot unify "(fun x : Set => x) s" and "(fun x : Prop => x) s").

Most recent commit broke `Fixpoint`s in `Set`

Set Printing Universes.
Fixpoint CardinalityRepresentative (n : nat) : Set :=
  match n with
    | O => Empty_set
    | S n' => sum (CardinalityRepresentative n') unit
  end.
(* Toplevel input, characters 104-143:
Error:
In environment
CardinalityRepresentative : nat -> Set
n : nat
n' : nat
The term "(CardinalityRepresentative n' + unit)%type" has type
 "Type (* max(Top.73, Top.74) *)" while it is expected to have type
"Set". *)

I suspect this has something to do with the fact that Check (nat : Type) : Set. used to work in HoTT/coq, but now gives

Toplevel input, characters 22-32:
Error:
The term "nat:Type (* Top.11 *)" has type "Type (* Top.11 *)"
while it is expected to have type "Set" (Universe inconsistency).

Anomaly: Uncaught exception Reduction.NotConvertible. Please report.

The following code generates Anomaly: Uncaught exception Reduction.NotConvertible. Please report.:

Record Foo : Set :=
  {
    A' : nat;
    A : Prop := (A' = 0)
  }.

Removing the : Set makes it compile, but places Foo in Type (* (Set)+1 *). In Coq 8.4, the inferred universe level is Type (* Set *).

`change` seems to break polymorphism, gives a universe inconsistency

The following code works in coq 8.4, but not in HoTT/coq:

Set Implicit Arguments.
Set Universe Polymorphism.
Generalizable All Variables.

Record SpecializedCategory (obj : Type) :=
  {
    Object :> _ := obj
  }.

Record > Category :=
  {
    CObject : Type;
    UnderlyingCategory :> @SpecializedCategory CObject
  }.

Record SpecializedFunctor `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) :=
  {
    ObjectOf :> objC -> objD
  }.

Definition Functor (C D : Category) := SpecializedFunctor C D.

Parameter TerminalCategory : SpecializedCategory unit.

Definition focus A (_ : A) := True.

Definition CommaCategory_Object (A : Category) (S : Functor TerminalCategory A) : Type.
  assert (Hf : focus ((S tt) = (S tt))) by constructor.
  progress change CObject with (fun C => @Object (CObject C) C) in *;
    simpl in *.
  match type of Hf with
    | focus ?V => exact V
  end.
Defined.

Definition Build_SliceCategory (A : Category) (F : Functor TerminalCategory A) := @Build_SpecializedCategory (CommaCategory_Object F).
Parameter SetCat : @SpecializedCategory Set.

Set Printing Universes.
Check (fun (A : Category) (F : Functor TerminalCategory A) => @Build_SpecializedCategory (CommaCategory_Object F)) SetCat.
(* (fun (A : Category (* Top.68 *))
   (F : Functor (* Set Top.68 *) TerminalCategory A) =>
 {|  |}) SetCat (* Top.68 *)
     : forall
         F : Functor (* Set Top.68 *) TerminalCategory SetCat (* Top.68 *),
       let Object := CommaCategory_Object (* Top.68 Top.69 Top.68 *) F in
       SpecializedCategory (* Top.69 *)
         (CommaCategory_Object (* Top.68 Top.69 Top.68 *) F) *)
Check @Build_SliceCategory SetCat. (* Toplevel input, characters 0-34:
Error: Universe inconsistency (cannot enforce Top.51 <= Set because Set
< Top.51). *)

Anomaly when declaring canonical structures

(Working over b07e5d7, i.e. current stable branch.)

Declaring certain canonical structures fails, with “Anomaly: Mismatched instance and context when building universe substitution. Please report.” The smallest example I’ve found is:

Record Type_Over (X : Type) 
:= { Domain :> Type;
     proj : Domain -> X }.

Definition Self_Over (X : Type)
  := {| Domain := X; proj := (fun x => x) |}.

Canonical Structure Self_Over. (* fails *)

If Self_Over is changed to a monomorphic definition, then the Canonical Structure declaration still fails but with a different error: “Warning: No global reference exists for projection valuefun x : _UNBOUND_REL_1 => x in instance Self_Over of proj, ignoring it.”

As best as I can conjecture, this error seems to occur just when the record has a type parameter.

More troubles with type inference and [Prop]

This code fails in HoTT/Coq, but does not if I remove the change (present_obj) or intros lines:

Set Implicit Arguments.

Generalizable All Variables.

Set Asymmetric Patterns.

Polymorphic Record Category (obj : Type) :=
  Build_Category {
      Object :> _ := obj;
      Morphism : obj -> obj -> Type;

      Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
    }.

Polymorphic Record Functor objC (C : Category objC) objD (D : Category objD) :=
  { ObjectOf :> objC -> objD }.

Polymorphic Record NaturalTransformation objC C objD D (F G : Functor (objC := objC) C (objD := objD) D) :=
  { ComponentsOf' :> forall c, D.(Morphism) (F.(ObjectOf) c) (G.(ObjectOf) c);
    Commutes' : forall s d (m : C.(Morphism) s d), ComponentsOf' s = ComponentsOf' s }.

Ltac present_obj from to :=
  repeat match goal with
           | [ _ : appcontext[from ?obj ?C] |- _ ] => progress change (from obj C) with (to obj C) in *
           | [ |- appcontext[from ?obj ?C] ] => progress change (from obj C) with (to obj C) in *
         end.

Section NaturalTransformationComposition.
  Context `(C : @Category objC).
  Context `(D : @Category objD).
  Context `(E : @Category objE).
  Variables F F' F'' : Functor C D.

  Polymorphic Definition NTComposeT (T' : NaturalTransformation F' F'') (T : NaturalTransformation F F') :
    NaturalTransformation F F''.
    exists (fun c => Compose _ _ _ _ (T' c) (T c)).
    progress present_obj @Morphism @Morphism. (* removing this line makes the error go away *)
    intros. (* removing this line makes the error go away *)
    admit.
  Defined.
End NaturalTransformationComposition.


Polymorphic Definition FunctorCategory objC (C : Category objC) objD (D : Category objD) :
  @Category (Functor C D)
  := @Build_Category (Functor C D)
                     (NaturalTransformation (C := C) (D := D))
                     (NTComposeT (C := C) (D := D)).

Definition Cat0 : Category Empty_set
  := @Build_Category Empty_set
                     (@eq _)
                     (fun x => match x return _ with end).

Polymorphic Definition FunctorFrom0 objC (C : Category objC) : Functor Cat0 C
  := Build_Functor Cat0 C (fun x => match x with end).

Section Law0.
  Variable objC : Type.
  Variable C : Category objC.

  Set Printing All.
  Set Printing Universes.
  Set Printing Existential Instances.

  Polymorphic Definition ExponentialLaw0Functor_Inverse_ObjectOf : Object (FunctorCategory Cat0 C).
    hnf.
    refine (@FunctorFrom0 _ _).
    (* Toplevel input, characters 23-40:
Error:
In environment
objC : Type (* Top.61069 *)
C : Category (* Top.61069 Top.61071 *) objC
The term
 "@FunctorFrom0 (* Top.61077 Top.61078 *) ?69 (* [objC, C] *)
    ?70 (* [objC, C] *)" has type
 "@Functor (* Set Prop Top.61077 Top.61078 *) Empty_set Cat0
    ?69 (* [objC, C] *) ?70 (* [objC, C] *)"
 while it is expected to have type
 "@Functor (* Set Prop Set Prop *) Empty_set Cat0 objC C".
*)

Anomaly: apply_coercion. Please report.

Generated by:

Set Implicit Arguments.

Generalizable All Variables.

Polymorphic Record SpecializedCategory (obj : Type) := Build_SpecializedCategory' {
  Object :> _ := obj;
  Morphism' : obj -> obj -> Type;

  Identity' : forall o, Morphism' o o;
  Compose' : forall s d d', Morphism' d d' -> Morphism' s d -> Morphism' s d'
}.

Polymorphic Definition Morphism obj (C : @SpecializedCategory obj) : forall s d : C, _ := Eval cbv beta delta [Morphism'] in C.(Morphism').

(* eh, I'm not terribly happy.  meh. *)
Polymorphic Definition SmallSpecializedCategory (obj : Set) (*mor : obj -> obj -> Set*) := SpecializedCategory obj.
Identity Coercion SmallSpecializedCategory_LocallySmallSpecializedCategory_Id : SmallSpecializedCategory >-> SpecializedCategory.

Polymorphic Record Category := {
  CObject : Type;

  UnderlyingCategory :> @SpecializedCategory CObject
}.

Polymorphic Definition GeneralizeCategory `(C : @SpecializedCategory obj) : Category.
  refine {| CObject := C.(Object) |}; auto.
Defined.

Coercion GeneralizeCategory : SpecializedCategory >-> Category.



Section SpecializedFunctor.
  Context `(C : @SpecializedCategory objC).
  Context `(D : @SpecializedCategory objD).

  Polymorphic Record SpecializedFunctor := {
    ObjectOf' : objC -> objD;
    MorphismOf' : forall s d, C.(Morphism') s d -> D.(Morphism') (ObjectOf' s) (ObjectOf' d);
    FCompositionOf' : forall s d d' (m1 : C.(Morphism') s d) (m2: C.(Morphism') d d'),
      MorphismOf' _ _ (C.(Compose') _ _ _ m2 m1) = D.(Compose') _ _ _ (MorphismOf' _ _ m2) (MorphismOf' _ _ m1);
    FIdentityOf' : forall o, MorphismOf' _ _ (C.(Identity') o) = D.(Identity') (ObjectOf' o)
  }.
End SpecializedFunctor.

Global Coercion ObjectOf' : SpecializedFunctor >-> Funclass.

Section Functor.
  Variable C D : Category.

  Polymorphic Definition Functor := SpecializedFunctor C D.
End Functor.

Identity Coercion Functor_SpecializedFunctor_Id : Functor >-> SpecializedFunctor.
Polymorphic Definition GeneralizeFunctor objC C objD D (F : @SpecializedFunctor objC C objD D) : Functor C D := F.
Coercion GeneralizeFunctor : SpecializedFunctor >-> Functor.

Arguments SpecializedFunctor {objC} C {objD} D.


Polymorphic Record SmallCategory := {
  SObject : Set;

  SUnderlyingCategory :> @SmallSpecializedCategory SObject
}.

Polymorphic Definition GeneralizeSmallCategory `(C : @SmallSpecializedCategory obj) : SmallCategory.
  refine {| SObject := obj |}; destruct C; econstructor; eassumption.
Defined.

Coercion GeneralizeSmallCategory : SmallSpecializedCategory >-> SmallCategory.

Bind Scope category_scope with SmallCategory.


Polymorphic Definition TypeCat : @SpecializedCategory Type := (@Build_SpecializedCategory' Type
                                                                                          (fun s d => s -> d)
                                                                                          (fun _ => (fun x => x))
                                                                                          (fun _ _ _ f g => (fun x => f (g x)))).

Polymorphic Definition FunctorCategory objC (C : @SpecializedCategory objC) objD (D : @SpecializedCategory objD) :
  @SpecializedCategory (SpecializedFunctor C D).
Admitted.

Polymorphic Definition DiscreteCategory (O : Type) : @SpecializedCategory O.
Admitted.

Polymorphic Definition ComputableCategory (I : Type) (Index2Object : I -> Type) (Index2Cat : forall i : I, @SpecializedCategory (@Index2Object i)) :
  @SpecializedCategory I.
Admitted.

Polymorphic Definition is_unique (A : Type) (x : A) := forall x' : A, x' = x.

Polymorphic Definition InitialObject obj {C : SpecializedCategory obj} (o : C) :=
    forall o', { m : C.(Morphism) o o' | is_unique m }.

Polymorphic Definition SmallCat := ComputableCategory _ SUnderlyingCategory.

Lemma InitialCategory_Initial : InitialObject (C := SmallCat) (DiscreteCategory Empty_set : SmallSpecializedCategory _).
  admit.
Qed.


Section GraphObj.
  Context `(C : @SpecializedCategory objC).

  Inductive GraphIndex := GraphIndexSource | GraphIndexTarget.

  Polymorphic Definition GraphIndex_Morphism (a b : GraphIndex) : Set :=
    match (a, b) with
      | (GraphIndexSource, GraphIndexSource) => unit
      | (GraphIndexTarget, GraphIndexTarget) => unit
      | (GraphIndexTarget, GraphIndexSource) => Empty_set
      | (GraphIndexSource, GraphIndexTarget) => GraphIndex
    end.

  Global Arguments GraphIndex_Morphism a b /.

  Polymorphic Definition GraphIndex_Compose s d d' (m1 : GraphIndex_Morphism d d') (m2 : GraphIndex_Morphism s d) :
    GraphIndex_Morphism s d'.
  Admitted.

  Polymorphic Definition GraphIndexingCategory : @SpecializedCategory GraphIndex.
    refine {|
      Morphism' := GraphIndex_Morphism;
      Identity' := (fun x => match x with GraphIndexSource => tt | GraphIndexTarget => tt end);
      Compose' := GraphIndex_Compose
    |};
    admit.
  Defined.

  Polymorphic Definition UnderlyingGraph_ObjectOf x :=
    match x with
      | GraphIndexSource => { sd : objC * objC & C.(Morphism) (fst sd) (snd sd) }
      | GraphIndexTarget => objC
    end.

  Global Arguments UnderlyingGraph_ObjectOf x /.

  Polymorphic Definition UnderlyingGraph_MorphismOf s d (m : Morphism GraphIndexingCategory s d) :
    UnderlyingGraph_ObjectOf s -> UnderlyingGraph_ObjectOf d.
  Admitted.

  Polymorphic Definition UnderlyingGraph : SpecializedFunctor GraphIndexingCategory TypeCat.
  Proof.
    match goal with
      | [ |- SpecializedFunctor ?C ?D ] =>
        refine (Build_SpecializedFunctor C D
          UnderlyingGraph_ObjectOf
          UnderlyingGraph_MorphismOf
          _
          _
        )
    end;
    admit.
  Defined.
End GraphObj.


Polymorphic Definition UnderlyingGraphFunctor_MorphismOf (C D : SmallCategory) (F : SpecializedFunctor C D) :
  Morphism (FunctorCategory TypeCat GraphIndexingCategory) (UnderlyingGraph C) (UnderlyingGraph D).

Sorry it's so long.

Some bugs: slowness, universe inconsistencies, and anomalies

The new version has fixed most of the problems I was having with my category theory library. Great work!

There still seem to be a few bugs, though. When I apply the patch at https://gist.github.com/JasonGross/5308008 to the tip (ede8193) of https://bitbucket.org/JasonGross/catdb, I get the following output. Some of these are probably just minor incompatibilities (for example, Build_Equivalence now takes one fewer explicit argument than it did in Coq 8.4) that I haven't gotten around to tracking down yet. However, the anomaly and the error on case H are probably actual bugs. The problem in Grothendieck.v seems to be related to Identity Coercions; do these coercions fix universe levels which don't need to be fixed? The universe inconsistencies are also worrying, given that I've Set Universe Polymorphism in all of my files. Additionally, InducedLimitFunctors is much slower to compile (from 2.5 minutes to 32 minutes), as is CommaCategoryFunctors (from 8.5 minutes to more than 19 minutes). I'll be creating individual issues with small reproducing cases for these bugs as I have time over the next few days, but I figured I'd put them all here in case you want to tackle them before I get a chance to make smaller test cases.

"coqc"  -q  -I .  -dont-load-proofs  EnrichedCategory
"coqc"  -q  -I .  -dont-load-proofs  CommaCategoryFunctors
"coqc"  -q  -I .  -dont-load-proofs  DecidableDiscreteCategoryFunctors
"coqc"  -q  -I .  -dont-load-proofs  InducedLimitFunctors
"coqc"  -q  -I .  -dont-load-proofs  CoendFunctor
"coqc"  -q  -I .  -dont-load-proofs  Grothendieck
"coqc"  -q  -I .  -dont-load-proofs  Yoneda
"coqc"  -q  -I .  -dont-load-proofs  Examples
File "./EnrichedCategory.v", line 24, characters 2-34:
Anomaly: apply_coercion_args: mismatch between arguments and coercion.
Please report.
make[1]: *** [EnrichedCategory.vo] Error 1
File "./Grothendieck.v", line 114, characters 2-193:
Error: Illegal application:
The term "ObjectOf" of type
 "forall (objC : Type) (C : SpecializedCategory objC)
    (objD : Type) (D : SpecializedCategory objD),
  SpecializedFunctor C D -> objC -> objD"
cannot be applied to the terms
 "objC" : "Type"
 "C" : "SpecializedCategory objC"
 "Type" : "Type"
 "TypeCat" : "SpecializedCategory Set"
 "F'" : "SpecializedFunctorToType C"
 "SetGrothendieckC' G" : "objC"
The 5th term has type "SpecializedFunctorToType C"
which should be coercible to "SpecializedFunctor C TypeCat".
make[1]: *** [Grothendieck.vo] Error 1
File "./Yoneda.v", line 161, characters 2-63:
Error: Universe inconsistency.
make[1]: *** [Yoneda.vo] Error 1
File "./DecidableDiscreteCategoryFunctors.v", line 112, characters 4-5:
In nested Ltac calls to "t" and "case H", last call failed.
Error: Cannot instantiate metavariable P of type
"forall a : O, x = a -> Prop" with abstraction
"fun (x : O) (e : x = x) =>
 match eq_sym e in (_ = y) return (Morphism O' (f y) (f x)) with
 | eq_refl => Identity (f x)
 end = Identity (f x)" of incompatible type "forall x : O, x = x -> Prop".
make[1]: *** [DecidableDiscreteCategoryFunctors.vo] Error 1
File "./Examples.v", line 236, characters 2-138:
Error: Proof is not complete.
make[1]: *** [Examples.vo] Error 1
File "./CoendFunctor.v", line 108, characters 4-830:
Error: Proof is not complete.
make[1]: *** [CoendFunctor.vo] Error 1
Finished transaction in 280.631 secs (280.629u,0.016s)
File "./CommaCategoryFunctors.v", line 364, characters 2-6:
Error: Universe inconsistency.
make[1]: *** [CommaCategoryFunctors.vo] Error 1

Anomaly: Uncaught exception Reductionops.NotASort(_). Please report.

The code

Require Import FunctionalExtensionality.

Goal forall y, @f_equal = y.
intro.
apply functional_extensionality_dep.

causes

Toplevel input, characters 15-50:
Anomaly: Uncaught exception Reductionops.NotASort(_). Please report.
frame @ file "toplevel/vernac.ml", line 343, characters 6-16
raise @ file "toplevel/vernac.ml", line 335, characters 18-25
frame @ file "toplevel/vernac.ml", line 327, characters 14-104
raise @ file "library/states.ml", line 40, characters 45-46
frame @ file "tactics/tacinterp.ml", line 72, characters 6-11
frame @ file "proofs/refiner.ml", line 429, characters 14-49
frame @ file "proofs/refiner.ml", line 107, characters 13-78
frame @ file "proofs/refiner.ml", line 85, characters 6-134
frame @ file "lib/cList.ml", line 290, characters 19-24
frame @ file "proofs/refiner.ml", line 43, characters 16-35
raise @ unknown
frame @ file "tactics/tactics.ml", line 992, characters 10-39
frame @ file "proofs/clenvtac.ml", line 80, characters 26-66
frame @ file "proofs/clenv.ml", line 283, characters 12-58
frame @ file "pretyping/unification.ml", line 1012, characters 12-47
frame @ file "pretyping/unification.ml", line 901, characters 14-83
frame @ file "pretyping/unification.ml", line 862, characters 8-72
raise @ unknown
frame @ file "pretyping/evarsolve.ml", line 1404, characters 10-69
raise @ unknown
frame @ file "pretyping/evarsolve.ml", line 1329, characters 15-58
raise @ unknown
frame @ file "pretyping/evarsolve.ml", line 1047, characters 8-53
frame @ file "pretyping/retyping.ml", line 94, characters 28-68
frame @ file "pretyping/retyping.ml", line 106, characters 32-50
frame @ file "pretyping/retyping.ml", line 114, characters 31-70
frame @ file "pretyping/retyping.ml", line 114, characters 16-29
frame @ file "pretyping/retyping.ml", line 114, characters 16-29
raise @ file "pretyping/reductionops.ml", line 973, characters 15-23

If I manually instantiate the first parameter (if I do apply (@functional_extensionality_dep Type).), then it works fine.

Error: There is an inductive name deep in a "in" clause.

The following code generates Error: There is an inductive name deep in a "in" clause. in the trunk version of HoTT/coq, but executes fine in v8.4:

Require Import Omega.
Theorem foo : forall (n m : nat) (pf : n = m),
                match pf in _ = N with 
                  | eq_refl => unit
                end.

Conversion fails on final typechecking

The file types/Circle.v in this branch fails on the "Defined." of S1_decode, complaining that some term

... has type "Int = Int" which should be coercible to
"S1_rechnd Set Int (path_universe succ_int) base =
S1_rechnd Set Int (path_universe succ_int) base".

But as far as I can tell, "S1_rechnd Set Int (path_universe succ_int) base" actually does reduce to "Int".

This code is intended for use with the "private types" patch to make the Agda hack for HITs work in Coq, but without that patch it should still compile if we remove the "Local" annotation on the "Inductive" -- and it does, in older commits of HoTT/Coq. git bisect suggests to me that whatever breaks it was introduced in late January, although it's hard to be sure since a lot of the commits fail to compile HoTT for other reasons.

Universe inconsistency (cannot enforce Set <= Prop)

Here's some code that works in 8.4, but fails in tip with "Universe inconsistency (cannot enforce Set <= Prop)".

Set Implicit Arguments.
Set Universe Polymorphism.
Generalizable All Variables.

Record Category (obj : Type) := { Morphism : obj -> obj -> Type }.

Definition SetCat : @Category Set := @Build_Category Set (fun s d => s -> d).

Record Foo := { foo : forall A (f : Morphism SetCat A A), True }.

Local Notation PartialBuild_Foo pf := (@Build_Foo (fun A f => pf A f)).

Set Printing Universes.
Let SetCatFoo' : Foo.
  let pf := fresh in
  let pfT := fresh in
  evar (pfT : Prop);
    cut pfT;
    [ subst pfT; intro pf;
      let t := constr:(PartialBuild_Foo pf) in
      let t' := (eval simpl in t) in
      exact t'
    | ].
  admit.
(* Toplevel input, characters 15-20:
Error: Universe inconsistency (cannot enforce Set <= Prop).
 *)

Feature Request: Supporting explicit universe level variables

Is there any plan to have explicit universe level variables in Coq?

Alternatively, is there a way to get the following approach to "work"?

Set Implicit Arguments.

Set Printing Universes.

Set Printing All.

Section Cat.
  Polymorphic Let typeof {T : Type} (_ : T) := T.


  Polymorphic Record Category (i : Type) (j : Type) :=
    {
      Object :> typeof i;
      Morphism : Object -> Object -> typeof j
    }.

  Check Category.  (* Category (* Top.108
Top.109 *)
     : forall (_ : Type (* Top.108 *)) (_ : Type (* Top.109 *)),
       Type (* max(Top.100, Top.108) *) *)
  Check (@Category nat). (*  Category (* Set Top.111 *) nat
     : forall _ : Type (* Top.111 *), Type (* max(Top.100, Set) *) *)
  Check (@Category nat nat). (* Category (* Set Set *) nat nat
     : Type (* max(Top.100, Set) *) *)
End Cat.

In particular, where does the Top.100 come from, and are there any reasonable semantics that make Category nat nat land in Set?

Failure to infer that a type is equal to [Prop]

This code works fine in 8.4, but the second Check errors in HoTT/Coq.

Set Printing Universes.
Local Close Scope nat_scope.
  Check (fun ab : Prop * Prop => (fst ab : Prop) * (snd ab : Prop)).
  (* fun ab : Prop * Prop =>
(fst (* Top.5817 Top.5818 *) ab:Prop) * (snd (* Top.5817 Top.5818 *) ab:Prop)
     : Prop * Prop -> Prop *)
  Check (fun ab : Prop * Prop => (fst ab : Prop) * (snd ab : Prop) : Prop).
  (* Toplevel input, characters 51-84:
Error: In environment
ab : Prop * Prop
The term
 "(fst (* Top.5833 Top.5834 *) ab:Prop) *
  (snd (* Top.5833 Top.5834 *) ab:Prop)" has type
 "Type (* max(Top.5829, Top.5830) *)" while it is expected to have type
 "Prop". *)

Term can be constructed interactively, but not given explicitly.

In this file, the definition flip_P_is_retr1 successfully constructs a term interactively (by explicitly unfolding some of the types involved); but the resulting term, when given explicitly (including all explicit arguments etc.), as flip_P_is_retr3, fails to typecheck.

(A couple of other variations on the definition are also included.)

`Prop : Prop` should not work

Check Prop : Prop. (* Prop:Prop
     : Prop *)
Check Set : Prop. (* Set:Prop
     : Prop *)
Check ((bool -> Prop) : Prop). (* bool -> Prop:Prop
     : Prop *)
Axiom proof_irrelevance : forall (P : Prop) (p1 p2 : P), p1 = p2.
Check ((True : Prop) : Set). (* (True:Prop):Set
     : Set *)
Goal (forall (v : Type) (f1 f0 : v -> Prop),
        @eq (v -> Prop) f0 f1).
intros.
apply proof_irrelevance.
Defined. (* Unnamed_thm is defined *)
Set Printing Universes.
Check ((True : Prop) : Set). (* Toplevel input, characters 0-28:
Error: Universe inconsistency (cannot enforce Prop <= Set because Set
< Prop). *)

Globally renaming arguments within section causes "Anomaly: dirpath_prefix: empty dirpath."

The following code suffices to trigger it, on my system:

Definition my_fun (n:nat) := n.

Section My_Sec.
Global Arguments my_fun x : rename.
End My_Sec.

The Global Arguments declaration succeeds fine, but the End My_Sec fails, with Anomaly: dirpath_prefix: empty dirpath. Please report.

If Global is removed, or if no arguments are renamed, then everything works as expected.

If other declarations go between the Global Arguments and the End My_Sec, then the other declarations work normally, but the End My_Sec still fails.

(Working over b07e5d7, i.e. current stable branch. I haven’t tested this in the main coq trunk since I’m having problems building that, but I will do so as soon as I can.)

Coqide comes up and then dies ...

Coqide comes up and then dies ...
It does raise an error message, but it disappears to fast to read it.
If you give me a clue about where the logs are, I may be able to give more information.

as requested, anomaly please report

code in here ... sorry, it's kind-of crufty.

The last proof is accepted, but the closing Defined produces

Anomaly: File "proofs/proof.ml", line 155, characters 12-18: Assertion failed.
Please report.

Therefore, here you go!

Universe Inconsistency

Here's some code that works in Coq 8.4, but fails with a Universe Inconsistency in HoTT/coq. Note that changing auto to assumption on the specified line makes the inconsistency go away.

Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Universe Polymorphism.

Delimit Scope object_scope with object.
Delimit Scope morphism_scope with morphism.
Delimit Scope category_scope with category.
Delimit Scope functor_scope with functor.

Local Open Scope category_scope.

Record SpecializedCategory (obj : Type) :=
  {
    Object :> _ := obj;
    Morphism : obj -> obj -> Type;

    Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
  }.

Bind Scope category_scope with SpecializedCategory.
Bind Scope object_scope with Object.
Bind Scope morphism_scope with Morphism.

Arguments Object {obj%type} C%category / : rename.
Arguments Morphism {obj%type} !C%category s d : rename. (* , simpl nomatch. *)
Arguments Compose {obj%type} [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename.

Record Category := {
  CObject : Type;

  UnderlyingCategory :> @SpecializedCategory CObject
}.

Definition GeneralizeCategory `(C : @SpecializedCategory obj) : Category.
  refine {| CObject := C.(Object) |}; auto. (* Changing this [auto] to [assumption] removes the universe inconsistency. *)
Defined.

Coercion GeneralizeCategory : SpecializedCategory >-> Category.

Record SpecializedFunctor
       `(C : @SpecializedCategory objC)
       `(D : @SpecializedCategory objD)
  := {
      ObjectOf :> objC -> objD;
      MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d)
    }.

Section Functor.
  Variable C D : Category.

  Definition Functor := SpecializedFunctor C D.
End Functor.

Bind Scope functor_scope with SpecializedFunctor.
Bind Scope functor_scope with Functor.

Arguments SpecializedFunctor {objC} C {objD} D.
Arguments Functor C D.
Arguments ObjectOf {objC%type C%category objD%type D%category} F%functor c%object : rename, simpl nomatch.
Arguments MorphismOf {objC%type} [C%category] {objD%type} [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch.

Section FunctorComposition.
  Context `(B : @SpecializedCategory objB).
  Context `(C : @SpecializedCategory objC).
  Context `(D : @SpecializedCategory objD).
  Context `(E : @SpecializedCategory objE).

  Definition ComposeFunctors (G : SpecializedFunctor D E) (F : SpecializedFunctor C D) : SpecializedFunctor C E
    := Build_SpecializedFunctor C E
                                (fun c => G (F c))
                                (fun _ _ m => G.(MorphismOf) (F.(MorphismOf) m)).
End FunctorComposition.

Record SpecializedNaturalTransformation
       `{C : @SpecializedCategory objC}
       `{D : @SpecializedCategory objD}
       (F G : SpecializedFunctor C D)
  := {
      ComponentsOf :> forall c, D.(Morphism) (F c) (G c)
    }.

Definition ProductCategory
           `(C : @SpecializedCategory objC)
           `(D : @SpecializedCategory objD)
: @SpecializedCategory (objC * objD)%type
  := @Build_SpecializedCategory _
                                (fun s d => (C.(Morphism) (fst s) (fst d) * D.(Morphism) (snd s) (snd d))%type)
                                (fun s d d' m2 m1 => (Compose (fst m2) (fst m1), Compose (snd m2) (snd m1))).

Infix "*" := ProductCategory : category_scope.

Section ProductCategoryFunctors.
  Context `{C : @SpecializedCategory objC}.
  Context `{D : @SpecializedCategory objD}.

  Definition fst_Functor : SpecializedFunctor (C * D) C
    := Build_SpecializedFunctor (C * D) C
                                (@fst _ _)
                                (fun _ _ => @fst _ _).

  Definition snd_Functor : SpecializedFunctor (C * D) D
    := Build_SpecializedFunctor (C * D) D
                                (@snd _ _)
                                (fun _ _ => @snd _ _).
End ProductCategoryFunctors.


Definition OppositeCategory `(C : @SpecializedCategory objC) : @SpecializedCategory objC :=
  @Build_SpecializedCategory objC
                             (fun s d => Morphism C d s)
                             (fun _ _ _ m1 m2 => Compose m2 m1).

Section OppositeFunctor.
  Context `(C : @SpecializedCategory objC).
  Context `(D : @SpecializedCategory objD).
  Variable F : SpecializedFunctor C D.
  Let COp := OppositeCategory C.
  Let DOp := OppositeCategory D.

  Definition OppositeFunctor : SpecializedFunctor COp DOp
    := Build_SpecializedFunctor COp DOp
                                (fun c : COp => F c : DOp)
                                (fun (s d : COp) (m : C.(Morphism) d s) => MorphismOf F (s := d) (d := s) m).
End OppositeFunctor.

Section FunctorProduct.
  Context `(C : @SpecializedCategory objC).
  Context `(D : @SpecializedCategory objD).
  Context `(D' : @SpecializedCategory objD').

  Definition FunctorProduct (F : Functor C D) (F' : Functor C D') : SpecializedFunctor C (D * D').
    match goal with
      | [ |- SpecializedFunctor ?C0 ?D0 ] =>
        refine (Build_SpecializedFunctor
                  C0 D0
                  (fun c => (F c, F' c))
                  (fun s d m => (MorphismOf F m, MorphismOf F' m)))
    end.
  Defined.
End FunctorProduct.

Section FunctorProduct'.
  Context `(C : @SpecializedCategory objC).
  Context `(D : @SpecializedCategory objD).
  Context `(C' : @SpecializedCategory objC').
  Context `(D' : @SpecializedCategory objD').
  Variable F : Functor C D.
  Variable F' : Functor C' D'.

  Definition FunctorProduct' : SpecializedFunctor  (C * C') (D * D')
    := FunctorProduct (ComposeFunctors F fst_Functor) (ComposeFunctors F' snd_Functor).
End FunctorProduct'.

(** XXX TODO(jgross): Change this to [FunctorProduct]. *)
Infix "*" := FunctorProduct' : functor_scope.

Definition TypeCat : @SpecializedCategory Type :=
  (@Build_SpecializedCategory Type
                              (fun s d => s -> d)
                              (fun _ _ _ f g => (fun x => f (g x)))).

Section HomFunctor.
  Context `(C : @SpecializedCategory objC).
  Let COp := OppositeCategory C.

  Definition CovariantHomFunctor (A : COp) : SpecializedFunctor C TypeCat
    := Build_SpecializedFunctor C TypeCat
                                (fun X : C => C.(Morphism) A X : TypeCat)
                                (fun X Y f => (fun g : C.(Morphism) A X => Compose f g)).

  Definition hom_functor_object_of (c'c : COp * C) := C.(Morphism) (fst c'c) (snd c'c) : TypeCat.

  Definition hom_functor_morphism_of (s's : (COp * C)%type) (d'd : (COp * C)%type) (hf : (COp * C).(Morphism) s's d'd) :
    TypeCat.(Morphism) (hom_functor_object_of s's) (hom_functor_object_of d'd).
    unfold hom_functor_object_of in *.
    destruct s's as [ s' s ], d'd as [ d' d ].
    destruct hf as [ h f ].
    intro g.
    exact (Compose f (Compose g h)).
  Defined.

  Definition HomFunctor : SpecializedFunctor (COp * C) TypeCat
    := Build_SpecializedFunctor (COp * C) TypeCat
                                (fun c'c : COp * C => C.(Morphism) (fst c'c) (snd c'c) : TypeCat)
                                (fun X Y (hf : (COp * C).(Morphism) X Y) => hom_functor_morphism_of hf).
End HomFunctor.

Section FullFaithful.
  Context `(C : @SpecializedCategory objC).
  Context `(D : @SpecializedCategory objD).
  Variable F : SpecializedFunctor C D.
  Let COp := OppositeCategory C.
  Let DOp := OppositeCategory D.
  Let FOp := OppositeFunctor F.

  Definition InducedHomNaturalTransformation :
    SpecializedNaturalTransformation (HomFunctor C) (ComposeFunctors (HomFunctor D) (FOp * F))
    := (Build_SpecializedNaturalTransformation (HomFunctor C) (ComposeFunctors (HomFunctor D) (FOp * F))
                                               (fun sd : (COp * C) =>
                                                  MorphismOf F (s := _) (d := _))).
End FullFaithful.

Definition FunctorCategory
           `(C : @SpecializedCategory objC)
           `(D : @SpecializedCategory objD)
: @SpecializedCategory (SpecializedFunctor C D).
  refine (@Build_SpecializedCategory _
                                     (SpecializedNaturalTransformation (C := C) (D := D))
                                     _);
  admit.
Defined.

Notation "C ^ D" := (FunctorCategory D C) : category_scope.

Section Yoneda.
  Context `(C : @SpecializedCategory objC).
  Let COp := OppositeCategory C.

  Section Yoneda.
    Let Yoneda_NT s d (f : COp.(Morphism) s d) : SpecializedNaturalTransformation (CovariantHomFunctor C s) (CovariantHomFunctor C d)
      := Build_SpecializedNaturalTransformation
           (CovariantHomFunctor C s)
           (CovariantHomFunctor C d)
           (fun c : C => (fun m : C.(Morphism) _ _ => Compose m f)).

    Definition Yoneda : SpecializedFunctor COp (TypeCat ^ C)
      := Build_SpecializedFunctor COp (TypeCat ^ C)
                                  (fun c : COp => CovariantHomFunctor C c : TypeCat ^ C)
                                  (fun s d (f : Morphism COp s d) => Yoneda_NT s d f).
  End Yoneda.
End Yoneda.

Section FullyFaithful.
  Context `(C : @SpecializedCategory objC).

  Check InducedHomNaturalTransformation (Yoneda C).

[Set Printing All.] does not imply [Set Printing Universes.]

Should [Set Printing All.] really mean “all”, or is this a deliberate omission?

tip (b4115d0328adb0bbb150ab5c22dd395265f2e1d4) does not compile

After a make -j16 -k; make -j16, I get

$ make -j16
make --warn-undefined-variable --no-builtin-rules -f Makefile.build "world"
make[1]: Entering directory `/afs/csail.mit.edu/u/j/jgross/coq'
OCAMLDEP  ide/coqide_main_opt.ml
make[1]: Leaving directory `/afs/csail.mit.edu/u/j/jgross/coq'
make[1]: Entering directory `/afs/csail.mit.edu/u/j/jgross/coq'
CHECK revision
OCAMLOPT  pretyping/indrec.ml
OCAMLC    pretyping/indrec.ml
File "pretyping/indrec.ml", line 1:
Error: The implementation pretyping/indrec.ml
       does not match the interface pretyping/indrec.cmi:
       The field `modify_sort_scheme' is required but not provided
make[1]: *** [pretyping/indrec.cmx] Error 2
make[1]: *** Waiting for unfinished jobs....
File "pretyping/indrec.ml", line 1:
Error: The implementation pretyping/indrec.ml
       does not match the interface pretyping/indrec.cmi:
       The field `modify_sort_scheme' is required but not provided
make[1]: *** [pretyping/indrec.cmo] Error 2
make[1]: Leaving directory `/afs/csail.mit.edu/u/j/jgross/coq'
make: *** [world] Error 2

Change in behavior of [Set Implicit Arguments]

The code

Set Implicit Arguments.

Inductive telescope :=
| Base : forall (A : Type) (B : A -> Type), (forall a, B a) -> (forall a, B a) -> telescope
| Quant : forall A : Type, (A -> telescope) -> telescope.

Fixpoint telescopeOut (t : telescope) :=
  match t with
    | Base _ _ x y => x = y
    | Quant _ f => forall x, telescopeOut (f x)
  end.

fails to compile, informing me that Base expects 3 arguments. Removing Set Implicit Arguments changes this. In 8.4, this succeeds either way.

Anomaly: apply_coercion_args: mismatch between arguments and coercion. Please report.

Here's some code that generates

Toplevel input, characters 15-41:
Anomaly: apply_coercion_args: mismatch between arguments and coercion.
Please report.
frame @ file "toplevel/vernac.ml", line 343, characters 6-16
raise @ file "toplevel/vernac.ml", line 335, characters 18-25
frame @ file "toplevel/vernac.ml", line 327, characters 14-104
raise @ file "library/states.ml", line 40, characters 45-46
frame @ file "library/states.ml", line 38, characters 4-7
raise @ file "toplevel/vernacentries.ml", line 1829, characters 12-13
frame @ file "toplevel/vernacentries.ml", line 1818, characters 4-12
frame @ file "toplevel/command.ml", line 175, characters 4-86
frame @ file "toplevel/command.ml", line 95, characters 18-85
frame @ file "pretyping/pretyping.ml", line 780, characters 2-70
frame @ file "pretyping/pretyping.ml", line 713, characters 1-46
frame @ file "pretyping/evarutil.ml", line 29, characters 17-28
raise @ unknown
frame @ file "pretyping/coercion.ml", line 377, characters 17-45
raise @ unknown
frame @ file "pretyping/coercion.ml", line 331, characters 6-489
frame @ file "list.ml", line 86, characters 24-34
frame @ file "pretyping/coercion.ml", line 337, characters 5-79
frame @ file "pretyping/coercion.ml", line 50, characters 12-42
frame @ file "pretyping/coercion.ml", line 46, characters 7-85
raise @ file "lib/errors.ml", line 27, characters 18-39

Sorry that it's a bit long, and sorry for all the notations. If I get rid of Eval unfold AssociatorCoherenceCondition in towards the bottom, the code runs fine. The code runs fine as-is in Coq 8.4.

Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Universe Polymorphism.

Reserved Notation "x # y" (at level 40, left associativity).
Reserved Notation "x #m y" (at level 40, left associativity).

Delimit Scope object_scope with object.
Delimit Scope morphism_scope with morphism.
Delimit Scope category_scope with category.

Record Category (obj : Type) :=
  {
    Object :> _ := obj;
    Morphism : obj -> obj -> Type;

    Identity : forall x, Morphism x x;
    Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
  }.

Bind Scope object_scope with Object.
Bind Scope morphism_scope with Morphism.

Arguments Object {obj%type} C%category / : rename.
Arguments Morphism {obj%type} !C%category s d : rename. (* , simpl nomatch. *)
Arguments Identity {obj%type} [!C%category] x%object : rename.
Arguments Compose {obj%type} [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename.

Bind Scope category_scope with Category.

Record Functor
       `(C : @Category objC)
       `(D : @Category objD)
  := {
      ObjectOf :> objC -> objD;
      MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d)
    }.

Record NaturalTransformation
       `(C : @Category objC)
       `(D : @Category objD)
       (F G : Functor C D)
  := {
      ComponentsOf :> forall c, D.(Morphism) (F c) (G c)
    }.

Definition ProductCategory
           `(C : @Category objC)
           `(D : @Category objD)
: @Category (objC * objD)%type.
  refine (@Build_Category _
                          (fun s d => (C.(Morphism) (fst s) (fst d) * D.(Morphism) (snd s) (snd d))%type)
                          (fun o => (Identity (fst o), Identity (snd o)))
                          (fun s d d' m2 m1 => (Compose (fst m2) (fst m1), Compose (snd m2) (snd m1)))).

Defined.

Infix "*" := ProductCategory : category_scope.

Record IsomorphismOf `{C : @Category objC} {s d} (m : C.(Morphism) s d) :=
  {
    IsomorphismOf_Morphism :> C.(Morphism) s d := m;
    Inverse : C.(Morphism) d s
  }.

Record NaturalIsomorphism
       `(C : @Category objC)
       `(D : @Category objD)
       (F G : Functor C D)
  := {
      NaturalIsomorphism_Transformation :> NaturalTransformation F G;
      NaturalIsomorphism_Isomorphism : forall x : objC, IsomorphismOf (NaturalIsomorphism_Transformation x)
    }.

Section PreMonoidalCategory.
  Context `(C : @Category objC).

  Variable TensorProduct : Functor (C * C) C.

  Let src {C : @Category objC} {s d} (_ : Morphism C s d) := s.
  Let dst {C : @Category objC} {s d} (_ : Morphism C s d) := d.

  Local Notation "A # B" := (TensorProduct (A, B)).
  Local Notation "A #m B" := (TensorProduct.(MorphismOf) ((@src _ _ _ A, @src _ _ _ B)) ((@dst _ _ _ A, @dst _ _ _ B)) (A, B)%morphism).

  Let TriMonoidalProductL_ObjectOf (abc : C * C * C) : C :=
    (fst (fst abc) # snd (fst abc)) # snd abc.

  Let TriMonoidalProductR_ObjectOf (abc : C * C * C) : C :=
    fst (fst abc) # (snd (fst abc) # snd abc).

  Let TriMonoidalProductL_MorphismOf (s d : C * C * C) (m : Morphism (C * C * C) s d) :
    Morphism C (TriMonoidalProductL_ObjectOf s) (TriMonoidalProductL_ObjectOf d).
  Admitted.

  Let TriMonoidalProductR_MorphismOf (s d : C * C * C) (m : Morphism (C * C * C) s d) :
    Morphism C (TriMonoidalProductR_ObjectOf s) (TriMonoidalProductR_ObjectOf d).
  Admitted.

  Definition TriMonoidalProductL : Functor (C * C * C) C.
    refine (Build_Functor (C * C * C) C
                          TriMonoidalProductL_ObjectOf
                          TriMonoidalProductL_MorphismOf).
  Defined.

  Definition TriMonoidalProductR : Functor (C * C * C) C.
    refine (Build_Functor (C * C * C) C
                          TriMonoidalProductR_ObjectOf
                          TriMonoidalProductR_MorphismOf).
  Defined.

  Variable Associator : NaturalIsomorphism TriMonoidalProductL TriMonoidalProductR.

  Section AssociatorCoherenceCondition.
    Variables a b c d : C.

    (* going from top-left *)
    Let AssociatorCoherenceConditionT0 : Morphism C (((a # b) # c) # d) ((a # (b # c)) # d)
      := Associator (a, b, c) #m Identity (C := C) d.
    Let AssociatorCoherenceConditionT1 : Morphism C ((a # (b # c)) # d) (a # ((b # c) # d))
      := Associator (a, b # c, d).
    Let AssociatorCoherenceConditionT2 : Morphism C (a # ((b # c) # d)) (a # (b # (c # d)))
      := Identity (C := C) a #m Associator (b, c, d).
    Let AssociatorCoherenceConditionB0 : Morphism C (((a # b) # c) # d) ((a # b) # (c # d))
      := Associator (a # b, c, d).
    Let AssociatorCoherenceConditionB1 : Morphism C ((a # b) # (c # d)) (a # (b # (c # d)))
      := Associator (a, b, c # d).

    Definition AssociatorCoherenceCondition' :=
      Compose AssociatorCoherenceConditionT2 (Compose AssociatorCoherenceConditionT1 AssociatorCoherenceConditionT0)
      = Compose AssociatorCoherenceConditionB1 AssociatorCoherenceConditionB0.
  End AssociatorCoherenceCondition.

  Definition AssociatorCoherenceCondition := Eval unfold AssociatorCoherenceCondition' in
                                              forall a b c d : C, AssociatorCoherenceCondition' a b c d.
End PreMonoidalCategory.

Section MonoidalCategory.
  Variable objC : Type.

  Let AssociatorCoherenceCondition' := Eval unfold AssociatorCoherenceCondition in @AssociatorCoherenceCondition.

  Record MonoidalCategory :=
    {
      MonoidalUnderlyingCategory :> @Category objC;
      TensorProduct : Functor (MonoidalUnderlyingCategory * MonoidalUnderlyingCategory) MonoidalUnderlyingCategory;
      IdentityObject : objC;
      Associator : NaturalIsomorphism (TriMonoidalProductL TensorProduct) (TriMonoidalProductR TensorProduct);
      AssociatorCoherent : AssociatorCoherenceCondition' Associator
    }.
End MonoidalCategory.

Section EnrichedCategory.
  Context `(M : @MonoidalCategory objM).
  Let x : M := IdentityObject M.

Theorem about transport?

Is there a good name for the theorem

(forall A X Y Z x y p a b, @transport A (fun a => forall (x : X) (y : Y a x), Z a x y) x y p a b
                                    = @transport A (fun a => forall y : Y a b, Z a b y) x y p (a b))

which is trivially provable by path induction and reflexivity? Also, is the a version where X depends on A?

`Error: Illegal application (Type Error)` due to ... greedy universe level unification?

I get the error

Error: Illegal application (Type Error): 
The term "Functor" of type
 "forall (objC : Type (* Top.1194 *)) (_ : Cat objC)
    (objD : Type (* Top.1194 *)) (_ : Cat objD),
  Type (* Top.1194 *)"
cannot be applied to the terms
 "Prop" : "Type (* (Set)+1 *)"
 "TypeCat" : "Cat Type (* Top.1201 *)"
 "objC" : "Type (* Top.1194 *)"
 "C" : "Cat objC"
The 2nd term has type "Cat Type (* Top.1201 *)"
which should be coercible to "Cat Prop".

on the Defined. of the following code:

Set Implicit Arguments.

Record Cat (obj : Type) := {}.

Record Functor objC (C : Cat objC) objD (D : Cat objD) :=
  {
    ObjectOf' : objC -> objD
  }.

Definition TypeCat : Cat Type. constructor. Defined.
Definition PropCat : Cat Prop. constructor. Defined.

Definition FunctorFrom_Type2Prop objC (C : Cat objC) (F : Functor TypeCat C) : Functor PropCat C.
  Set Printing All.
  Set Printing Universes.
  Check F. (* F : @Functor Type (* Top.1201 *) TypeCat objC C *)
  exact (Build_Functor PropCat C (ObjectOf' F)).
  Show Proof. (* (fun (objC : Type (* Top.1194 *)) (C : Cat objC)
   (F : @Functor Prop TypeCat objC C) =>
 @Build_Functor Prop PropCat objC C
   (@ObjectOf' Prop TypeCat objC C F)) *)
Defined.

Note that the argument F has somehow acquired the type F : @Functor Prop TypeCat objC C, rather than F : @Functor Type TypeCat objC C. This code goes through fine on Coq 8.4.

Ltac unification should either ignore universe constraints, deferring them to when the proof tree is built, or should update universe constraints

I want the following code to work:

Goal Type = Type.
  match goal with |- ?x = ?x => idtac end.

I'm not sure what the behavior should be if one of the Types is replaced by Set or Prop. I'm running into a problem where rewrite fails to find the term it needs to rewrite with because of a universe mismatch, I think. (It's not quite the same as this; it's failing to unify ap10 (* Top.191 Top.191 Top.191 *) with ap10 (* Top.1863 Top.191 Top.1865 *).) It's very annoying to have to go manually fill in the arguments to the rewrite, pose the lemma, and change the variant in the goal with the variant in the hypothesis, just to rewrite. I've recently emailed coq-club about this; here is what I wrote:

I have a goal where the following succeed:

lazymatch goal with |- ?f ?x0 ?x1 ?x2 ?x3 ?x4 ?x5 = ?g ?x0 ?x1 ?x2 ?x3 ?x4' ?x5
=> let check := constr:(eq_refl : f = g) in idtac
end.
lazymatch goal with |- ?f ?x0 ?x1 ?x2 ?x3 ?x4 ?x5 = ?g ?x0 ?x1 ?x2 ?x3 ?x4' ?x5
=> change f with g
end.
lazymatch goal with |- ?f ?x0 ?x1 ?x2 ?x3 ?x4 ?x5 = ?g ?x0 ?x1 ?x2 ?x3 ?x4' ?x5
=> let F := eval hnf in f in let G := eval hnf in g in constr_eq F G
end.
lazymatch goal with |- ?f ?x0 ?x1 ?x2 ?x3 ?x4 ?x5 = ?g ?x0 ?x1 ?x2 ?x3 ?x4' ?x5
=> pose Type as stupid;
let F := eval cbv delta [stupid] in f in let G := eval cbv delta [stupid] in g in constr_eq F G
end.
lazymatch goal with |- ?f ?x0 ?x1 ?x2 ?x3 ?x4 ?x5 = ?g ?x0 ?x1 ?x2 ?x3 ?x4' ?x5
=> let T := type of f in let T' := type of g in constr_eq T T'
end.
lazymatch goal with |- ?f ?x0 ?x1 ?x2 ?x3 ?x4 ?x5 = ?g ?x0 ?x1 ?x2 ?x3 ?x4' ?x5
=> let F := constr:(fun _ : Set => f) in let G := constr:(fun _ : Set => g) in constr_eq F G
end.

and the following fail:

lazymatch goal with |- ?f ?x0 ?x1 ?x2 ?x3 ?x4 ?x5 = ?g ?x0 ?x1 ?x2 ?x3 ?x4' ?x5
=> constr_eq f g
end.
(* note the lack of [g] in the following match *)
lazymatch goal with |- ?f ?x0 ?x1 ?x2 ?x3 ?x4 ?x5 = ?f ?x0 ?x1 ?x2 ?x3 ?x4' ?x5
=> idtac
end.

note that match goal with |- ?G => has_evar G end fails, indicating that the problem is not evars.

Even more weirdly,

lazymatch goal with |- ?f ?x0 ?x1 ?x2 ?x3 ?x4 ?x5 = ?f' ?x0 ?x1 ?x2 ?x3 ?x4' ?x5
=> let check := constr:(idpath : f = f') in idtac
end.
lazymatch goal with |- ?f ?x0 ?x1 ?x2 ?x3 ?x4 ?x5 = ?f' ?x0 ?x1 ?x2 ?x3 ?x4' ?x5
=> progress change f with f'
end.

fails, but if I switch the order of the lazymatches, then it goes through!

What's going on here? I strongly suspect that this is a bug. (Also, what's kind of reduction does [cbv deta [foo] in bar] do when [foo] doesn't appear in [bar]?)

-Jason

P.S. The code I'm working with is available at https://github.com/JasonGross/HoTT-categories/blob/3a47db011ea7ff6f7a3fcb538fd9bcefbd6e4b0f/theories/Grothendieck/ToCat.v#L194. It only runs on top of HoTT/coq, sorry.

Anomaly: Mismatched instance and context when building universe substitution. on coqc -xml

If bug05.v is

Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Universe Polymorphism.

Delimit Scope object_scope with object.
Delimit Scope morphism_scope with morphism.
Delimit Scope category_scope with category.
Delimit Scope functor_scope with functor.

Local Open Scope category_scope.

Record SpecializedCategory (obj : Type) :=
  {
    Object :> _ := obj;
    Morphism : obj -> obj -> Type;

    Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
  }.

I get

$ coqc -xml -debug -q -I . bug05
File "./bug05.v", line 13, characters 0-187:
Anomaly: Mismatched instance and context when building universe substitution.
Please report.
frame @ file "toplevel/vernac.ml", line 420, characters 12-38
raise @ file "toplevel/vernac.ml", line 111, characters 8-56
frame @ file "toplevel/vernac.ml", line 374, characters 27-64
frame @ file "toplevel/vernac.ml", line 348, characters 11-32
frame @ file "toplevel/vernac.ml", line 343, characters 6-16
raise @ file "toplevel/vernac.ml", line 335, characters 18-25
frame @ file "toplevel/vernac.ml", line 327, characters 14-104
raise @ file "library/states.ml", line 40, characters 45-46
frame @ file "library/states.ml", line 38, characters 4-7
raise @ file "lib/flags.ml", line 15, characters 10-17
frame @ file "lib/flags.ml", line 11, characters 14-17
raise @ file "toplevel/vernacentries.ml", line 1829, characters 12-13
frame @ file "toplevel/vernacentries.ml", line 1818, characters 4-12
frame @ file "toplevel/vernacentries.ml", line 546, characters 10-90
frame @ file "toplevel/record.ml", line 470, characters 11-178
frame @ file "toplevel/record.ml", line 332, characters 11-97
frame @ file "toplevel/command.ml", line 504, characters 15-40
frame @ file "library/declare.ml", line 321, characters 2-41
frame @ file "plugins/xml/xmlcommand.ml", line 403, characters 32-91
frame @ file "plugins/xml/xmlcommand.ml", line 241, characters 4-663
frame @ file "array.ml", line 128, characters 9-30
frame @ file "kernel/inductive.ml", line 178, characters 6-38
frame @ file "kernel/inductive.ml", line 56, characters 4-44
raise @ file "lib/errors.ml", line 27, characters 18-39

make world gets stuck

In 55fa982... somehow make world gets stuck on COQC theories/Sorting/Permutation.v
This issue is not present in 431838b...
And it might just be me.

`Polymorphic Variables A B : ...` should separate the universe variables of `A` and of `B`

Here's some more code that produces a universe inconsistency in the tip of HoTT/coq, but not in 8.4:

Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.

Record SpecializedCategory (obj : Type) :=
  {
    Object :> _ := obj;
    Morphism : obj -> obj -> Type
  }.


Record > Category :=
  {
    CObject : Type;

    UnderlyingCategory :> @SpecializedCategory CObject
  }.

Record SpecializedFunctor `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) :=
  {
    ObjectOf :> objC -> objD;
    MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d)
  }.

(* Replacing this with [Definition Functor (C D : Category) :=
SpecializedFunctor C D.] gets rid of the universe inconsistency. *)
Section Functor.
  Variable C D : Category.

  Definition Functor := SpecializedFunctor C D.
End Functor.

Record SpecializedNaturalTransformation `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) (F G : SpecializedFunctor C D) :=
  {
    ComponentsOf :> forall c, D.(Morphism) (F c) (G c)
  }.

Definition FunctorProduct' `(F : Functor C D) : SpecializedFunctor C D.
admit.
Defined.

Definition TypeCat : @SpecializedCategory Type.
  admit.
Defined.


Definition CovariantHomFunctor `(C : @SpecializedCategory objC) : SpecializedFunctor C TypeCat.
  refine (Build_SpecializedFunctor C TypeCat
                                   (fun X : C => C.(Morphism) X X)
                                   _
         ); admit.
Defined.

Definition FunctorCategory `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) : @SpecializedCategory (SpecializedFunctor C D).
  refine (@Build_SpecializedCategory _
                                     (SpecializedNaturalTransformation (C := C) (D := D))).
Defined.

Definition Yoneda `(C : @SpecializedCategory objC) : SpecializedFunctor C (FunctorCategory C TypeCat).
  match goal with
    | [ |- SpecializedFunctor ?C0 ?D0 ] =>
      refine (Build_SpecializedFunctor C0 D0
                                       (fun c => CovariantHomFunctor C)
                                       _
             )
  end;
  admit.
Defined.

Section FullyFaithful.
  Context `(C : @SpecializedCategory objC).
  Let TypeCatC := FunctorCategory C TypeCat.
  Let YC := (Yoneda C).
  Check @FunctorProduct' C TypeCatC YC. (* works *)
  Check @FunctorProduct' C TypeCatC (Yoneda C). (* Universe inconsistency *)

Note that there are two things that fix the universe inconsistency: making C and D arguments of Functor, and sticking YC in a Let. No idea why the second one fixes things, but here's why the first one changes things:

Section foo.
  Polymorphic Variable C D : Type.
  Polymorphic Definition foo := (C * D)%type.
End foo.
Polymorphic Definition bar (C D : Type) := (C * D)%type.
Set Printing Universes.
Print foo.
(* Polymorphic foo =
fun C D : Type (* Top.1134 *) => (C * D)%type
     : Type (* Top.1134 *) -> Type (* Top.1134 *) -> Type (* Top.1134 *)
(* Top.1134 |=  *) *)
Print bar.
(* Polymorphic bar =
fun (C : Type (* Top.1138 *)) (D : Type (* Top.1139 *)) => (C * D)%type
     : Type (* Top.1138 *) ->
       Type (* Top.1139 *) -> Type (* max(Top.1138, Top.1139) *)
(* Top.1138
   Top.1139 |=  *) *)

Illegal application errors relating to Identity Coercions

This code compiles in Coq 8.4, but fails in HoTT/coq. I'm a bit confused as to why Let F' := (F : FunctorToSet _) : FunctorToType _. goes through in HoTT/coq but not Coq 8.4 without the identity coercion. Perhaps HoTT/coq unfolds FunctorToType and FunctorToSet and then unifies the Type with Set?

Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Universe Polymorphism.

Record Category (obj : Type) := { Morphism : obj -> obj -> Type }.

Record Functor `(C : Category objC) `(D : Category objD) :=
  { ObjectOf :> objC -> objD;
    MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d) }.

Definition TypeCat : @Category Type := @Build_Category Type (fun s d => s -> d).
Definition SetCat : @Category Set := @Build_Category Set (fun s d => s -> d).

Definition FunctorToSet `(C : @Category objC) := Functor C SetCat.
Definition FunctorToType `(C : @Category objC) := Functor C TypeCat.

(* Removing the following line, as well as the [Definition] and [Identity Coercion] immediately following it, makes the file go through *)
Identity Coercion FunctorToType_Id : FunctorToType >-> Functor.

Definition FunctorTo_Set2Type `(C : @Category objC) (F : FunctorToSet C)
: FunctorToType C.
  refine (@Build_Functor _ C _ TypeCat
                         (fun x => F.(ObjectOf) x)
                         (fun s d m => F.(MorphismOf) _ _ m)).
Defined. (* Toplevel input, characters 0-8:
Error:
The term
 "fun (objC : Type) (C : Category objC) (F : FunctorToSet C) =>
  {|
  ObjectOf := fun x : objC => F x;
  MorphismOf := fun (s d : objC) (m : Morphism C s d) => MorphismOf F s d m |}"
has type
 "forall (objC : Type) (C : Category objC),
  FunctorToSet C -> Functor C TypeCat" while it is expected to have type
 "forall (objC : Type) (C : Category objC), FunctorToSet C -> FunctorToType C".
 *)

Coercion FunctorTo_Set2Type : FunctorToSet >-> FunctorToType.

Record GrothendieckPair `(C : @Category objC) (F : Functor C TypeCat) :=
  { GrothendieckC : objC;
    GrothendieckX : F GrothendieckC }.

Record SetGrothendieckPair `(C : @Category objC) (F' : Functor C SetCat) :=
  { SetGrothendieckC : objC;
    SetGrothendieckX : F' SetGrothendieckC }.

Section SetGrothendieckCoercion.
  Context `(C : @Category objC).
  Variable F : Functor C SetCat.
  Let F' := (F : FunctorToSet _) : FunctorToType _.

  Set Printing Universes.
  Definition SetGrothendieck2Grothendieck (G : SetGrothendieckPair F) : GrothendieckPair F'
    := {| GrothendieckC := G.(SetGrothendieckC); GrothendieckX := G.(SetGrothendieckX) : F' _ |}.
  (* Toplevel input, characters 0-187:
Error: Illegal application:
The term "ObjectOf (* Top.8375 Top.8376 Top.8379 Set *)" of type
 "forall (objC : Type (* Top.8375 *))
    (C : Category (* Top.8375 Top.8376 *) objC) (objD : Type (* Top.8379 *))
    (D : Category (* Top.8379 Set *) objD),
  Functor (* Top.8375 Top.8376 Top.8379 Set *) C D -> objC -> objD"
cannot be applied to the terms
 "objC" : "Type (* Top.8375 *)"
 "C" : "Category (* Top.8375 Top.8376 *) objC"
 "Type (* Set *)" : "Type (* Set+1 *)"
 "TypeCat (* Top.8379 Set *)" : "Category (* Top.8379 Set *) Set"
 "F'" : "FunctorToType (* Top.8375 Top.8376 Top.8379 Set *) C"
 "SetGrothendieckC (* Top.8375 Top.8376 Top.8379 *) G" : "objC"
The 5th term has type "FunctorToType (* Top.8375 Top.8376 Top.8379 Set *) C"
which should be coercible to
 "Functor (* Top.8375 Top.8376 Top.8379 Set *) C TypeCat (* Top.8379 Set *)".
 *)
End SetGrothendieckCoercion.

Universe Inconsistency

The following code works in 8.4 (presumably adding an extra universe constraint), but not in HoTT/coq. Replacing @eq with fun T => @eq T removes the universe inconsistency, but prevents coq (both 8.4 and HoTT/coq) from inferring that the underscore should be (@eq_equivalence). I'm not sure what the right behavior is here. Having @eq get fresh universe variables every time it's mentioned is too expensive, right?

Require Import Classes.RelationClasses List Setoid.

Set Universe Polymorphism.

Definition RowType := list Type.


Inductive Row : RowType -> Type :=
| RNil : Row nil
| RCons : forall T Ts, T -> Row Ts -> Row (T :: Ts).

Inductive RowTypeDecidable (P : forall T, relation T) `(H : forall T, Equivalence (P T))
: RowType -> Type :=
| RTDecNil : RowTypeDecidable P H nil
| RTDecCons : forall T Ts, (forall t0 t1 : T,
                              {P T t0 t1} + {~P T t0 t1})
                           -> RowTypeDecidable P H Ts
                           -> RowTypeDecidable P H (T :: Ts).

Set Printing Universes.

Fixpoint Row_eq Ts
: RowTypeDecidable (@eq) _ Ts -> forall r1 r2 : Row Ts, {@eq (Row Ts) r1 r2} + {r1 <> r2}.
(* Toplevel input, characters 81-87:
Error:
In environment
Ts : RowType (* Top.53 Coq.Init.Logic.8 *)
r1 : Row (* Top.54 Top.55 *) Ts
r2 : Row (* Top.56 Top.57 *) Ts
The term "Row (* Coq.Init.Logic.8 Top.59 *) Ts" has type
 "Type (* max(Top.58+1, Top.59) *)" while it is expected to have type
 "Type (* Coq.Init.Logic.8 *)" (Universe inconsistency). *)

JMeq should be a Polymorphic Inductive

The following code generates a universe inconsistency unless JMeq_refl is polymorphic (at 4745a7b):

Require Import Eqdep Eqdep_dec FunctionalExtensionality JMeq ProofIrrelevance Setoid.

Set Implicit Arguments.

(*Polymorphic Inductive JMeq (A : Type (* Coq.Logic.JMeq.7 *)) (x : A)
: forall B : Type (* Coq.Logic.JMeq.8 *), B -> Prop :=
  JMeq_refl : JMeq x x. *) (* Uncommenting this out gets rid of the universe inconsistency. *)

Local Infix "==" := JMeq (at level 70).
Polymorphic Definition sigT_of_sigT2 A P Q (x : @sigT2 A P Q) := let (a, h, _) := x in existT _ a h.
Global Coercion sigT_of_sigT2 : sigT2 >-> sigT.
Polymorphic Definition projT3 A P Q (x : @sigT2 A P Q) :=
  let (x0, _, h) as x0 return (Q (projT1 x0)) := x in h.

Polymorphic Definition sig_of_sig2 A P Q (x : @sig2 A P Q) := let (a, h, _) := x in exist _ a h.
Global Coercion sig_of_sig2 : sig2 >-> sig.


Ltac destruct_all_matches_then matcher tac :=
  repeat match goal with
           | [ H : ?T |- _ ] => matcher T; destruct H; tac
         end.

Ltac destruct_all_matches matcher := destruct_all_matches_then matcher ltac:(simpl in            *)           .


Ltac destruct_type_matcher T HT :=
  match HT with
    | context[T] => idtac
  end.
Ltac destruct_type T := destruct_all_matches ltac:(destruct_type_matcher T).

Ltac destruct_sig_matcher HT :=
  let HT' := eval hnf in HT in
                          match HT' with
                            | @sig _ _ => idtac
                            | @sigT _ _ => idtac
                            | @sig2 _ _ _ => idtac
                            | @sigT2 _ _ _ => idtac
                          end.
Ltac destruct_sig := destruct_all_matches destruct_sig_matcher.

Polymorphic Lemma sig_eq A P (s s' : @sig A P) : proj1_sig s = proj1_sig s' -> s = s'.
admit.
Defined.

Polymorphic Lemma sig2_eq A P Q (s s' : @sig2 A P Q) : proj1_sig s = proj1_sig s' -> s = s'.
admit.
Defined.

Polymorphic Lemma sigT_eq A P (s s' : @sigT A P) : projT1 s = projT1 s' -> projT2 s == projT2 s' -> s = s'.
admit.
Defined.

Polymorphic Lemma sigT2_eq A P Q (s s' : @sigT2 A P Q) :
  projT1 s = projT1 s'
  -> projT2 s == projT2 s'
  -> projT3 s == projT3 s'
  -> s = s'.
admit.
Defined.

Polymorphic Lemma injective_projections_JMeq (A B A' B' : Type) (p1 : A * B) (p2 : A' * B') :
  fst p1 == fst p2 -> snd p1 == snd p2 -> p1 == p2.
admit.
Defined.

Ltac clear_refl_eq :=
  repeat match goal with
           | [ H : ?x = ?x |- _ ] => clear H
         end.


Ltac simpl_eq' :=
  apply sig_eq
        || apply sig2_eq
        || ((apply sigT_eq || apply sigT2_eq); intros; clear_refl_eq)
        || apply injective_projections
        || apply injective_projections_JMeq.

Ltac simpl_eq := intros; repeat (
                             simpl_eq'; simpl in *
                           ).

Ltac subst_body :=
  repeat match goal with
           | [ H := _ |- _ ] => subst H
         end.


Ltac expand :=
  match goal with
    | [ |- ?X = ?Y ] =>
      let X' := eval hnf in X in let Y' := eval hnf in Y in change (X' = Y')
    | [ |- ?X == ?Y ] =>
      let X' := eval hnf in X in let Y' := eval hnf in Y in change (X' == Y')
  end; simpl.

Polymorphic Lemma unit_eq_eq (u u' : unit) (H H' : u = u') : H = H'.
admit.
Defined.

Reserved Notation "S â†“ T" (at level 70, no associativity).

Delimit Scope object_scope with object.
Delimit Scope morphism_scope with morphism.
Delimit Scope category_scope with category.
Delimit Scope functor_scope with functor.

Polymorphic Lemma f_equal_JMeq A A' B B' a b (f : forall a : A, A' a) (g : forall b : B, B' b) :
  f == g -> (f == g -> A' == B') -> (f == g -> a == b) -> f a == g b.
admit.
Defined.

Polymorphic Lemma eq_JMeq T (A B : T) : A = B -> A == B.
admit.
Defined.

Ltac JMeq_eq :=
  repeat match goal with
           | [ |- _ == _ ] => apply eq_JMeq
           | [ H : _ == _ |- _ ] => apply JMeq_eq in H
         end.
Generalizable All Variables.

Polymorphic Record ComputationalCategory (obj : Type) :=
  Build_ComputationalCategory {
      Object :> _ := obj;
      Morphism : obj -> obj -> Type;

      Identity : forall x, Morphism x x;
      Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
    }.

Arguments Identity {obj%type} [!C%category] x%object : rename.
Arguments Compose {obj%type} [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename.

Polymorphic Class IsSpecializedCategory (obj : Type) (C : ComputationalCategory obj) : Prop :=
  {
    Associativity : forall o1 o2 o3 o4
                           (m1 : Morphism C o1 o2)
                           (m2 : Morphism C o2 o3)
                           (m3 : Morphism C o3 o4),
                      Compose (Compose m3 m2) m1 = Compose m3 (Compose m2 m1);

    Associativity_sym : forall o1 o2 o3 o4
                               (m1 : Morphism C o1 o2)
                               (m2 : Morphism C o2 o3)
                               (m3 : Morphism C o3 o4),
                          Compose m3 (Compose m2 m1) = Compose (Compose m3 m2) m1;
    LeftIdentity : forall a b (f : Morphism C a b), Compose (Identity b) f = f;
    RightIdentity : forall a b (f : Morphism C a b), Compose f (Identity a) = f
  }.

Polymorphic Record > SpecializedCategory (obj : Type) :=
  Build_SpecializedCategory' {
      UnderlyingCCategory :> ComputationalCategory obj;
      UnderlyingCCategory_IsSpecializedCategory :> IsSpecializedCategory UnderlyingCCategory
    }.

Existing Instance UnderlyingCCategory_IsSpecializedCategory.
Polymorphic Definition Build_SpecializedCategory (obj : Type)
            (Morphism : obj -> obj -> Type)
            (Identity' : forall o : obj, Morphism o o)
            (Compose' : forall s d d' : obj, Morphism d d' -> Morphism s d -> Morphism s d')
            (Associativity' : forall (o1 o2 o3 o4 : obj) (m1 : Morphism o1 o2) (m2 : Morphism o2 o3) (m3 : Morphism o3 o4),
                                Compose' o1 o2 o4 (Compose' o2 o3 o4 m3 m2) m1 = Compose' o1 o3 o4 m3 (Compose' o1 o2 o3 m2 m1))
            (LeftIdentity' : forall (a b : obj) (f : Morphism a b), Compose' a b b (Identity' b) f = f)
            (RightIdentity' : forall (a b : obj) (f : Morphism a b), Compose' a a b f (Identity' a) = f) :
  @SpecializedCategory obj
  := Eval hnf in
      let C := (@Build_ComputationalCategory obj
                                             Morphism
                                             Identity' Compose') in
      @Build_SpecializedCategory' obj
                                  C
                                  (@Build_IsSpecializedCategory obj C
                                                                Associativity'
                                                                (fun _ _ _ _ _ _ _ => eq_sym (Associativity' _ _ _ _ _ _ _))
                                                                LeftIdentity'
                                                                RightIdentity').


Polymorphic Definition LocallySmallSpecializedCategory (obj : Type)   := SpecializedCategory obj.
Polymorphic Definition SmallSpecializedCategory (obj : Set)   := SpecializedCategory obj.

Section DCategory.
  Variable O : Type.

  Let DiscreteCategory_Morphism (s d : O) := s = d.

  Polymorphic Definition DiscreteCategory_Compose (s d d' : O) (m : DiscreteCategory_Morphism d d') (m' : DiscreteCategory_Morphism s d) :
    DiscreteCategory_Morphism s d'.
admit.
Defined.

  Polymorphic Definition DiscreteCategory_Identity o : DiscreteCategory_Morphism o o.
admit.
Defined.

  Polymorphic Definition DiscreteCategory : @SpecializedCategory O.
admit.
Defined.
End DCategory.

Section SpecializedFunctor.
  Context `(C : @SpecializedCategory objC).
  Context `(D : @SpecializedCategory objD).


  Polymorphic Record SpecializedFunctor :=
    {
      ObjectOf :> objC -> objD;
      MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d);
      FCompositionOf : forall s d d' (m1 : C.(Morphism) s d) (m2: C.(Morphism) d d'),
                         MorphismOf _ _ (Compose m2 m1) = Compose (MorphismOf _ _ m2) (MorphismOf _ _ m1);
      FIdentityOf : forall x, MorphismOf _ _ (Identity x) = Identity (ObjectOf x)
    }.
End SpecializedFunctor.
Arguments MorphismOf {objC%type} [C%category] {objD%type} [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch.

Section FunctorComposition.
End FunctorComposition.

Section IdentityFunctor.
  Context `(C : @SpecializedCategory objC).


  Polymorphic Definition IdentityFunctor : SpecializedFunctor C C.
admit.
Defined.
End IdentityFunctor.

Section IdentityFunctorLemmas.
End IdentityFunctorLemmas.

Section SpecializedNaturalTransformation.
  Context `(C : @SpecializedCategory objC).
  Context `(D : @SpecializedCategory objD).
  Variables F G : SpecializedFunctor C D.


  Polymorphic Record SpecializedNaturalTransformation :=
    {
      ComponentsOf :> forall c, D.(Morphism) (F c) (G c);
      Commutes : forall s d (m : C.(Morphism) s d),
                   Compose (ComponentsOf d) (F.(MorphismOf) m) = Compose (G.(MorphismOf) m) (ComponentsOf s)
    }.
End SpecializedNaturalTransformation.

Section NaturalTransformationComposition.
  Context `(C : @SpecializedCategory objC).
  Context `(D : @SpecializedCategory objD).
  Variables F F' F'' : SpecializedFunctor C D.



  Polymorphic Definition NTComposeT (T' : SpecializedNaturalTransformation F' F'') (T : SpecializedNaturalTransformation F F') :
    SpecializedNaturalTransformation F F''.
admit.
Defined.
End NaturalTransformationComposition.

Section IdentityNaturalTransformation.
  Context `(C : @SpecializedCategory objC).
  Context `(D : @SpecializedCategory objD).
  Variable F : SpecializedFunctor C D.


  Polymorphic Definition IdentityNaturalTransformation : SpecializedNaturalTransformation F F.
admit.
Defined.
End IdentityNaturalTransformation.

Section ProductCategory.
  Context `(C : @SpecializedCategory objC).
  Context `(D : @SpecializedCategory objD).

  Polymorphic Definition ProductCategory : @SpecializedCategory (objC * objD)%type.
  refine (@Build_SpecializedCategory _
                                     (fun s d => (C.(Morphism) (fst s) (fst d) * D.(Morphism) (snd s) (snd d))%type)
                                     (fun o => (Identity (fst o), Identity (snd o)))
                                     (fun s d d' m2 m1 => (Compose (fst m2) (fst m1), Compose (snd m2) (snd m1)))
                                     _
                                     _
                                     _); admit.
  Defined.
End ProductCategory.

Infix "*" := ProductCategory : category_scope.

Local Open Scope category_scope.
Polymorphic Definition OppositeComputationalCategory `(C : @ComputationalCategory objC) : ComputationalCategory objC :=
  @Build_ComputationalCategory objC
                               (fun s d => Morphism C d s)
                               (Identity (C := C))
                               (fun _ _ _ m1 m2 => Compose m2 m1).

Polymorphic Instance OppositeIsSpecializedCategory `(H : @IsSpecializedCategory objC C) : IsSpecializedCategory (OppositeComputationalCategory C) :=
  @Build_IsSpecializedCategory objC (OppositeComputationalCategory C)
                               (fun _ _ _ _ _ _ _ => @Associativity_sym _ _ _ _ _ _ _ _ _ _)
                               (fun _ _ _ _ _ _ _ => @Associativity _ _ _ _ _ _ _ _ _ _)
                               (fun _ _ => @RightIdentity _ _ _ _ _)
                               (fun _ _ => @LeftIdentity _ _ _ _ _).

Polymorphic Definition OppositeCategory `(C : @SpecializedCategory objC) : @SpecializedCategory objC :=
  @Build_SpecializedCategory' objC
                              (OppositeComputationalCategory (UnderlyingCCategory C))
                              _.

Section FunctorCategory.
  Context `(C : @SpecializedCategory objC).
  Context `(D : @SpecializedCategory objD).


  Polymorphic Definition FunctorCategory : @SpecializedCategory (SpecializedFunctor C D).
  refine (@Build_SpecializedCategory _
                                     (SpecializedNaturalTransformation (C := C) (D := D))
                                     (IdentityNaturalTransformation (C := C) (D := D))
                                     (NTComposeT (C := C) (D := D))
                                     _
                                     _
                                     _); admit.
  Defined.
End FunctorCategory.

Notation "C ^ D" := (FunctorCategory D C) : category_scope.


Fixpoint CardinalityRepresentative (n : nat) : Set :=
  match n with
    | O => Empty_set
    | 1 => unit
    | S n' => (CardinalityRepresentative n' + unit)%type
  end.

Coercion CardinalityRepresentative : nat >-> Sortclass.

Polymorphic Definition NatCategory (n : nat) := Eval unfold DiscreteCategory, DiscreteCategory_Identity in DiscreteCategory n.

Coercion NatCategory : nat >-> SpecializedCategory.
Polymorphic Definition TerminalCategory : SmallSpecializedCategory _ := 1.

Section Law4.

  Section ComputableCategory.
    Variable I : Type.
    Variable Index2Object : I -> Type.
    Variable Index2Cat : forall i : I, @SpecializedCategory (@Index2Object i).
  End ComputableCategory.

  Section CommaSpecializedCategory.

    Context `(A : @SpecializedCategory objA).
    Context `(B : @SpecializedCategory objB).
    Context `(C : @SpecializedCategory objC).
    Variable S : SpecializedFunctor A C.
    Variable T : SpecializedFunctor B C.





    Polymorphic Record CommaSpecializedCategory_Object := { CommaSpecializedCategory_Object_Member :> { Î±Î² : objA * objB & C.(Morphism) (S (fst Î±Î²)) (T (snd Î±Î²)) } }.

    Let SortPolymorphic_Helper (A T : Type) (Build_T : A -> T) := A.

    Polymorphic Definition CommaSpecializedCategory_ObjectT := Eval hnf in SortPolymorphic_Helper Build_CommaSpecializedCategory_Object.
    Polymorphic Definition Build_CommaSpecializedCategory_Object' (mem : CommaSpecializedCategory_ObjectT) := Build_CommaSpecializedCategory_Object mem.
    Global Coercion Build_CommaSpecializedCategory_Object' : CommaSpecializedCategory_ObjectT >-> CommaSpecializedCategory_Object.

    Polymorphic Record CommaSpecializedCategory_Morphism (Î±Î²f Î±'Î²'f' : CommaSpecializedCategory_ObjectT) := { CommaSpecializedCategory_Morphism_Member :>
                                                                                                                                                       { gh : (A.(Morphism) (fst (projT1 Î±Î²f)) (fst (projT1 Î±'Î²'f'))) * (B.(Morphism) (snd (projT1 Î±Î²f)) (snd (projT1 Î±'Î²'f')))  |
                                                                                                                                                         Compose (T.(MorphismOf) (snd gh)) (projT2 Î±Î²f) = Compose (projT2 Î±'Î²'f') (S.(MorphismOf) (fst gh))
                                                                                                                                                       }
                                                                                                            }.

    Polymorphic Definition CommaSpecializedCategory_MorphismT (Î±Î²f Î±'Î²'f' : CommaSpecializedCategory_ObjectT) :=
      Eval hnf in SortPolymorphic_Helper (@Build_CommaSpecializedCategory_Morphism Î±Î²f Î±'Î²'f').
    Polymorphic Definition Build_CommaSpecializedCategory_Morphism' Î±Î²f Î±'Î²'f' (mem : @CommaSpecializedCategory_MorphismT Î±Î²f Î±'Î²'f') :=
      @Build_CommaSpecializedCategory_Morphism _ _ mem.
    Global Coercion Build_CommaSpecializedCategory_Morphism' : CommaSpecializedCategory_MorphismT >-> CommaSpecializedCategory_Morphism.

    Polymorphic Definition CommaSpecializedCategory_Compose s d d'
                (gh : CommaSpecializedCategory_MorphismT d d') (g'h' : CommaSpecializedCategory_MorphismT s d) :
      CommaSpecializedCategory_MorphismT s d'.
admit.
Defined.

    Polymorphic Definition CommaSpecializedCategory_Identity o : CommaSpecializedCategory_MorphismT o o.
admit.
Defined.

    Polymorphic Definition CommaSpecializedCategory : @SpecializedCategory CommaSpecializedCategory_Object.
    match goal with
      | [ |- @SpecializedCategory ?obj ] =>
        refine (@Build_SpecializedCategory obj
                                           CommaSpecializedCategory_Morphism
                                           CommaSpecializedCategory_Identity
                                           CommaSpecializedCategory_Compose
                                           _ _ _
               )
    end; admit.
    Defined.
  End CommaSpecializedCategory.

  Local Notation "S â†“ T" := (CommaSpecializedCategory S T).

  Section SliceSpecializedCategory.
    Context `(A : @SpecializedCategory objA).
    Context `(C : @SpecializedCategory objC).
    Variable a : C.
    Variable S : SpecializedFunctor A C.
    Let B := TerminalCategory.

    Polymorphic Definition SliceSpecializedCategory_Functor : SpecializedFunctor B C.
    refine {| ObjectOf := (fun _ => a);
              MorphismOf := (fun _ _ _ => Identity a)
           |}; admit.
    Defined.

    Polymorphic Definition SliceSpecializedCategory := CommaSpecializedCategory S SliceSpecializedCategory_Functor.


  End SliceSpecializedCategory.

  Section SliceSpecializedCategoryOver.
    Context `(C : @SpecializedCategory objC).
    Variable a : C.

    Polymorphic Definition SliceSpecializedCategoryOver := SliceSpecializedCategory a (IdentityFunctor C).
  End SliceSpecializedCategoryOver.

  Section CommaCategory.
  End CommaCategory.


  Section CommaCategoryInducedFunctor.
    Context `(A : @SpecializedCategory objA).
    Context `(B : @SpecializedCategory objB).
    Context `(C : @SpecializedCategory objC).

    Let CommaCategoryInducedFunctor_ObjectOf s d (m : Morphism ((OppositeCategory (C ^ A)) * (C ^ B)) s d)
        (x : fst s â†“ snd s) : (fst d â†“ snd d)
      := existT _
                (projT1 x)
                (Compose ((snd m) (snd (projT1 x))) (Compose (projT2 x) ((fst m) (fst (projT1 x))))) :
           CommaSpecializedCategory_ObjectT (fst d) (snd d).

    Let CommaCategoryInducedFunctor_MorphismOf s d m s0 d0 (m0 : Morphism (fst s â†“ snd s) s0 d0) :
      Morphism (fst d â†“ snd d)
               (@CommaCategoryInducedFunctor_ObjectOf s d m s0)
               (@CommaCategoryInducedFunctor_ObjectOf s d m d0).
      refine (_ : CommaSpecializedCategory_MorphismT _ _); subst_body; simpl in *.
      exists (projT1 m0);
        simpl in *; clear.
      admit.
    Defined.

    Polymorphic Definition CommaCategoryInducedFunctor s d (m : Morphism ((OppositeCategory (C ^ A)) * (C ^ B)) s d) :
      SpecializedFunctor (fst s â†“ snd s) (fst d â†“ snd d).
    refine (Build_SpecializedFunctor (fst s â†“ snd s) (fst d â†“ snd d)
                                     (@CommaCategoryInducedFunctor_ObjectOf s d m)
                                     (@CommaCategoryInducedFunctor_MorphismOf s d m)
                                     _
                                     _
           );
      subst_body; simpl; clear;

      admit.

    Defined.
  End CommaCategoryInducedFunctor.
  Context `(A : LocallySmallSpecializedCategory objA).
  Context `(B : LocallySmallSpecializedCategory objB).
  Context `(C : SpecializedCategory objC).

  Polymorphic Lemma sig_JMeq A0 A1 B0 B1 (a : @sig A0 A1) (b : @sig B0 B1) : A1 == B1 -> proj1_sig a == proj1_sig b -> a == b.
  intros.
  destruct a, b.
  simpl in *.
  destruct H0. (* Commenting out [destruct H0.] gets rid of the Universe Inconsistency. *)
  admit.
  Defined.

  Set Printing Universes.

  Polymorphic Lemma foo  (x : SpecializedFunctor A C * SpecializedFunctor B C)
              (s d : CommaSpecializedCategory_Object (fst x) (snd x))
              (m : CommaSpecializedCategory_Morphism s d)
  : MorphismOf
      (CommaCategoryInducedFunctor
         (IdentityNaturalTransformation (fst x),
          IdentityNaturalTransformation (snd x))) m == m.
  Proof.
    destruct m as [m]; expand.
    match goal with
      | [ |- JMeq (?f ?x) (?g ?y) ] =>
        let x' := fresh "x'" in
        set (x' := x);
          simpl in x';
          let H := fresh in
          pose proof (@f_equal_JMeq _ _ _ _ x' y f g) as H;
            apply H;
            clear H;
            subst x'
    end;
      intros; simpl in *; try ((apply sig_JMeq; fail 1) || admit).
    apply sig_JMeq.
    admit.

Illegal application (preemptive lowering of Type to Set?)

This works in Coq 8.4, but not HoTT/coq.

The fragment of the code in #36 which reproduces this is:

Set Implicit Arguments.
Set Universe Polymorphism.
Generalizable All Variables.

Record SpecializedCategory (obj : Type) :=
  {
    Object :> _ := obj
  }.

Record > Category :=
  {
    CObject : Type;
    UnderlyingCategory :> @SpecializedCategory CObject
  }.

Record SpecializedFunctor `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) :=
  {
    ObjectOf :> objC -> objD
  }.

Definition Functor (C D : Category) := SpecializedFunctor C D.

Parameter TerminalCategory : SpecializedCategory unit.

Definition focus A (_ : A) := True.

Definition CommaCategory_Object (A : Category) (S : Functor TerminalCategory A) : Type.
  assert (Hf : focus ((S tt) = (S tt))) by constructor.
  progress change CObject with (fun C => @Object (CObject C) C) in *;
    simpl in *.
  let V := match type of Hf with
             | focus ?V => constr:(V)
           end
  in exact V.
(* Toplevel input, characters 89-96:
Error: Illegal application:
The term "ObjectOf" of type
 "forall (objC : Set) (C : SpecializedCategory objC)
    (objD : Type) (D : SpecializedCategory objD),
  SpecializedFunctor C D -> objC -> objD"
cannot be applied to the terms
 "Object TerminalCategory" : "Type"
 "TerminalCategory" : "SpecializedCategory unit"
 "Object A" : "Type"
 "UnderlyingCategory A" : "SpecializedCategory (CObject A)"
 "S" : "Functor TerminalCategory A"
 "tt" : "unit"
The 1st term has type "Type" which should be coercible to
"Set". *)
Defined.

Unification in inductives is not done up to eta-expansion; alternatively, inference eta-expands where it should not

The following code works in Coq 8.4, but not HoTT/coq:

Require Import Classes.RelationClasses List Setoid.

Definition RowType := list Type.

Inductive RowTypeDecidable (P : forall T, relation T) `(forall T, Equivalence (P T))
: RowType -> Type :=
| RTDecNil : RowTypeDecidable P _ nil
| RTDecCons : forall T Ts, (forall t0 t1 : T,
                              {P T t0 t1} + {~P T t0 t1})
                           -> RowTypeDecidable P _ Ts
                           -> RowTypeDecidable P _ (T :: Ts).
(* Toplevel input, characters 15-378:
Error:
Last occurrence of "RowTypeDecidable" must have "H" as 2nd argument in
 "RowTypeDecidable P (fun T : Type => H T) nil". *)

"Cannot instantiate metavariable" error breaks through [try] and breaks backtracking.

This code succeeds in Coq 8.4:

Goal forall (O obj : Type) (f : O -> obj) (x : O) (e : x = x)
     (T : obj -> obj -> Type) (m : forall x0 : obj, T x0 x0),
   match eq_sym e in (_ = y) return (T (f y) (f x)) with
   | eq_refl => m (f x)
   end = m (f x).
intros.
try case e.

In HoTT/coq, I get

Toplevel input, characters 19-25:
Error: Cannot instantiate metavariable P of type
"forall a : O, x = a -> Prop" with abstraction
"fun (x : O) (e : x = x) =>
 match eq_sym e in (_ = y) return (T (f y) (f x)) with
 | eq_refl => m (f x)
 end = m (f x)" of incompatible type "forall x : O, x = x -> Prop".

which should not happen, because I wrapped the case e in a try.

Feature request/memoryful 'assert'?

curretly, the assert tactic doesn't like to tell you how you proved a thing (which admittedly sometimes is the right thing to do) and set doesn't let you interactively construct the thing wanted. Could not a case be written for set ( ident : type ) that allows interactive construction of the term, and remembers the eventual construction?

Universe Polymorphism checking inside opaque terms? (Difference between [Qed.] vs [Opaque])

I have some code in a file Functor.v, that when I change two lemmas from Lemma foo : fooT. ... Qed. to Lemma foo : fooT. ... Defined. Global Opaque foo., the time to compile another file shoots up from around 4 minutes to around 90 minutes (I think; I haven't yet fully tracked down the issue, but I'm somewhat confident this is the issue).

With Qeds, the times are:

jgross@cagnode17:~/catdb$ time coqc -q -I . -dont-load-proofs LaxCommaCategory

real    3m47.426s
user    3m45.970s
sys     0m1.300s
jgross@cagnode17:~/catdb$ time coqc -q -I . LaxCommaCategory

real    4m3.526s
user    4m1.895s
sys     0m1.300s

With Defined + Opaque, the time is

real    119m57.947s
user    118m8.419s
sys     0m2.748s

Is universe polymorphism checked differently for Qeded lemmas vs opaque lemmas?

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

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?