diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-10-11 22:59:21 -0700 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-10-11 22:59:21 -0700 |
| commit | 7cb4f160835178d06e0c0bf9802c3cad6d48a9d0 (patch) | |
| tree | 824730560ce0c3d1b08267a6b46da9daf23384c1 /Data/WiringDiagram | |
| parent | 4e6acbf8b8084bea12327683aceb300a9b64c367 (diff) | |
Add hom-set addition to semiadditive recordmain
Diffstat (limited to 'Data/WiringDiagram')
| -rw-r--r-- | Data/WiringDiagram/Equalities.agda | 8 |
1 files changed, 5 insertions, 3 deletions
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 ∎ |