Equivalences of Polynomial Functors

This file defines equivalences between polynomial functors and proves basic properties about them.

An equivalence between two polynomial functors P and Q, written P ≃ₚ Q, is given by an equivalence of the A types and an equivalence between the B types for each a : A.

We provide various canonical equivalences for operations on polynomial functors, such as:

• Sum operations: P + 0 ≃ₚ P, 0 + P ≃ₚ P
• Product operations and their properties
• Equivalences for sigma and pi constructions
• Universe lifting equivalences
• Tensor product equivalences
• Composition equivalences

Main definitions

• PFunctor.Equiv: An equivalence between two polynomial functors
• ≃ₚ: Notation for polynomial functor equivalences

Main results

• Basic equivalence properties: reflexivity, symmetry, transitivity
• Canonical equivalences for sum, product, and other constructions on polynomial functors

instance instIsEmptySigma {α : Sort u} {β : α → Sort v} [inst : IsEmpty α] : IsEmpty ((a : α) ×' β a)

def PFunctor.Equiv.sumZero (P : PFunctor.{uA₁, uB}) : (P + 0).Equiv P

Addition with the zero functor on the left is equivalent to the original functor

@[simp]

theorem PFunctor.Equiv.sumZero_equivB (P : PFunctor.{uA₁, uB}) (x✝ : (P + 0).A) : (sumZero P).equivB x✝ = Sum.casesOn x✝ (fun (x : P.A) => _root_.Equiv.refl ((P + 0).B (Sum.inl x))) fun (a : A 0) => PEmpty.elim a

@[simp]

theorem PFunctor.Equiv.sumZero_equivA (P : PFunctor.{uA₁, uB}) : (sumZero P).equivA = Equiv.sumEmpty P.A PEmpty.{uA₁ + 1}

def PFunctor.Equiv.zeroSum (P : PFunctor.{uA₁, uB}) : (0 + P).Equiv P

Addition with the zero functor on the right is equivalent to the original functor

@[simp]

theorem PFunctor.Equiv.zeroSum_equivA (P : PFunctor.{uA₁, uB}) : (zeroSum P).equivA = Equiv.emptySum PEmpty.{uA₁ + 1} P.A

@[simp]

theorem PFunctor.Equiv.zeroSum_equivB (P : PFunctor.{uA₁, uB}) (x✝ : (0 + P).A) : (zeroSum P).equivB x✝ = Sum.casesOn x✝ (fun (a : A 0) => PEmpty.elim a) fun (x : P.A) => _root_.Equiv.refl ((0 + P).B (Sum.inr x))

def PFunctor.Equiv.sumComm (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) : (P + Q).Equiv (Q + P)

Sum of polynomial functors is commutative up to equivalence

@[simp]

theorem PFunctor.Equiv.sumComm_equivA (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) : (sumComm P Q).equivA = _root_.Equiv.sumComm P.A Q.A

@[simp]

theorem PFunctor.Equiv.sumComm_equivB (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) (x✝ : (P + Q).A) : (sumComm P Q).equivB x✝ = Sum.casesOn x✝ (fun (x : P.A) => _root_.Equiv.refl ((P + Q).B (Sum.inl x))) fun (x : Q.A) => _root_.Equiv.refl ((P + Q).B (Sum.inr x))

def PFunctor.Equiv.sumAssoc (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) (R : PFunctor.{uA₃, uB}) : (P + Q + R).Equiv (P + (Q + R))

Sum of polynomial functors is associative up to equivalence

@[simp]

theorem PFunctor.Equiv.sumAssoc_equivB (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) (R : PFunctor.{uA₃, uB}) (x✝ : (P + Q + R).A) : (sumAssoc P Q R).equivB x✝ = Sum.casesOn x✝ (fun (x : (P + Q).A) => Sum.casesOn x (fun (x : P.A) => _root_.Equiv.refl ((P + Q + R).B (Sum.inl (Sum.inl x)))) fun (x : Q.A) => _root_.Equiv.refl ((P + Q + R).B (Sum.inl (Sum.inr x)))) fun (x : R.A) => _root_.Equiv.refl ((P + Q + R).B (Sum.inr x))

@[simp]

theorem PFunctor.Equiv.sumAssoc_equivA (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) (R : PFunctor.{uA₃, uB}) : (sumAssoc P Q R).equivA = _root_.Equiv.sumAssoc P.A Q.A R.A

def PFunctor.Equiv.sumCongr {P Q : PFunctor.{u_1, u_2}} {R : PFunctor.{uA₃, uB₁}} {S : PFunctor.{uA₄, uB₁}} (e₁ : P.Equiv R) (e₂ : Q.Equiv S) : (P + Q).Equiv (R + S)

If P ≃ₚ R and Q ≃ₚ S, then P + Q ≃ₚ R + S

@[simp]

theorem PFunctor.Equiv.sumCongr_equivB {P Q : PFunctor.{u_1, u_2}} {R : PFunctor.{uA₃, uB₁}} {S : PFunctor.{uA₄, uB₁}} (e₁ : P.Equiv R) (e₂ : Q.Equiv S) (x✝ : (P + Q).A) : (e₁.sumCongr e₂).equivB x✝ = Sum.casesOn x✝ (fun (x : P.A) => e₁.equivB x) fun (x : Q.A) => e₂.equivB x

@[simp]

theorem PFunctor.Equiv.sumCongr_equivA {P Q : PFunctor.{u_1, u_2}} {R : PFunctor.{uA₃, uB₁}} {S : PFunctor.{uA₄, uB₁}} (e₁ : P.Equiv R) (e₂ : Q.Equiv S) : (e₁.sumCongr e₂).equivA = e₁.equivA.sumCongr e₂.equivA

def PFunctor.Equiv.sumSumSumComm (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) (R : PFunctor.{uA₃, uB}) (S : PFunctor.{uA₄, uB}) : (P + Q + (R + S)).Equiv (P + R + (Q + S))

Rearrangement of nested sums: (P + Q) + (R + S) ≃ₚ (P + R) + (Q + S)

def PFunctor.Equiv.prodZero (P : PFunctor.{uA₁, uB₁}) : (P * 0).Equiv 0

Product with 0 on the right is 0

def PFunctor.Equiv.zeroProd (P : PFunctor.{uA₁, uB₁}) : (0 * P).Equiv 0

Product with 0 on the left is 0

def PFunctor.Equiv.prodOne (P : PFunctor.{uA₁, uB₁}) : (P * 1).Equiv P

Product with the unit functor on the right is equivalent to the original functor

@[simp]

theorem PFunctor.Equiv.prodOne_equivA (P : PFunctor.{uA₁, uB₁}) : (prodOne P).equivA = Equiv.prodPUnit P.A

@[simp]

theorem PFunctor.Equiv.prodOne_equivB (P : PFunctor.{uA₁, uB₁}) (a : (P * 1).A) : (prodOne P).equivB a = Equiv.sumEmpty (P.B a.1) PEmpty.{uB₁ + 1}

def PFunctor.Equiv.oneProd (P : PFunctor.{uA₁, uB₁}) : (1 * P).Equiv P

Product with the unit functor on the left is equivalent to the original functor

@[simp]

theorem PFunctor.Equiv.oneProd_equivA (P : PFunctor.{uA₁, uB₁}) : (oneProd P).equivA = Equiv.punitProd P.A

@[simp]

theorem PFunctor.Equiv.oneProd_equivB (P : PFunctor.{uA₁, uB₁}) (a : (1 * P).A) : (oneProd P).equivB a = Equiv.emptySum PEmpty.{uB₁ + 1} (P.B a.2)

def PFunctor.Equiv.prodComm (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) : (P * Q).Equiv (Q * P)

Product of polynomial functors is commutative up to equivalence

@[simp]

theorem PFunctor.Equiv.prodComm_equivB (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) (a : (P * Q).A) : (prodComm P Q).equivB a = _root_.Equiv.sumComm (P.B a.1) (Q.B a.2)

@[simp]

theorem PFunctor.Equiv.prodComm_equivA (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) : (prodComm P Q).equivA = _root_.Equiv.prodComm P.A Q.A

def PFunctor.Equiv.prodAssoc (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) (R : PFunctor.{uA₃, uB₃}) : (P * Q * R).Equiv (P * (Q * R))

Product of polynomial functors is associative up to equivalence

@[simp]

theorem PFunctor.Equiv.prodAssoc_equivB (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) (R : PFunctor.{uA₃, uB₃}) (a : (P * Q * R).A) : (prodAssoc P Q R).equivB a = _root_.Equiv.sumAssoc (P.B a.1.1) (Q.B a.1.2) (R.B a.2)

@[simp]

theorem PFunctor.Equiv.prodAssoc_equivA (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) (R : PFunctor.{uA₃, uB₃}) : (prodAssoc P Q R).equivA = _root_.Equiv.prodAssoc P.A Q.A R.A

def PFunctor.Equiv.prodCongr {P Q : PFunctor.{u_1, u_2}} {R : PFunctor.{uA₃, uB₃}} {S : PFunctor.{uA₄, uB₄}} (e₁ : P.Equiv R) (e₂ : Q.Equiv S) : (P * Q).Equiv (R * S)

Equivalence is preserved under product: if P ≃ₚ R and Q ≃ₚ S, then P * Q ≃ₚ R * S

@[simp]

theorem PFunctor.Equiv.prodCongr_equivA {P Q : PFunctor.{u_1, u_2}} {R : PFunctor.{uA₃, uB₃}} {S : PFunctor.{uA₄, uB₄}} (e₁ : P.Equiv R) (e₂ : Q.Equiv S) : (e₁.prodCongr e₂).equivA = e₁.equivA.prodCongr e₂.equivA

@[simp]

theorem PFunctor.Equiv.prodCongr_equivB {P Q : PFunctor.{u_1, u_2}} {R : PFunctor.{uA₃, uB₃}} {S : PFunctor.{uA₄, uB₄}} (e₁ : P.Equiv R) (e₂ : Q.Equiv S) (a : (P * Q).A) : (e₁.prodCongr e₂).equivB a = (e₁.equivB a.1).sumCongr (e₂.equivB a.2)

def PFunctor.Equiv.prodProdProdComm (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) (R : PFunctor.{uA₃, uB₃}) (S : PFunctor.{uA₄, uB₄}) : (P * Q * (R * S)).Equiv (P * R * (Q * S))

Rearrangement of nested products: (P * Q) * (R * S) ≃ₚ (P * R) * (Q * S)

@[simp]

theorem PFunctor.Equiv.prodProdProdComm_equivA (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) (R : PFunctor.{uA₃, uB₃}) (S : PFunctor.{uA₄, uB₄}) : (prodProdProdComm P Q R S).equivA = _root_.Equiv.prodProdProdComm P.A Q.A R.A S.A

@[simp]

theorem PFunctor.Equiv.prodProdProdComm_equivB (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) (R : PFunctor.{uA₃, uB₃}) (S : PFunctor.{uA₄, uB₄}) (a : (P * Q * (R * S)).A) : (prodProdProdComm P Q R S).equivB a = _root_.Equiv.sumSumSumComm (P.B a.1.1) (Q.B a.1.2) (R.B a.2.1) (S.B a.2.2)

def PFunctor.Equiv.sumProdDistrib (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₁}) (R : PFunctor.{uA₃, uB₂}) : ((P + Q) * R).Equiv (P * R + Q * R)

