Notes on existing work [00BB]

1. Classical Species [00BA]

Groupoid cardinality as motivation

1.1. Groupoid Cardinality [007L]

Definition 1.1.1. Groupoid [007M]

A groupoid is a category in which every morphism is an isomorphism.

Example 1.1.2. finite Sets with bijections [007N]

It is easy to see that the category of finite sets with bijections as morphisms forms a groupoid. We will denote this category with .

Definition 1.1.3. Set [007O]

We can view a set as the groupoid with the sets elements as objects and identity morphism only. Essentially a set is the most boring kind of groupoid we can think about since its points carry no symmetries.

Definition 1.1.4. Coproduct of Groupoids [007W]

TODO. Essentially just disjoint union.

Lemma 1.1.5. [007Y]

TODO. Cardinality of coproduct is sum of cardinality.

Definition 1.1.6. Product of Groupoids [007X]

TODO. Objects are pairs of G and H, morphisms are pairs of morphisms.

Lemma 1.1.7. [007Z]

TODO. Cardinality of product is product of cardinality.

We now want to extend our definition of a cardinality from sets to groupoids. To make this a nice definition it should be invariant under equivalences.

Definition 1.1.8. Groupoid Cardinality [007P]

For the cardinality of a groupoid we pick a representative for each isomorphism class of objects in . Each representative then contributes to the formal sum by , where denotes the cardinality of the automorphism group of x. In symbols

In the case where is finite for all and the series converges we may evaluate it to a real number.

Remark 1.1.9. [007R]

Notice how the definition of groupoid cardinality is crafted explicitly to be an invariant with respect to equivalence of categories.

Proof. TODO

Consider for example the terminal category as well as the groupoid with two isomorphic objects and the obvious 4 morphisms. Both are equivalent as categories and indeed they both have cardinality 1.

Observation 1.1.10. rational cardinalities [007S]

Other than sets, proper Groupoids may admit non-integer cardinalities. The groupoid consisting of a single point with 3 automorphisms has cardinality .

Example 1.1.11. Eulers Number [007T]

The cardinality of the the groupoid of is eulers number .

Definition 1.1.12. Weak Quotient / action groupoid [007U]

TODO

1.1.13. |S//G| = |S|/|G| [007V]

Definition 1.1.14. Exponent [0080]

TODO

Species count the number of structure of a specific type that one can put on a finite set of labels. Formally we define a species as follows.

Definition 1.2. Species [0081]

A (combinatorial) species is a functor . Given a finite set of labels we let denote the set of -structures one can put on the set.

Example 1.3. two-colorings [0082]

TODO

Example 1.4. graphs [0083]

TODO

The above are examples where there is only a finite number of ways to put a structure on a given finite set. But our definition of a species permits degenerate examples like the following.

Example 1.5. not so tame species [0085]

For a finite set define as the set of all real valued funcitons with domain .

Definition 1.6. tame [0086]

We call a species tame if is finite for every finite set .

Idea 1.7. [0084]

We consider the action groupoid of the symmetric group acting of F(n). This should give rise to the generating function of species quite naturally.

–

generating functions
Coproduct
Hamard Product
Cauchy-Product
Catalan Numbers and binary rooted trees
species count things up to isomorphism

-> univalence

species as dependent types

2. Species of Types [008K]

This is a small attempt at deformalizing the foundational work on species that is present in agda-unimath with the goal to be more human-readable.

See agda-unimath/species

TODO LIST
--- species of types ---
- [x] species-of-types
- [x] equivalences-species-of-types
- [x] morphisms-species-of-types 
- [x] coproducts-species-of-types 
- [x] cauchy-products-species-of-types 
- [x] cartesian-exponents-species-of-types
- [x] cartesian-products-species-of-types
- [x] cauchy-exponentials-species-of-types
- [ ] dirichlet-exponentials-species-of-types (long)
- [ ] dirichlet-products-species-of-types (easy)
- [ ] cycle-index-series-species-of-types (interesting)
- [ ] derivatives-species-of-types (easy)

--- cauchy series of species of types ---
- [x] cauchy-series-species-of-types 
- [ ] products-cauchy-series-species-of-types (easy)
- [ ] composition-cauchy-series-species-of-types (long)
- [ ] exponentials-cauchy-series-of-types (mid)

--- dirichlet product of species of types ---
- [ ] dirichlet-series-species-of-types (easy)
- [ ] products-dirichlet-series-species-of-types (long)

--- cauchy composition of species of types ---
- [ ] cauchy-composition-species-of-types (long)
- [ ] unit-cauchy-composition-species-of-types (easy)

