From 7cb4f160835178d06e0c0bf9802c3cad6d48a9d0 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Sun, 11 Oct 2026 22:59:21 -0700 Subject: Add hom-set addition to semiadditive record --- Data/WiringDiagram/Equalities.agda | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'Data/WiringDiagram/Equalities.agda') diff --git a/Data/WiringDiagram/Equalities.agda b/Data/WiringDiagram/Equalities.agda index 1c3928e..a932c61 100644 --- a/Data/WiringDiagram/Equalities.agda +++ b/Data/WiringDiagram/Equalities.agda @@ -57,9 +57,9 @@ loop∘push∘loop≈merge f id≤f†∘f = ≈ᵢ ⌸ (identityˡ ○ identity ∇ ∘ id ×₁ ∇ ∘ ⟨ π₁ , (f † ∘ f) ×₁ (f †) ⟩ ≈⟨ refl⟩∘⟨ pushʳ (sym assocˡ∘⟨⟩) ⟩ ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ ⟨ ⟨ π₁ , (f † ∘ f) ∘ π₁ ⟩ , f † ∘ π₂ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-congʳ (⟨⟩-congʳ identityˡ) ⟨ ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ ⟨ ⟨ id ∘ π₁ , (f † ∘ f) ∘ π₁ ⟩ , f † ∘ π₂ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-congʳ ⟨⟩∘ ⟨ - ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ ⟨ id , f † ∘ f ⟩ ×₁ (f †) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ×₁-congʳ ×₁∘Δ ⟨ - ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ (id ×₁ (f † ∘ f) ∘ Δ) ×₁ (f †) ≈⟨ extendʳ ∇-assoc-×₁ ⟨ - ∇ ∘ (∇ ×₁ id) ∘ (id ×₁ (f † ∘ f) ∘ Δ) ×₁ (f †) ≈⟨ refl⟩∘⟨ first∘×₁ ⟩ + ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ ⟨ id , f † ∘ f ⟩ ×₁ (f †) ≈⟨ extendʳ ∇-assoc-×₁ ⟨ + ∇ ∘ (∇ ×₁ id) ∘ ⟨ id , f † ∘ f ⟩ ×₁ (f †) ≈⟨ refl⟩∘⟨ first∘×₁ ⟩ + ∇ ∘ (∇ ∘ ⟨ id , f † ∘ f ⟩) ×₁ (f †) ≈⟨ refl⟩∘⟨ ×₁-congʳ +-∇∘⟨⟩ ⟨ ∇ ∘ (id + (f † ∘ f)) ×₁ (f †) ≈⟨ refl⟩∘⟨ ×₁-congʳ id≤f†∘f ⟩ ∇ ∘ (f † ∘ f) ×₁ (f †) ≈⟨ refl⟩∘⟨ ×₁∘first ⟨ ∇ ∘ (f †) ×₁ (f †) ∘ f ×₁ id ≈⟨ extendʳ ⇒∇-×₁ ⟨ @@ -93,6 +93,8 @@ loop∘pull∘loop≈split f f∘f†≤id = ≈ᵢ ⌸ (identityˡ ○ identity ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ (id ×₁ (f ∘ f †)) ×₁ f ∘ Δ ×₁ id ≈⟨ extendʳ ∇-assoc-×₁ ⟨ ∇ ∘ ∇ ×₁ id ∘ (id ×₁ (f ∘ f †)) ×₁ f ∘ Δ ×₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ×₁∘first ⟩ ∇ ∘ ∇ ×₁ id ∘ (id ×₁ (f ∘ f †) ∘ Δ) ×₁ f ≈⟨ refl⟩∘⟨ first∘×₁ ⟩ + ∇ ∘ (∇ ∘ id ×₁ (f ∘ f †) ∘ Δ) ×₁ f ≈⟨ refl⟩∘⟨ ×₁-congʳ (refl⟩∘⟨ ×₁∘Δ) ⟩ + ∇ ∘ (∇ ∘ ⟨ id , f ∘ f † ⟩) ×₁ f ≈⟨ refl⟩∘⟨ ×₁-congʳ +-∇∘⟨⟩ ⟨ ∇ ∘ (id + (f ∘ f †)) ×₁ f ≈⟨ refl⟩∘⟨ ×₁-congʳ (+-comm id (f ∘ f †)) ⟩ ∇ ∘ ((f ∘ f †) + id) ×₁ f ≈⟨ refl⟩∘⟨ ×₁-congʳ f∘f†≤id ⟩ ∇ ∘ id ×₁ f ∎ -- cgit v1.2.3