Smash products in HoTT

[Ali Caglayan]

*Disclaimer: Take what I say with a pinch of salt as I can and do say frivolous things occasionally*

So yesterday, Mike said that to his knowledge there was no proof of associativity of the smash product (I suppose if you define it as a pushout). I would like to collect some information about this so perhaps it can get some ideas floating around.

So in classical Algebraic Topology, the smash product is only associative when (at least two of) the spaces are compact and Hausdorff. The usual counter example is (Q∧Q)∧N not being homeomorphic to Q∧(Q∧N) where Q, N are the rationals and naturals with subspace topology. The problems come from Q not being locally compact (and therefore not compact). This example is explained in detail in May and Sigurdsson's book 'Parameterized Homotopy Theory' (Section 1.5).

Now we shouldn't have any of those problems with types, given that they are essentially CW-complexes and by Univalence we have homotopic types are equal so we should expect this to be true.

We can define the wedge sum of two (pointed or inhabited) types in HoTT as the pushout X <-- 1 --> Y. The smash product can then be defined as the pushout of  1 <-- XvY --> XxY. Where the map XvY --> XxY is the inclusion of the wedge sum into the product type. This can be defined by induction on the HIT of the pushout. Really the smash product is the correct coproduct of pointed types, the product being the same.

So this definition is pretty simple, and I think is the one that is used in the agda formalisation. I have formalise the definition in coq, using the pushouts as coequalisers, however I can't manage to use Mike's new commit which gets rid of coequalisers.

Here is some Coq code if you want to try it yourself, if you manage to prove the last statement please let me know :)

Require Import HoTT.HIT.Pushout.
Require Import HoTT.Basics.Overture.
Require Import HoTT.Pointed.
Require Import HoTT.Types.Unit.


Open Scope pointed_scope.

Definition unit_map (A : pType) : Unit -> A
  := fun _ => point A.

Definition Wedge (A B : pType) : pType.
  simple refine (Build_pType (pushout (unit_map A) (unit_map B)) _).
  refine (coeq _).
  refine (inl (point A)).
Defined.


Definition Cofiber {A B : pType} (f : A -> B) : pType.
  refine (Build_pType (pushout (fun _ => tt) f) _).
  refine (coeq _).
  refine (inr (f (point A))).
Defined.

(* Now we need to define the inclusion map i : AvB -> AxB *)

Definition wedge_prod_inc {A B : pType} : (Wedge A B) -> (A * B).
  simple refine (pushout_ind _ _ _ _ _).
  + induction a.
    refine ((a, point B)).
    refine ((point A, b)).
  + compute.
    induction a.
    induction (cp tt).
    reflexivity.
Defined.

Definition Smash (A B : pType) : pType.
  simple refine (Build_pType (@Cofiber _ _ _) _).
  refine (Wedge A B).
  refine (Build_pType (A*B) ispointed_prod).
  refine (wedge_prod_inc).
Defined.

Theorem Smash_Assoc {A B C : pType} : Smash (Smash A B) C <~> Smash A (Smash B C).
Proof.

[Floris van Doorn]

The associativity of the smash product has been proven. It has been formalized here:

https://github.com/cmu-phil/Spectral/blob/master/homotopy/smash_adjoint.hlean#L484-L485

I also think that Guillaume Brunerie has a proof and/or formalization. In the above formalization we use the adjunction between the smash product and pointed maps:

((A ∧ B) →* C) ≃ (A →* B →* C)

The hard part which is not proven is the pentagon of associativities (and some other coherences, although Guillaume has proven the hexagon, see Guillaume's thesis for the statements of these coherences).

--
You received this message because you are subscribed to the Google Groups "HoTT Cafe" group.
To unsubscribe from this group and stop receiving emails from it, send an email to hott-cafe+...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Ali Caglayan]

So I gather that this means associativity and pMap adjunctions have actually been proven. What hasn't been proven is that pointed types form a monoidal category with smash product?

[Floris van Doorn]

Yes, that is correct. Although you have to be careful with the term "monoidal category". Pointed types do not form a monoidal 1-category, and we don't know how to state internally that it forms a monoidal (\infty,1)-category, but we can state the first few levels of coherences.

[Michael Shulman]

My memory is that the adjunction is a little subtle, right? You've
shown that there is a smash/pMap adjunction, but not that that
adjunction is itself enriched over pointed types; the latter would
imply, by the Eilenberg-Kelly closed-categories argument, that the
pentagon holds.

Regarding terminology, couldn't one just 0-truncate the hom-types to
obtain a monoidal 1-category of pointed types?