Sum distributes over product: (P + Q) * R ≃ₚ (P * R) + (Q * R)

def PFunctor.Equiv.prodSumDistrib (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) (R : PFunctor.{uA₃, uB₂}) : (P * (Q + R)).Equiv (P * Q + P * R)

Product distributes over sum: P * (Q + R) ≃ₚ (P * Q) + (P * R)

TODO: define in terms of sumProdDistrib

@[simp]

theorem PFunctor.Equiv.prodSumDistrib_equivB (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) (R : PFunctor.{uA₃, uB₂}) (x✝ : (P * (Q + R)).A) : (prodSumDistrib P Q R).equivB x✝ = match x✝ with | (fst, a) => Sum.casesOn a (fun (x : Q.A) => _root_.Equiv.refl ((P * (Q + R)).B (fst, Sum.inl x))) fun (x : R.A) => _root_.Equiv.refl ((P * (Q + R)).B (fst, Sum.inr x))

@[simp]

theorem PFunctor.Equiv.prodSumDistrib_equivA (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) (R : PFunctor.{uA₃, uB₂}) : (prodSumDistrib P Q R).equivA = _root_.Equiv.prodSumDistrib P.A Q.A R.A

instance PFunctor.Equiv.instIsEmptyASigma {I : Type v} (F : I → PFunctor.{uA₂, uB₂}) [inst : IsEmpty I] : IsEmpty (sigma F).A

