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

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

        TODO: write some nice prose here.

        3. Function Extensionality [008T]

          TODO, follows from univalence.

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

              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.

                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

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

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

                          TODO

                          Definition 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 13. Cauchy Product of Species of Types [008Y]

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

                              Remark 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 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 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 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 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?