diff --git a/src/species/composition-cauchy-series-species-of-types.lagda.md b/src/species/composition-cauchy-series-species-of-types.lagda.md index e9a9d3e04f..2daa753e6a 100644 --- a/src/species/composition-cauchy-series-species-of-types.lagda.md +++ b/src/species/composition-cauchy-series-species-of-types.lagda.md @@ -88,8 +88,8 @@ module _ ( λ V → ( equiv-prod ( id-equiv) - ( inv-equiv equiv-up-product ∘e - equiv-prod id-equiv equiv-ev-pair)) ∘e + ( ( inv-equiv equiv-up-product) ∘e + ( equiv-prod id-equiv equiv-ev-pair))) ∘e ( left-unit-law-Σ-is-contr ( is-torsorial-equiv' (Σ U V)) ( Σ U V , id-equiv))))))) ∘e