def PFunctor.Equiv.emptySigma {I : Type v} (F : I → PFunctor.{uA₂, uB₂}) [inst : IsEmpty I] : (sigma F).Equiv 0

Sigma of an empty family is the zero functor.

def PFunctor.Equiv.uniqueSigma {I : Type v} (F : I → PFunctor.{uA₂, uB₂}) [Unique I] : (sigma F).Equiv (F default)

def PFunctor.Equiv.punitSigma {F : PUnit.{u_1 + 1} → PFunctor.{uA, uB}} : (sigma F).Equiv (F PUnit.unit)

Sigma of a PUnit-indexed family is equivalent to the functor itself.

def PFunctor.Equiv.sumSigmaDistrib (P : PFunctor.{uA₁, uB₁}) {I : Type v} (F : I → PFunctor.{uA₂, uB₁}) [Unique I] : (P + sigma F).Equiv (sigma fun (i : I) => P + F i)

Left distributivity of sum over sigma.

def PFunctor.Equiv.sigmaSumDistrib (P : PFunctor.{uA₁, uB₁}) {I : Type v} (F : I → PFunctor.{uA₂, uB₁}) [Unique I] : (sigma F + P).Equiv (sigma fun (i : I) => F i + P)

Right distributivity of sum over sigma.

def PFunctor.Equiv.prodSigmaDistrib (P : PFunctor.{uA₁, uB₁}) {I : Type v} (F : I → PFunctor.{uA₂, uB₂}) : (P * sigma F).Equiv (sigma fun (i : I) => P * F i)

Left distributivity of product over sigma.

def PFunctor.Equiv.sigmaProdDistrib (P : PFunctor.{uA₁, uB₁}) {I : Type v} (F : I → PFunctor.{uA₂, uB₂}) : (sigma F * P).Equiv (sigma fun (i : I) => F i * P)

Right distributivity of product over sigma.

def PFunctor.Equiv.tensorSigmaDistrib (P : PFunctor.{uA₁, uB₁}) {I : Type v} (F : I → PFunctor.{uA₂, uB₂}) : (P.tensor (sigma F)).Equiv (sigma fun (i : I) => P.tensor (F i))

Left distributivity of tensor product over sigma.

def PFunctor.Equiv.sigmaTensorDistrib {I : Type v} (F : I → PFunctor.{uA₁, uB₁}) (P : PFunctor.{uA₂, uB₂}) : ((sigma F).tensor P).Equiv (sigma fun (i : I) => (F i).tensor P)

Right distributivity of tensor product over sigma.

def PFunctor.Equiv.sigmaCompDistrib {I : Type v} (F : I → PFunctor.{uA₁, uB₁}) (P : PFunctor.{uA₂, uB₂}) : ((sigma F).comp P).Equiv (sigma fun (i : I) => (F i).comp P)

Right distributivity of composition over sigma.

def PFunctor.Equiv.piPUnit (P : PFunctor.{uA, uB}) : (pi fun (x : PUnit.{u_1 + 1}) => P).Equiv P

Pi over a PUnit-indexed family is equivalent to the functor itself.

def PFunctor.Equiv.uliftEquiv (P : PFunctor.{uA₁, uB₁}) : P.Equiv P.ulift

Equivalence between a polynomial functor and its universe-lifted version

def PFunctor.Equiv.uliftUliftEquiv (P : PFunctor.{uA₁, uB₁}) : P.ulift.ulift.Equiv P.ulift

Universe lifting is idempotent up to equivalence

def PFunctor.Equiv.uliftSumEquiv (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₁}) : (P + Q).ulift.Equiv (P.ulift + Q.ulift)

Universe lifting commutes with sum

def PFunctor.Equiv.uliftProdEquiv (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) : (P * Q).ulift.Equiv (P.ulift * Q.ulift)

Universe lifting commutes with product.

def PFunctor.Equiv.tensorZero (P : PFunctor.{uA₁, uB₁}) : (P.tensor 0).Equiv 0

Tensor product with 0 on the right is 0

def PFunctor.Equiv.zeroTensor (P : PFunctor.{uA₁, uB₁}) : (tensor 0 P).Equiv 0

Tensor product with 0 on the left is 0

instance PFunctor.Equiv.instIsEmptyBTensorOfNat {P : PFunctor.{u_1, u_2}} {a : (P.tensor 1).A} : IsEmpty ((P.tensor 1).B a)

def PFunctor.Equiv.tensorOne (P : PFunctor.{uA₁, uB₁}) : (P.tensor 1).Equiv (C P.A)

Tensor product with 1 on the right is equivalent to the constant functor

instance PFunctor.Equiv.instIsEmptyBTensorOfNat_1 {P : PFunctor.{u_1, u_2}} {a : (tensor 1 P).A} : IsEmpty ((tensor 1 P).B a)

def PFunctor.Equiv.oneTensor (P : PFunctor.{uA₁, uB₁}) : (tensor 1 P).Equiv (C P.A)

Tensor product with 1 on the left is equivalent to the constant functor

def PFunctor.Equiv.tensorX (P : PFunctor.{uA₁, uB₁}) : (P.tensor X).Equiv P

Tensor product with the functor Y on the right

@[simp]

theorem PFunctor.Equiv.tensorX_equivB (P : PFunctor.{uA₁, uB₁}) (a : (P.tensor X).A) : (tensorX P).equivB a = Equiv.prodPUnit (P.B a.1)

@[simp]

theorem PFunctor.Equiv.tensorX_equivA (P : PFunctor.{uA₁, uB₁}) : (tensorX P).equivA = Equiv.prodPUnit P.A

def PFunctor.Equiv.xTensor (P : PFunctor.{uA₁, uB₁}) : (X.tensor P).Equiv P

Tensor product with the functor Y on the left

@[simp]

theorem PFunctor.Equiv.xTensor_equivA (P : PFunctor.{uA₁, uB₁}) : (xTensor P).equivA = Equiv.punitProd P.A

@[simp]

theorem PFunctor.Equiv.xTensor_equivB (P : PFunctor.{uA₁, uB₁}) (a : (X.tensor P).A) : (xTensor P).equivB a = Equiv.punitProd (P.B a.2)

def PFunctor.Equiv.tensorComm (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) : (P.tensor Q).Equiv (Q.tensor P)

Tensor product of polynomial functors is commutative up to equivalence

@[simp]

theorem PFunctor.Equiv.tensorComm_equivA (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) : (tensorComm P Q).equivA = _root_.Equiv.prodComm P.A Q.A

@[simp]

theorem PFunctor.Equiv.tensorComm_equivB (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) (a : (P.tensor Q).A) : (tensorComm P Q).equivB a = _root_.Equiv.prodComm (P.B a.1) (Q.B a.2)

def PFunctor.Equiv.tensorAssoc (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) (R : PFunctor.{uA₃, uB₃}) : ((P.tensor Q).tensor R).Equiv (P.tensor (Q.tensor R))

Tensor product of polynomial functors is associative up to equivalence

@[simp]

theorem PFunctor.Equiv.tensorAssoc_equivA (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) (R : PFunctor.{uA₃, uB₃}) : (tensorAssoc P Q R).equivA = _root_.Equiv.prodAssoc P.A Q.A R.A

@[simp]

