JMeq should be a Polymorphic Inductive

[JasonGross]

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.