Quelle bug_14221.v Sprache: Coq

Axiom proof_admitted : False.
Tactic Notation "admit" := abstract case proof_admitted.
Require Corelib.Program.Basics Corelib.Program.Tactics.
Export Corelib.Program.Basics Corelib.Program.Tactics.
Set Primitive Projections.
Set Universe Polymorphism.

Close Scope nat_scope.
Require Setoid.
Require Export Corelib.Classes.CMorphisms.

Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
  (at level 200, x binder, y binder, right associativity).

Class Setoid A := {
  equiv : crelation A;
  setoid_equiv :: Equivalence equiv
}.

Notation "f ≈ g" := (equiv f g) (at level 79).

Ltac cat :=
  intros;
  autorewrite with categories;
  auto with category_laws;
  try reflexivity.

#[export] Hint Extern 4 (equiv ?A ?A) => reflexivity : category_laws.

Ltac proper := repeat intro; simpl; try cat; intuition.

Ltac cat_simpl :=
  program_simpl; autounfold;
  try solve [
    program_simpl; autounfold in *;
    simpl in *; intros;
    simpl in *; cat];
  simpl in *.

Global Obligation Tactic := cat_simpl.

Reserved Infix "~>" (at level 90, right associativity).

Class Category := {
  obj : Type;

  uhom := Type : Type;
  hom : obj -> obj -> uhom where "a ~> b" := (hom a b);
  homset :: ∀ X Y, Setoid (X ~> Y);

  id {x} : x ~> x;
}.

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

Notation "x ~> y" := (@hom _%category x%object y%object)
  (at level 90, right associativity) : homset_scope.
Notation "x ~{ C }~> y" := (@hom C%category x%object y%object)
  (at level 90) : homset_scope.

Notation "id[ x ]" := (@id _%category x%object)
  (at level 9, format "id[ x ]") : morphism_scope.

Coercion obj : Category >-> Sortclass.

Open Scope homset_scope.
Open Scope morphism_scope.

Class Functor (C D : Category) := {
  fobj : C -> D;
  fmap {x y : C} (f : x ~> y) : fobj x ~> fobj y;

  fmap_respects :: ∀ x y, Proper (equiv ==> equiv) (@fmap x y);

  fmap_id {x : C} : fmap (@id C x) ≈ id;
}.
Delimit Scope functor_scope with functor.

Coercion fobj : Functor >-> Funclass.

Notation "fmap[ F ]" := (@fmap _ _ F%functor _ _)
  (at level 9, format "fmap[ F ]") : morphism_scope.

#[export] Hint Rewrite @fmap_id : categories.

Definition Product (C D : Category) : Category := {|
  obj     := C * D;
  hom     := fun x y => (fst x ~> fst y) * (snd x ~> snd y);
  homset  := fun x y =>
    let setoid_C := @homset C (fst x) (fst y) in
    let setoid_D := @homset D (snd x) (snd y) in
    {| equiv := fun f g =>
         (@equiv _ setoid_C (fst f) (fst g) *
          @equiv _ setoid_D (snd f) (snd g))
     ; setoid_equiv := _
         {| Equivalence_Reflexive  := fun x =>
              (@Equivalence_Reflexive _ _ (@setoid_equiv _ setoid_C) (fst x),
               @Equivalence_Reflexive _ _ (@setoid_equiv _ setoid_D) (snd x))
          ; Equivalence_Symmetric  := fun x y f =>
              (@Equivalence_Symmetric
                 _ _ (@setoid_equiv _ setoid_C) (fst x) (fst y) (fst f),
               @Equivalence_Symmetric
                 _ _ (@setoid_equiv _ setoid_D) (snd x) (snd y) (snd f))
          ; Equivalence_Transitive := fun x y z f g =>
              (@Equivalence_Transitive
                 _ _ (@setoid_equiv _ setoid_C) (fst x) (fst y) (fst z)
                 (fst f) (fst g),
               @Equivalence_Transitive
                 _ _ (@setoid_equiv _ setoid_D) (snd x) (snd y) (snd z)
                 (snd f) (snd g)) |} |};
  id      := fun _ => (id, id);
|}.

Section Bifunctor.

Context {C : Category}.
Context {D : Category}.
Context {E : Category}.

Definition bimap {F : Functor (Product C D) E} {x w : C} {y z : D}
           (f : x ~{C}~> w) (g : y ~{D}~> z) :
  F (x, y) ~{E}~> F (w, z) := @fmap (Product C D) E F (x, y) (w, z) (f, g).

Global Program Instance bimap_respects {F : Functor (Product C D) E} {x w : C} {y z : D} :
  Proper (equiv ==> equiv ==> equiv) (@bimap F x w y z).
Next Obligation.
admit.
Defined.

Lemma bimap_id_id {F : Functor (Product C D) E} {x y} :
  bimap (id[x]) (id[y]) ≈ id.
admit.
Defined.

End Bifunctor.

Notation "bimap[ F ]" := (@bimap _ _ _ F%functor _ _ _ _)
  (at level 9, format "bimap[ F ]") : morphism_scope.

#[export] Hint Rewrite @bimap_id_id : categories.

Reserved Infix "⨂" (at level 30, right associativity).

Class Monoidal {C : Category} := {
  tensor : Functor (Product C C) C where "x ⨂ y" := (tensor (x, y));
}.

Notation "x ⨂ y" := (@tensor _ _ (x%object, y%object))
  (at level 30, right associativity) : object_scope.
Notation "f ⨂ g" := (bimap[@tensor _ _] f g)
  (at level 30, right associativity) : morphism_scope.

#[export] Program Instance PP
        {C : Category} {D : Category} `{@Monoidal D}
        {F : Functor C D} {G : Functor C D} : Functor C D := {
  fobj := fun x => (F x ⨂ G x)%object;
  fmap := fun _ _ f => fmap[F] f ⨂ fmap[G] f
}.
Next Obligation.
  proper.
  rewrite X. (* was anomaly undefined universe *)
  reflexivity.
Qed.

quality99%

¤ Dauer der Verarbeitung: 0.4 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.