theorem PFunctor.Equiv.tensorAssoc_equivB (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) (R : PFunctor.{uA₃, uB₃}) (a : ((P.tensor Q).tensor R).A) : (tensorAssoc P Q R).equivB a = _root_.Equiv.prodAssoc (P.B a.1.1) (Q.B a.1.2) (R.B a.2)

def PFunctor.Equiv.tensorCongr {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} {S : PFunctor.{uA₄, uB₄}} (e₁ : P.Equiv R) (e₂ : Q.Equiv S) : (P.tensor Q).Equiv (R.tensor S)

Tensor product preserves equivalences: if P ≃ₚ R and Q ≃ₚ S, then P ⊗ Q ≃ₚ R ⊗ S

@[simp]

theorem PFunctor.Equiv.tensorCongr_equivA {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} {S : PFunctor.{uA₄, uB₄}} (e₁ : P.Equiv R) (e₂ : Q.Equiv S) : (e₁.tensorCongr e₂).equivA = e₁.equivA.prodCongr e₂.equivA

@[simp]

theorem PFunctor.Equiv.tensorCongr_equivB {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} {S : PFunctor.{uA₄, uB₄}} (e₁ : P.Equiv R) (e₂ : Q.Equiv S) (a : (P.tensor Q).A) : (e₁.tensorCongr e₂).equivB a = (e₁.equivB a.1).prodCongr (e₂.equivB a.2)

def PFunctor.Equiv.tensorTensorTensorComm (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) (R : PFunctor.{uA₃, uB₃}) (S : PFunctor.{uA₄, uB₄}) : ((P.tensor Q).tensor (R.tensor S)).Equiv ((P.tensor R).tensor (Q.tensor S))

Rearrangement of nested tensor products: (P ⊗ Q) ⊗ (R ⊗ S) ≃ₚ (P ⊗ R) ⊗ (Q ⊗ S)

def PFunctor.Equiv.sumTensorDistrib (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₁}) (R : PFunctor.{uA₃, uB₂}) : ((P + Q).tensor R).Equiv (P.tensor R + Q.tensor R)

Sum distributes over tensor product: (P + Q) ⊗ R ≃ₚ (P ⊗ R) + (Q ⊗ R)

def PFunctor.Equiv.tensorSumDistrib (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) (R : PFunctor.{uA₃, uB₂}) : (P.tensor (Q + R)).Equiv (P.tensor Q + P.tensor R)

Tensor product distributes over sum: P ⊗ (Q + R) ≃ₚ (P ⊗ Q) + (P ⊗ R)

instance PFunctor.Equiv.instIsEmptyACompOfNat (P : PFunctor.{uA₁, uB₁}) : IsEmpty (comp 0 P).A

def PFunctor.Equiv.zeroComp (P : PFunctor.{uA₁, uB₁}) : (comp 0 P).Equiv 0

instance PFunctor.Equiv.instIsEmptyBCompOfNat (P : PFunctor.{uA₁, uB₁}) {a : (comp 1 P).A} : IsEmpty ((comp 1 P).B a)

def PFunctor.Equiv.oneComp (P : PFunctor.{uA₁, uB₁}) : (comp 1 P).Equiv 1

def PFunctor.Equiv.compAssoc (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) (R : PFunctor.{uA₃, uB₃}) : ((P.comp Q).comp R).Equiv (P.comp (Q.comp R))

Associativity of composition

def PFunctor.Equiv.compX (P : PFunctor.{uA₁, uB₁}) : (P.comp X).Equiv P

Composition with X is identity (right)

def PFunctor.Equiv.XComp (P : PFunctor.{uA₁, uB₁}) : (X.comp P).Equiv P

Composition with X is identity (left)

def PFunctor.Equiv.sumCompDistrib (P : PFunctor.{uA₁, uB₁}) (R : PFunctor.{uA₃, uB₃}) (Q : PFunctor.{uA₂, uB₁}) : ((P + Q).comp R).Equiv (P.comp R + Q.comp R)

Distributivity of composition over sum on the right

def PFunctor.Equiv.prodCompDistrib (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) (R : PFunctor.{uA₃, uB₃}) : ((P * Q).comp R).Equiv (P.comp R * Q.comp R)

Composition distributes over product on the left.