Formalizaciones de la teoría de categorías en asistentes de pruebas.

Question

¿Cuáles son los existentes formalizaciones de la categoría de la teoría en la prueba de los asistentes?

Estoy interesado principalmente en el dominio público el código de la aplicación de la categoría de la teoría en una prueba de ayudante (Coq, Agda, Isabelle/HOL, Mizar, NuPRL, Twelf, Lego, Idris, Matita, etc.), aunque yo también estoy interesado en trabajos sobre formalizaciones de la categoría de la teoría en la prueba de los asistentes.

He añadido las respuestas a esta pregunta para todos los papeles y formalizaciones, que yo sepa, y los detalles acerca de las construcciones en mi propio repositorio a partir de la fecha de la adición. Además de la adición de formalizaciones que no se ve aquí, usted debe sentirse libre para agregar detalles y mejorar el formato de las otras entradas (sobre todo incluyendo lo que en lenguaje de la formalización es, en qué categoría de la teoría que abarca, los enlaces a los documentos que presentan y/o puesta a disposición pública el código fuente, si no es bajo desarrollo activo, lo que la más reciente versión de la prueba auxiliar que se compila con es), etc.).

Answer 1

HoTT/HoTT Categorías

Enlaces: https://github.com/HoTT/HoTT/tree/master/theories/Categories (actual), https://github.com/JasonGross/HoTT-categories (de edad), https://bitbucket.org/JasonGross/catdb (el más antiguo). Índice interactivo, no índice interactivo, de nivel superior de la wiki

Idioma: Coq 8.6; se compila con 8.7 cuando sale; la más antigua versión compilada con Coq 8.4)

Autor: Jason Bruto

Desarrollo activo: No, pero se mantiene activa en su forma actual (junio de 2017)

Conceptos Formalizados:

• 1-precategories (en el sentido de la HoTT Libro)

• univalentes/saturados categorías (o categorías, en la HoTT Libro)

• functor precategories $\mathcal C \to \mathcal D$

• doble functor isomorphisms $\text{Cat} \to \text{Cat}$; y $(\mathcal{C} \to \mathcal{D})^{\text{op}} \to (\mathcal{C}^{\text{op}} \to \mathcal{D}^{\text{op}})$

• la categoría de la Proposición de ($U$-pequeño) hProps

• el Conjunto de la categoría de ($U$-pequeño) hSets

• la categoría de Gato de ($U$-pequeño) estricto (pre)categorías (estricta en el sentido de los objetos que se hSets)

• pseudofunctors

• profunctors

  • identidad profunction (el hom functor $\mathcal C^\text{op} \times \mathcal C \to \text{Set}$)

• adjoints

  • las equivalencias entre una serie de definiciones:
    • unidad-counit + zig-zag definición
    • unidad + UMP definición
    • counit + UMP definición
    • universal de morfismos definición
    • hom-definición de conjunto (portabilidad desde la antigua versión en curso)
  • composición, identidad, doble
  • pointwise adjunctions en la biblioteca, $G^\mathcal{E} \dashv F^\mathcal{C}$ e $\mathcal{E}^F \dashv \mathcal{C}^G$ a partir de la contigüidad $F \dashv G$ para functors $F : \mathcal C \leftrightarrows \mathcal D : G$ e $\mathcal E$ un precategory (todavía demasiado lento para ser incorporadas a la biblioteca adecuada; el código aquí)

• Yoneda lema

• Exponencial de las leyes

  • $\mathcal C^0 \cong 1$; $0^{\mathcal C} \cong 0$ dado un objeto en $\mathcal C$
  • $\mathcal C^1 \cong \mathcal C$; $1^{\mathcal C} \cong 1$
  • $\mathcal C^{\mathcal A + \mathcal B} \cong \mathcal C^{\mathcal A} \times \mathcal C^{\mathcal B}$
  • $(\mathcal A \times \mathcal B)^{\mathcal C} \cong \mathcal A^{\mathcal C} \times \mathcal B^{\mathcal C}$
  • $(\mathcal A^{\mathcal B})^{\mathcal C} \cong \mathcal A^{\mathcal B \times \mathcal C}$
• Producto de las leyes
  • $\mathcal C \times \mathcal D \cong \mathcal D \times \mathcal C$
  • $\mathcal C \times 0 \cong 0 \times \mathcal C \cong 0$
  • $\mathcal C \times 1 \cong 1 \times \mathcal C \cong \mathcal C$
