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. Overview [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.

Definition 3.2. Dirichlet Type of Species [00EY]

Given a species define the dirichlet type of by

Definition 3.3. Groupoid Cardinality of 1-types [00ER]

Let be a 1-type such that is finite, and for all is finite. Define the groupoid cardinality of as the rational number

where denotes a finite sum over rational numbers indexed by the finite set .

3.4. Dirichlet Series [00F1]

For a dirichlet species define

where is the dirichlet type of , and is the groupoid cardinality of the n-th component of the dirichlet type. We call the dirichlet series of , and the -th summand.

Definition 3.5. Dirichlet Product Species [00DP]

Given species define the dirichlet product by

where is the type of cartesian decompositions of .

TODO 3.6. Dirichlet series of dirichlet product of species is dirchlet product of dirichlet series [00FA]

i.e

clearly

To continue here we must first make progress on the groupoid cardinality of the dirichlet product of F and G, for that look at group action of on cartesian decompositions

TODO 3.7. Definition Dirichlet Power [00FE]

TODO

TODO 3.8. Definition Dirichlet exponential [00FG]

Definition 3.9. Euler Product of Species [00FI]

For type family of species indexed by with a p-local dirichlet species.

TODO 3.10. [00FJ]

3.11. Zeta Species [00EC]

Given , define

where is the underlying type of . See also Hasse-Weil species in agda-unimath

3.12. [00FP]

TODO 3.13. [00FQ]

3.14. [00FR]

Define an -structure on a finite set to be a way of making that set into a field of characteristic and then choose an element of .

TODO 3.15. [00FS]

TODO 3.16. Main Theorem [00EF]

The zeta species and the eulerproduct on the right hand side are isomorphic as types.

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

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. Groupoid Cardinality of Types [00EN]

5.1. Notation [00EO]

For a type write for .

5.2. Notation [00EP]

For a -type and write for the set .

5.3. Notation [00EQ]

Given a 1-type , denote by the set cardinality of the set of automorphisms. The universal property of the set truncation gives a unique map from to , that is compatible with the Automorphism-Cardinality. By abuse of notation we also denote this map by .

5.4. Rational Numbers [00ES]

We assume some construction of type of rational numbers. We assume that this type is a set with decidable equality, equipped with the usual addition and multiplication making it a field. We denote the field of rational numbers with . For a sketched construction see the HoTT book, section 11., section 11.1.

TODO: Make very clear what for what properties we need witnesses and find a construction we can borrow.

Definition 5.5. Groupoid Cardinality of 1-types [00ER]

Let be a 1-type such that is finite, and for all is finite. Define the groupoid cardinality of as the rational number

where denotes a finite sum over rational numbers indexed by the finite set .

Observation 5.6. Groupoid Cardinality is compatible with set cardinality [00EX]

TODO

Lemma 5.7. Groupoid Cardinality is additive [00EU]

TODO

Lemma 5.8. Groupoid Cardinality is multiplicative [00EV]

TODO

Lemma 5.9. Groupoid cardinality of BG [00EW]

6. Dirichlet Series of Species [00EA]

Definition 6.1. Dirichlet Type of Species [00EY]

Given a species define the dirichlet type of by

TODO 6.2. Identity Type of Dirichlet Type [00F6]

Idea 6.3. Generating Type of Species [00F8]

We can categorify the generating functions very similarly:

Notation 6.4. [00F0]

TODO 6.5. [00F4]

TODO 6.6. [00F5]

Definition 6.7. tame Species [00F2]

TODO

Definition 6.8. Dirichlet Species [00F3]

TODO

6.9. Dirichlet Series [00F1]

For a dirichlet species define

where is the dirichlet type of , and is the groupoid cardinality of the n-th component of the dirichlet type. We call the dirichlet series of , and the -th summand.

TODO 6.10. [00F9]

Compare classical definition.

Definition 6.11. Dirichlet Product of functions [00FB]

We can model the formal product of two dirichlet series by defining a dirichlet product for functions from into a ring, say .

For , define

7. Dirichlet Product of Species [00DV]

7.1. FinSet is closed under cartesian products [00DZ]

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

Notation 7.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 7.3. cartesian decomposition [00DQ]

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

Where cartesian product in FinSet.

hello world

Lemma 7.4. Identity type of cartesian decompositions [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.

Lemma 7.5. Identity type of cartesian decomposition with FTIT [00EL]

see folder.

Definition 7.6. Dirichlet Product Species [00DP]

Given species define the dirichlet product by

where is the type of cartesian decompositions of .

Lemma 7.7. 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

Proof.

Given , define . We then have that

We make use of the following charcterization of the idenity type of cartesian decompositions constructed here, and denote it by .

With that the equivalence becomes

Here we are using that, given some equivalence of types , we get an equivalence .

Now since is constant in we have by this lemma, that

We conclude that

Lemma 7.8. Identity type of dirichlet product with FTIT [00EJ]

We present an alternative proof of the characterization of the identity type of the dirichlet product using the fundamental theorem of identity types.

Let and be terms in the dirichlet product of species and . Then there is an equivalence

Proof. See folder.

Lemma 7.9. Unit Law Dirichlet Product [00E3]

Define by

Note that is a proposition (TODO: explain) 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: copy from Notebook II)

Lemma 7.10. Commutativity Dirichlet Product [00E8]

Given species on FinSet and we have that

Proof. TODO: just rearranging things

Lemma 7.11. Associativity Dirichlet Product [00E9]

Proof. TODO

TODO 7.12. The dirichlet product gives a symmetric monoidal structure on Species [00EI]

TODO: Look into the definition of symmetric monoidal, figure out what else there is to show here (i.e coherence stuff). Conclude.

TODO 7.13. [00FC]

TODO 7.14. Dirichlet series of dirichlet product of species is dirchlet product of dirichlet series [00FA]

i.e

clearly

To continue here we must first make progress on the groupoid cardinality of the dirichlet product of F and G, for that look at group action of on cartesian decompositions

8. Cartesian Decomposition of fixed shape [00E5]

Recall the definition of the cartesian decomposition

Definition 8.1. cartesian decomposition [00DQ]

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

Where cartesian product in FinSet.

hello world

Definition 8.2. cartesian decomposition of fixed shape [00E7]

Define

We can view the as

write for .

Now the acts on by

Transitivity (there is only one orbit)

Consider two decompositions

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

Not yet sure if this is usefull in any way.

Definition 9.1. cartesian decomposition [00DQ]

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

Where cartesian product in FinSet.

hello world

Definition 9.2. Dirichlet Product Species [00DP]

Given species define the dirichlet product by

where is the type of cartesian decompositions of .

9.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

10. Euler Product of Species [00FD]

TODO 10.1. Definition Dirichlet Power [00FE]

TODO

10.2. S_n acts on dirichlet power [00FF]

TODO

TODO 10.3. Definition Dirichlet exponential [00FG]

TODO 10.4. [00FH]

Definition 10.5. Euler Product of Species [00FI]

For type family of species indexed by with a p-local dirichlet species.

TODO 10.6. [00FJ]

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.

11. 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

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

TODO

13. Not all Types are decidable [00D4]

14. 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

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

TODO: Look at models, specifically simplicial sets.