Univalent Species [007K]

1. Literature [00B9]

2. Notes on existing work [00BB]

2.1. Classical Species [00BA]

Groupoid cardinality as motivation

2.1.1. Groupoid Cardinality [007L]

Definition 2.1.1.1. Groupoid [007M]

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

Example 2.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 2.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 2.1.1.4. Coproduct of Groupoids [007W]

TODO. Essentially just disjoint union.

Lemma 2.1.1.5. [007Y]

TODO. Cardinality of coproduct is sum of cardinality.

Definition 2.1.1.6. Product of Groupoids [007X]

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

Lemma 2.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 2.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 2.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 2.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 2.1.1.11. Eulers Number [007T]

The cardinality of the the groupoid of is eulers number .

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

TODO

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

Definition 2.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 2.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 2.1.3. two-colorings [0082]

TODO

Example 2.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 2.1.5. not so tame species [0085]

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

Definition 2.1.6. tame [0086]

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

Idea 2.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.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.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.2. Univalence [008Q]

TODO: write some nice prose here.

2.2.3. Function Extensionality [008T]

TODO, follows from univalence.

Definition 2.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.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.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.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.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.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.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.2.11. Torsorial Homotopy of Morphisms of Species of Types [008W]

TODO

Definition 2.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.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.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.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.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.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.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?

3. Roadmap WIP [00DS]

This note attempts to state a HoTTification of the key results from the paper Dirichlet Species and Arithmetic Zeta Functions. Some things I say here may simply be wrong because I have not proved most of what I am claiming here. This serves more as a roadmap than as a collection of results.

Definition 3.1. Species on FinSet [00DT]

A species is a function , where is the groupoid of finite sets and bijections.

Given a species we obtain a dirichlet series , classically given by

See the paper

A categorification of this is the -Dirichlet series defined for with by

See Dirichlet series of species of types in agda-unimath

It is not quite clear to me how this unifies what should happen to s and -s -> TODO.

Given a function we get a species as follows. A structure on a finite set is a way of making it into a simisimple commutative ring and picking an element of .

This is called the Hasse-Weil species

For a HoTTification see Hasse-Weil species in agda-unimath

Artin-Wedderburn Theorem

Finite semisimple commutative ring is the same as a finite product of finite fields. –> Pobably "just" isomorphism of types

The Dirichlet series of the hasse-weil species is equal to the usual hasse-weil zeta function. –> How do we say this in HoTT, in particular, how do we category the hasse-weil zeta function for a given X nicely?

generalization to stuff types –> (in n-lab entry but not paper) –> some of this is present in agda-unimath

this feels very similar to what we are doing to species in HoTT already
groupoid cardinality instead of cardinality
dirichlet series
multiplicative species generalize to multiplicative stuff types

–> allegedly these too have dirichlet series admitting euler factorizations.

4. Species on FinSet and action types [00D9]

This is an eleaboration on the notes from my call with Egbert on the XX.XX.

Definition 4.1. isFinSet [00DA]

See symmetry book definition 2.24.1

Lemma 4.2. [00DB]

isFinSet(X) is a proposition and equivalent to . See symmetry book lemma 2.24.4

Definition 4.3. Groupoid of finite sets FinSet [00DD]

We define the groupoid of finite sets as

and the groupoid of sets with cardinality by

Lemma 4.4. [00DE]

By Lemma 2.24.4 we get that

Definition 4.5. G-Set [00DI]

Given a group , a -set is a function .

Any paths in gives us a map that we call the group action of .

Observation 4.6. Loop space of FinSet_n [00DF]

The groupoid of finite sets with cardinality , is pointed connected with base point . Its loop space is the symmetric group .

In other words

Proof. TODO.

Definition 4.7. Species on FinSet [00DT]

A species is a function , where is the groupoid of finite sets and bijections.

4.8. [00DG]

Consider a species . By this and by this, restricts to

In other words, is given precisely by what is does on each , since

4.9. X([n]) is an S_n-set [00DH]

Given a path in , any type family gives a transport map

In particular for we have . So becomes an -set (see G-set) with the action

4.10. Total space is action groupoid [00DJ]

Given for a fix , the total space is by definition what we call the action type . Its objects are pairs of the form , with

See also definition 5.4.1 in the symmetry book. The action type corresponds to what we call the action groupoid or weak quotient in category theory. We will see in a second that paths in the identity type of the action type correspond precisely to the morphisms in the the action groupoid

4.11. Identity type of the total space [00DK]

As a Sigma-Type, the identity type of the total space is given by

, since (by definition), this is

So an element of the identity type is an element together with a proof that , which is exacly what we would expect from a morphism in the action groupoid.