• Grothendieck construcción (oplax colimit) de un pseudofunctor para Gato
• Categoría de secciones (da lugar a oplax límite de una pseudofunctor a Cat cuando se aplica a Grothendieck construcción
• functor composición es functorial (hay un functor $\Delta : (\mathcal C \to \mathcal D) \to (\mathcal D \to \mathcal E) \to (\mathcal C \to \mathcal E)$, donde cada una de las $\mathcal A \to \mathcal B$ es un functor categoría)
• Kan extensiones son adjoints a la functorial composición functor
• (co)de los límites definidos como Kan extensiones cuando una de las categorías es la terminal
• La coma functor $\left(\mathcal C^{\mathcal A}\right)^{\text{op}} \times \mathcal C^{\mathcal B} \to \text{Cat}_{/ \mathcal A \times \mathcal B}$ que envía a $\mathcal A \xrightarrow{f} \mathcal C \xleftarrow{g} \mathcal B$ a de la coma categoría $(f / g)$, y la proyección del functor a $\mathcal A \times \mathcal B$
• monoidal categorías (portabilidad desde la versión más antigua todavía en progreso)
• enriquecido categorías (portabilidad desde la versión más antigua todavía en progreso)

Conceptos actualmente en construcción:

• pseudonatural transformaciones
• (op)lax coma categorías
• pointwise Kan extensiones
• Cartesiano categorías cerradas

La Construcción De Opciones:

• Morfismos son dependiente escrito $\text{Hom}_{\mathcal C} : \text{Ob}_{\mathcal C} \to \text{Ob}_{\mathcal C} \to \text{Type}$
• Morfismos de la tierra en el Tipo; proposicional igualdad se utiliza; más inductivos se utilizan los tipos de cocientes.
• Las categorías son registros sin parámetros y en todos los campos
• Basado en homotopy tipo de teoría; morfismos son hSets (0-truncado; satisfacer UIP)

Answer 2

El artículo Univalentes categorías y la Rezk finalización por Benedikt Ahrens, Chris Kapulkin, Michael Shulman tiene dos versiones:

• publicado en Estructuras Matemáticas en Ciencias de la computación doi:10.1017/S0960129514000486,
• proyecto de auxiliares de archivos,

El código es una parte de la UniMath de la biblioteca, el repositorio original , que ahora está considerado como obsoleto.

La biblioteca incluye:

• precategories
• isomorphisms en precategories
• functors naturales y transformaciones
• varias propiedades de los functors
• sub-precategories
• imagen de la factorización de un functor
• un completo subprecategory de una categoría es una categoría
• definición de contigüidad
• medico adjunto de equivalencia de precategories
• la prueba de que un medico adjunto de equivalencia de categorías de los rendimientos de un débil equivalencia de objetos
• totalmente fieles y esencialmente surjective functor induce la equivalencia de precategories si su origen es una categoría
• definición de la precategory de conjuntos
• la prueba de que se trata de una categoría
• definición de Yoneda la incrustación de
• la prueba de que es totalmente fiel
• definición de whiskering
• precomposición con un totalmente fieles y esencialmente surjective functor rendimientos totalmente fieles functor
• precomposición con un totalmente fieles y esencialmente surjective functor rendimientos esencialmente surjective functor
• Rezk finalización

Answer 3

Wolfram Kahl del RATH-Agda formalización :: http://relmics.mcmaster.ca/RATH-Agda/

" La categoría básica y la alegoría de la teoría de la biblioteca de la RATH-Agda proyecto, que contiene (sólo de forma esporádica, de verdad) alfabetizada teorías que van desde semigroupoids, que son "categorías sin identidad", a la "acción de celosía categorías", que son la división de alegorías, que son al mismo tiempo Kleene categorías (es decir, escrito álgebras de Kleene), incluyendo también monoidal categorías. Estas teorías están pensados como interfaces de programación de alto nivel; esta colección actual incluye implementaciones en particular a través de las relaciones concretas, y una serie de construcciones, incluidos los cocientes por (abstracciones) de parcial de las relaciones de equivalencia. "

Answer 4

Doctorado de Benedikt Ahrens , disponible en arxiv , con código en https://benedikt-ahrens.de/cgi-bin/r.cgi/coq , y un índice de impresión bonita aquí .

Answer 5

La formalización Coq de Nick Benton de la teoría de dominio y los espacios ultramétricos se basa en una formalización básica de categorías concretas. Papel y código . En correspondencia privada, Nick dijo que la principal característica interesante es el uso del patrón de "clases empaquetadas".