--- species of types in subuniverses ---
- [ ] cauchy-exponentials-species-of-types-in-subuniverses (long)
- [ ] cauchy-products-species-of-types-in-subuniverses (long)
- [ ] cauchy-series-species-of-types-in-subuniverses 
- [ ] products-cauchy-series-species-of-types-in-subuniverses 
- [ ] composition-cauchy-series-species-of-types-in-subuniverses (long)
- [ ] dirichlet-series-species-of-types-in-subuniverses 
- [ ] products-dirichlet-series-species-of-types-in-subuniverses 
- [ ] cauchy-composition-species-of-types-in-subuniverses (long)
- [ ] unit-cauchy-composition-species-of-types-in-subuniverses 
- [ ] small-cauchy-composition-species-of-types-in-subuniverses 
- [ ] coproducts-species-of-types-in-subuniverses (long)
- [ ] dirichlet-exponentials-species-of-types-in-subuniverses (long)
- [ ] dirichlet-products-species-of-types-in-subuniverses (long) 
- [ ] equivalences-species-of-types-in-subuniverses 
- [ ] exponentials-cauchy-series-of-types-in-subuniverses 




--- species of finite inhabited types ---
- [ ] species-of-finite-inhabited-types 
- [ ] dirichlet-series-species-of-finite-inhabited-types 
- [ ] products-dirichlet-series-species-of-finite-inhabited-types 
- [ ] small-cauchy-composition-species-of-finite-inhabited-types 

--- other kinds of species ---
- [ ] hasse-weil-species 
- [ ] species-of-finite-types 
- [ ] species-of-inhabited-types 
- [ ] pointing-species-of-types 
- [ ] unlabeled-structures-species 

--- finite species ---
- [ ] morphisms-finite-species 
- [ ] precategory-of-finite-species

2.1. Assuming enough Universes [008L]

We will assume that for every finite list of of types in context trough there exists a universe that contains these types. See Postulate 6.2.1 in Introduction to Homotopy Type Theory

Axiom 2.2. Univalence [008Q]

TODO: write some nice prose here.

2.3. Function Extensionality [008T]

TODO, follows from univalence.

Definition 2.4. Species of Types [008N]

Let and be universes, then a species of types is simply a map .

Note that the type is well-formed if we assume enough universes.

Compare the definition to Joyal's definition of a species.

Definition 2.5. Species (Joyal) [0081]

A (combinatorial) species is a functor . Given a finite set of labels we let denote the set of -structures one can put on the set.

Notice that this definition requires a species to be functorial. Conveniently for any species of types we can get functoriality in the following sense.

2.6. Transport in Species of Types [008P]

Let be a species of types and let , be types in the universe . Then for any equivalence of types , we get obtain a term of type as follows.

By univalence we upgrade to a path . Then transport gives us the desired map.

2.7. Equivalence of Species of Types [008S]

An equivalence of species is a pointwise equivalence of types. In symbols: For species and we define the type of equivalences as

2.8. Species of Types are extensional [008R]

The identity type of species is equivalent to the type of equivalences between them. This is immediate by function extensionality

Definition 2.9. Morphism of Species of Types [008U]

Let and be species of types. We define the type of and to be . We denote it by .

2.10. Homotopy of Morphisms of Species of Types [008V]

Let and be species of types and let and be morphisms of species of types between and . We define the type of homotopies between and as the type of pointwise homotopies, in symbols .

Definition 2.11. Torsorial Homotopy of Morphisms of Species of Types [008W]

TODO

Definition 2.12. Cauchy Series of Species of Types [008X]

Let be a species of types. We define the cauchy series of at as the type

TODO: Motivate this definition using the "classical" generating function
TODO: Equivalent Species of types have equivalent cauchy series
TODO: Cauchy series are equivalence invariant.

–> should both follow from univalence easily?

Definition 2.13. Cauchy Product of Species of Types [008Y]

Let and be species of types. We define the cauchy product of and on as

Remark 2.14. [00B0]

The cauchy product captures the idea of putting both an -structure and a -structure on by writing as a coproduct of and putting an -structure one one summand and a -structure on the other.

Definition 2.15. Cartesian exponent of species of types [00B1]

Given species of types and , we define the cartesian exponent of and at as the pointwise exponent

Definition 2.16. Cartesian product species of types [00B2]

The cartesian product of two species of types and at is their pointwise cartesian product

TODO: The adjunction between cartesian products and exponents of species of types

Definition 2.17. Cauchy exponential species of types [00BC]

For a species and we define the cauchy exponential at as

TODO: The Cauchy exponential in terms of composition

The proof of the below proposition is not the one given in agda-unimath.

Proposition 2.18. [00BD]

Let and be species of types. The cauchy exponential fullfills the following identity.

Proof. We give an equivalence by contructing maps and that are mutual inverses.

Forward map . Given an element of the LHS i.e a term with

we need write as a binary coproduct such that we can put an exp-structure on each summand.

We start by splitting into subtypes and as follows. TODO: are these actually subtypes?

Now we choose our summands as

Since , we can upgrade to an equivalence equivalence .

Now we want to place an - and -structure on and repectively. For this we need to construct the remaining terms.

Now

This completes our construction of . Notice that

Reverse map . We are given an element with

, define

then

giving . Define

And .

TODO: Make sure and really compose to the identity both ways.

—

How important is it to track universes closely when working informally? Can we just say F(X) and G(X) is a species without worrying about the universes that index them?