4.12. [00DN]

Putting all of the above together we get that

In words: The total space of a species splits into components by cardinality and the n-th component is precisely the action type .

5. Dirichlet Product of Species [00DV]

5.1. FinSet is closed under cartesian Products [00DZ]

FinSet is closed under cartesian products. Proof. See Notebook I.

Notation 5.2. [00E0]

For finite sets and , we write for finte set that is the cartesian product of and as constructed here.

By abuse of notation we will sometimes just write .

Definition 5.3. cartesian decomposition [00DQ]

Given a finite set , we define the type of cartesian decompositions by

Where cartesian product in FinSet.

Definition 5.4. Dirichlet Product Species [00DP]

Given species define the dirichlet product by

where is the type of cartesian decompositions of .

5.5. Identity type of cart-dec [00DY]

Fix a finite set . There is an equivalence

Where is the induced map from the paths and .

Proof. Denote by the type family .

In the second step, we make use of the rule:

For a path denote by the induced path . then for and we get a term of type

by doing path induction on : When , we get

So it suffices to provide a term of type , which is (up to unit-path) given by reversal of paths.

5.6. Identity type of Dirichlet Product [00E4]

Let and be terms in the dirichlet product of species and .

Let be indexed by the type of cartesian decompositions, then

where is the equivalence characterizing the identity type of cart-dec.

In the second step we are using that, given some equivalence of types , we get an equivalence

In the third step we are using the follwing. Given any , we have

TODO is this true? (third step):

spell this out using path induction.
here is again the equivalence characterizing the identity type of cart-dec.
A(T,U,e) ignores e

5.7. Unit Law Dirichlet Product [00E3]

Define by

Note that is a proposition (TODO: write out why) so in particular a set.

Note also that this fits the definition of in the paper quite well.

We prove that

by constructing for each a map

and showing it has contractible fibers.

Proof. A term of type is of the form

where

Note that , so contractible. We denote its center of contraction by . We now define an equivalence

by . Because is contractible, , so is indeed an equivalence.

By univalence gives us a path

Define

Now we show that the fibers of are contracible:

Let . Then the fiber is given by

Define

where is the right unit equivalence and is the identity.

Then

Pick as the center.

We now show that given , with

holds.

Observe, that using (from ), we get that

this means we get an element

(that we also call by abuse of notation)

We now use the the characterization of the Identity type of Dirichlet Product, so we only need to give a path

Thus we need

We already have have . Define by applying univalence to . Set . Note that , which is contracible,so

It only reamains to construct . TODO

6. Dirichlet product from an action-type point of view [00DO]

Not yet sure if this is usefull in any way.

Definition 6.1. cartesian decomposition [00DQ]

Given a finite set , we define the type of cartesian decompositions by

Where cartesian product in FinSet.

Definition 6.2. Dirichlet Product Species [00DP]

Given species define the dirichlet product by

where is the type of cartesian decompositions of .

6.3. [00DR]

For and , the transported Dirichlet product is

where denotes the product of the underlying finite sets.

Aut(A) xx Aut(B) acting on F(a,A) xx G(b,B).
In the case where A = [a] and B = [b], we get an -set
given an equivalence we can view S_a xx S_b as subgroup of S_n.

the S_n acts on the dirichlet product
the stabelizer of is

Whenever I tell people about HoTT there are reocurring points of confusion. The below trees collect some explainations that I find clarify things and make them less confusing.

7. Equality and Identity types [00D1]

A distinguishing feature of MLTT is the introduction of intentional equality in addition to the strict syntactic definitional equality. This way we can use MLTT to talk about equality just like other propositions that we model using types.

The formation rule for the family of identity types states that given any two terms we may form the type of identifications between them.

The introduction rule essentially states that things that are judgementally equal should have a canonical witness of equality inhabiting the identity type. We call this witness . In order words, equality should be reflexive.

TODO

When doing mathematics using HoTT we will (almost) never talk about definitional equality between things. We can see it more as a mechanism to reduce terms.

The difference between judgemental equality and intentional equality
MLTT undespecifies the identity types
- Axiom K
Why J does not proof that every path is refl
- short answer: It would not even typechek

8. Characterization of Sigma Types and the structure identity principle [00E2]

TODO

9. Not all Types are decidable [00D4]

10. Contractible means more than connected [00D2]

Define contractible
Define connected
Equal vs merely equal
truncation kills higher paths
S^1 is not contractible
S^1 does not have distinct connected components
S^1 is connected

11. What do you mean by "Types are Spaces"? [00D5]

TODO: Look at models, specifically simplicial sets.