Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Anomaly: apply_coercion. Please report. #14

Closed
JasonGross opened this issue Feb 15, 2013 · 2 comments
Closed

Anomaly: apply_coercion. Please report. #14

JasonGross opened this issue Feb 15, 2013 · 2 comments

Comments

@JasonGross
Copy link

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.

@mattam82
Copy link
Member

mattam82 commented Apr 4, 2013

Fixed in latest revision.

@mattam82 mattam82 closed this as completed Apr 4, 2013
@JasonGross
Copy link
Author

In trunk-polyproj, this is reponed, and gives Anomaly: apply_coercion_args: mismatch between arguments and coercion.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants