Formalisierung der grundlegenden Kategorietheorie in Coq

Ich bin ein absoluter Anfänger in Coq und ich versuche, einige kategorietheoretische Dinge als Übung zu implementieren.

Ich habe ein wenig unter den Git-Repos der vielen verfügbaren Implementierungen (HoTT, Awodeys Coq-Begleiter usw.) gesurft. Es scheint, dass jedes einzelne Projekt so etwas implementiert

Record Category : Type :=
  mkCategory{
    ob : Type ;
    mor : ob -> ob -> Type ;
    compose : forall x y z : ob,
                mor x y -> mor y z -> mor x z ;
    identity : forall x, mor x x ;
    (* ... axioms ... *)
  }.

Es ist eine Art natürlich, wenn man die meisten Definitionen von Kategorien in modernen Büchern berücksichtigt. Ich bin jedoch der Meinung, dass es einfacher wäre, es intern zu implementieren (wenn nicht falsch, war es zu Grothendiecks Zeiten die übliche Definition):

Definition. Eine Kategorie sind die Daten von

eine Menge / Klasse von Objekten, $\rm Ob$

eine Gruppe / Klasse von morphisms, $\rm Mor$

Funktionen und ( steht für Quelle , $s,t \colon {\rm Mor} \to {\rm Ob}$ $i \colon {\rm Ob} \to {\rm Mor}$ $s$ $t$ für Ziel und $i$ für Identität )

eine Funktion $\circ \colon {\rm Mor} \times_{s,t} {\rm Mor} \to {\rm Mor}$ deren Domäne ist das Faserprodukt von $M o r \overset{s}{\to} O b \overset{t}{\leftarrow} M o r$ ${\rm Mor} \stackrel s \to {\rm Ob} \stackrel t \leftarrow {\rm Mor}$

einige Axiome befriedigen ...

Der Vorteil einer solchen Definition besteht darin, dass sie direkt verallgemeinert wird, indem "Menge / Klasse" durch "Objekte einer bestimmten Kategorie" und "Funktionen" durch "Morphismen dieser Kategorie" ersetzt werden, was zum Konzept der internen Kategorie führt . (Dann können Sie von topologischen / differenziellen Kategorien oder Kategorien innerhalb eines Topos usw. sprechen.)

Mein Problem ist die Formalisierung des Faserprodukts in Coq. Mein erster Versuch wäre, so etwas zu tun

Record Category : Type :=
  mkCategory{
    ob : Type ;
    mor : Type ;
    s : mor -> ob ;
    t : mor -> ob ;
    compose : mor -> mor -> option mor ;
    i : ob -> mor ;

    adequacy : forall f g : mor, 
                 (exists h, (compose f g) = (some h)) -> (t f = s g) ;
    (* ... axioms ... *)
  }.

Aber ich denke, das könnte zu einem lästigen späteren Code führen. Beispielsweise wären verkettete Zusammensetzungen schwer zu lesen.

Gibt es ein Projekt mit einer Implementierung, die auf der internen Definition basiert? Gibt es eine schnelle Möglichkeit, das Faserprodukt zu definieren, das ich in Coq benötige?

Bearbeiten. Übrigens sehe ich viel

Ob :> Type

eher von

Ob : Type

Was bedeutet das zusätzliche ">"? Aus dem Dokument geht hervor, dass es sich um eine Art Zwang handelt . Was genau bedeutet das?

reference-request category-theory coq Pece
quelle

Um die zusätzliche Frage schnell zu beantworten, ist ein Zwang ein Gerät, mit dem ein Typ auf irgendeine Weise als ein anderer Typ behandelt werden kann. Dies ist ein gutes Beispiel. Ich habe diese genaue Syntax noch nie gesehen, also muss es sich um eine "spezielle" Art von Zwang handeln (wahrscheinlich eine triviale, dh alles kann eine sein Ob)?

Luke Mathieson

Siehe auch coq.inria.fr/refman/Reference-Manual021.html (obwohl das nur das Wasser trüben kann)

Luke Mathieson

Nur als Randnotiz sollten Sie wissen, dass abhängige Typen in coq sehr verfügbar sind und genau diesen Begriff des Faserprodukts erfassen! Eine natürliche Art, dies zu schreiben, wäre, mor abhängig von sund tz mor: forall s t : ob, Type.

Cody

@cody Ist das nicht der erste Ansatz (den ich nicht will)? Das Symbol

s

$s$ und

t

$t$ stehen soll nicht für Objekte , sondern für die Funktion Quelle und Ziel . Stellen Sie sich Diagramme anstelle von Kategorien vor: Der erste Ansatz definiert ein Diagramm als eine Menge von Eckpunkten und für jedes (sortierte) Paar eine Reihe von Kanten, während der zweite Ansatz ein Diagramm als zwei Mengen V und E definiert (V für die Eckpunkte, E für alle egdes) mit zwei anwendungen

s, t : E ⇉ V

$s,t \colon E \rightrightarrows V$ Bezeichnung der Quelle und des Ziels jeder Kante.

Pece

Oh, richtig, es tut mir leid, ich habe deinen ersten Punkt verpasst. Es scheint jedoch, dass Sie gegen genau den Punkt argumentieren, den Sie

ansprechen möchten

Antworten:

Eine natürliche Möglichkeit, aufzuschreiben, was Sie möchten, besteht darin , die Art der Komposition nur auf die "zusammensetzbaren" Morphismen zu beschränken:

c o m p o s e : \forall f g : m o r, t (f) = s (g) \to m o r

$\mathrm{compose}:\forall f\ g: \mathrm{mor}, t(f) = s(g)\rightarrow \mathrm{mor}$

natürlich die Bedingungen hinzufügen:

s (c o m p o s e f g e) = s (f)

$s(\mathrm{compose}\ f\ g\ e)=s(f)$

t (c o m p o s e f g e) = t (g)

$t(\mathrm{compose}\ f\ g\ e)=t(g)$

Dies funktioniert, da jetzt nur Funktionen komponiert werden können, die nachweislich komponierbar sind. Dies entspricht in etwa dem von Ihnen erwähnten Faserprodukt in der Kategorietheorie.

Dies ist jedoch etwas umständlich, da es jeder Anwendung von Beweispflichten hinzufügt compose, die schnell unüberschaubar werden können (selbst das Ausdrücken von Assoziativität ist schwierig!). Außerdem wird das Hinzufügen der Notation etwas ausgeschlossen $\circ=\mathrm{compose}$ , da composedauert 3 Argumente.

Dies ist ein etwas verbreitetes Problem in der Typentheorie, das sich aus der fundamentalen Spannung ergibt, Teilfunktionen in einer Gesamtsprache zu haben.

Eine andere, weniger elegante Lösung besteht darin, die Komposition so zu definieren, dass sie überall definiert wird :

c o m p o s e : m o r \to m o r \to m o r

$\mathrm{compose} :\mathrm{mor}\rightarrow\mathrm{mor}\rightarrow\mathrm{mor}$ und bewache jeden Satz, der Komposition mit genau definierten Bedingungen beinhaltet:

a s s o c : \forall f g h : m o r, t (f) = s (g) \land t (g) = s (h) \Rightarrow c o m p o s e f (c o m p o s e g h) = c o m p o s e (c o m p o s e f g) h

$\mathrm{assoc}:\forall f g h:\mathrm{mor}, t(f)=s(g)\wedge t(g)=s(h)\Rightarrow\\ \mathrm{compose}\ f\ (\mathrm{compose}\ g\ h) = \mathrm{compose}\ (\mathrm{compose}\ f\ g)\ h$ Dies bedeutet im Wesentlichen:

composewird überall definiert, aber die Definition ist nur dann sinnvoll, wenn sie auf zusammensetzbare Morphismen angewendet wird.

Dieser Ansatz hat auch Nachteile, hauptsächlich die gigantische Menge an Beweispflichten, die jeder Anwendung der Grundaxiome folgen.

Ich fürchte, Sie müssen in diesem Fall Ihr Gift auswählen oder einen cleveren Weg finden, um es besser zu machen ...

Cody
quelle

Möglicherweise müssen Sie auch eine Hypothese zur Irrelevanz von Beweisen hinzufügen: Sicherlich das Ergebnis des Komponierens fund gsollte nicht von dem Beweis abhängen, edass t(f)=s(g)...

Gallais

Ich denke, obwohl dieses Problem in den meisten Kontexten nicht auftreten sollte, in denen es nur einen Beweis dafür gibt, dass man t(f) = s(g)herumliegt (z. B. wenn die Gleichheit von Objekten entscheidbar ist).

Cody

Nach einigen Kämpfen denke ich, dass der beste Weg, das zu tun, was ich will, darin besteht, das Faserprodukt des Typs tatsächlich durch seine universelle Eigenschaft zu codieren.

Es geht in diese Richtung:

Class FiberProduct (A B C : Type) (f : A -> C) (g : B -> C) : Type :=
  {
    FiberProductCarrier : Type ;
    FiberProductProj_1 : FiberProductCarrier -> A ;
    FiberProductProj_2 : FiberProductCarrier -> B ;
    FiberProductCommutativity :
      forall x : FiberProductCarrier,
        f (FiberProductProj_1 x) = g (FiberProductProj_2 x) ;
    FiberProductUniversalExistence :
      forall X : Type, forall (p_1 : X -> A) (p_2 : X -> B),
        (forall x : X, f (p_1 x) = g (p_2 x)) ->
        (exists h : X -> FiberProductCarrier,
           (forall x : X, FiberProductProj_1 (h x) = p_1 x
                          /\ FiberProductProj_2 (h x) = p_2 x)) ;
    FiberProductUniversalUniqueness :
      forall X : Type, forall (p_1 : X -> A) (p_2 : X -> B),
        (forall x : X, f (p_1 x) = g (p_2 x)) ->
        (forall k l : X -> FiberProductCarrier,
           (forall x : X, FiberProductProj_1 (k x) = p_1 x
                          /\ FiberProductProj_2 (k x) = p_2 x
                          /\ FiberProductProj_1 (l x) = p_1 x
                          /\ FiberProductProj_2 (l x) = p_2 x)
           -> k = l)
  }.

Dann ist die interne Version des Begriffs der Kategorie gegeben durch:

Class InternalCategory : Type :=
  {
    ob : Type ;
    mor : Type ;
    s : mor -> ob ;
    t : mor -> ob ;
    i : ob -> mor ;
    comp_domain : FiberProduct mor mor ob s t ;
    comp : FiberProductCarrier  -> mor  ;
    (* axioms *)
    asso :
      forall fg_h f_gh : FiberProductCarrier,
        (exists fg gh : FiberProductCarrier,
           FiberProductProj_1 fg_h = comp fg /\
           FiberProductProj_2 f_gh = comp gh /\
           FiberProductProj_1 fg = FiberProductProj_1 f_gh /\
           FiberProductProj_2 fg = FiberProductProj_1 gh /\
           FiberProductProj_2 gh = FiberProductProj_2 fg_h) ->
        (comp fg_h = comp f_gh) ;
    id_right :
      forall fid : FiberProductCarrier,
      forall f : mor,
        (FiberProductProj_1 fid = f) ->
        (exists x : ob, FiberProductProj_2 fid = i x) ->
        (comp fid = f) ;
    id_left :
      forall idf : FiberProductCarrier,
      forall f : mor,
        (FiberProductProj_2 idf = f) ->
        (exists x : ob, FiberProductProj_1 idf = i x) ->
        (comp idf = f) ;
    id_s :
      forall x, s (i x) = x ;
    id_t :
      forall x, t (i x) = x          
  }.

Pece
quelle