diff options
Diffstat (limited to 'Category/Dagger')
| -rw-r--r-- | Category/Dagger/Semiadditive.agda | 37 |
1 files changed, 20 insertions, 17 deletions
diff --git a/Category/Dagger/Semiadditive.agda b/Category/Dagger/Semiadditive.agda index 41be19e..8c46e14 100644 --- a/Category/Dagger/Semiadditive.agda +++ b/Category/Dagger/Semiadditive.agda @@ -106,10 +106,14 @@ record SemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where +-† : {A B : Obj} {f g : A ⇒ B} → (f + g) † ≈ (f †) + (g †) +-† {f = f} {g} = begin - (∇ ∘ f ×₁ g ∘ Δ) † ≈⟨ †-homomorphism ⟩ - (f ×₁ g ∘ Δ) † ∘ ∇ † ≈⟨ pushˡ †-homomorphism ⟩ - Δ † ∘ (f ×₁ g) † ∘ ∇ † ≈⟨ Δ† ⟩∘⟨ †-resp-×₁ ⟩∘⟨ ∇† ⟩ - ∇ ∘ (f †) ×₁ (g †) ∘ Δ ∎ + (f + g) † ≈⟨ ⟨ +-∇∘⟨⟩ ⟩† ⟩ + (∇ ∘ ⟨ f , g ⟩) † ≈⟨ †-homomorphism ⟩ + ⟨ f , g ⟩ † ∘ ∇ † ≈⟨ refl⟩∘⟨ ∇† ⟩ + ⟨ f , g ⟩ † ∘ Δ ≈⟨ ⟨⟩-† ⟩∘⟨refl ⟩ + [ f † , g † ] ∘ Δ ≈⟨ pushˡ (Equiv.sym ∇∘×₁) ⟩ + ∇ ∘ (f †) ×₁ (g †) ∘ Δ ≈⟨ refl⟩∘⟨ ×₁∘Δ ⟩ + ∇ ∘ ⟨ f † , g † ⟩ ≈⟨ +-∇∘⟨⟩ ⟨ + (f †) + (g †) ∎ -- bilinearity of composition ∘-distribˡ : {A B C : Obj} {f : B ⇒ C} {g h : A ⇒ B} → f ∘ (g + h) ≈ f ∘ g + f ∘ h @@ -170,9 +174,9 @@ record IdempotentSemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where ≤-trans : {A B : Obj} {f g h : A ⇒ B} → f ≤ g → g ≤ h → f ≤ h ≤-trans {A} {B} {f} {g} {h} f≤g g≤h = begin - f + h ≈⟨ refl⟩∘⟨ ×₁-congˡ g≤h ⟩∘⟨refl ⟨ + f + h ≈⟨ +-congˡ g≤h ⟨ f + (g + h) ≈⟨ +-assoc f g h ⟨ - (f + g) + h ≈⟨ refl⟩∘⟨ ×₁-congʳ f≤g ⟩∘⟨refl ⟩ + (f + g) + h ≈⟨ +-congʳ f≤g ⟩ g + h ≈⟨ g≤h ⟩ h ∎ @@ -199,14 +203,13 @@ record IdempotentSemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where → g ≤ i → (f ×₁ g) ≤ (h ×₁ i) ≤-resp-×₁ {f = f} {h} {g} {i} f≤h g≤i = begin - ∇ ∘ (f ×₁ g) ×₁ (h ×₁ i) ∘ Δ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ Δ-⊕ ⟩ - ∇ ∘ (f ×₁ g) ×₁ (h ×₁ i) ∘ σ₂₃ ∘ Δ ×₁ Δ ≈⟨ refl⟩∘⟨ extendʳ σ₂₃-×₁ ⟩ - ∇ ∘ σ₂₃ ∘ (f ×₁ h) ×₁ (g ×₁ i) ∘ Δ ×₁ Δ ≈⟨ pushˡ ∇-⊕ ⟩ - ∇ ×₁ ∇ ∘ σ₂₃ ∘ σ₂₃ ∘ (f ×₁ h) ×₁ (g ×₁ i) ∘ Δ ×₁ Δ ≈⟨ refl⟩∘⟨ cancelˡ σ₂₃-σ₂₃ ⟩ - ∇ ×₁ ∇ ∘ (f ×₁ h) ×₁ (g ×₁ i) ∘ Δ ×₁ Δ ≈⟨ refl⟩∘⟨ ×₁∘×₁ ⟩ - ∇ ×₁ ∇ ∘ (f ×₁ h ∘ Δ) ×₁ (g ×₁ i ∘ Δ) ≈⟨ ×₁∘×₁ ⟩ - (∇ ∘ f ×₁ h ∘ Δ) ×₁ (∇ ∘ g ×₁ i ∘ Δ) ≈⟨ ×₁-cong₂ f≤h g≤i ⟩ - h ×₁ i ∎ + f ×₁ g + h ×₁ i ≈⟨ +-∇∘⟨⟩ ⟩ + ∇ ∘ ⟨ f ×₁ g , h ×₁ i ⟩ ≈⟨ pushˡ ∇-⊕ ⟩ + ∇ ×₁ ∇ ∘ σ₂₃ ∘ ⟨ f ×₁ g , h ×₁ i ⟩ ≈⟨ refl⟩∘⟨ σ₂₃-⟨⟩-×₁ ⟩ + ∇ ×₁ ∇ ∘ ⟨ f , h ⟩ ×₁ ⟨ g , i ⟩ ≈⟨ ×₁∘×₁ ⟩ + (∇ ∘ ⟨ f , h ⟩) ×₁ (∇ ∘ ⟨ g , i ⟩) ≈⟨ ×₁-cong₂ +-∇∘⟨⟩ +-∇∘⟨⟩ ⟨ + (f + h) ×₁ (g + i) ≈⟨ ×₁-cong₂ f≤h g≤i ⟩ + h ×₁ i ∎ ≤-resp-∘ : {A B C : Obj} @@ -234,9 +237,9 @@ record IdempotentSemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where -- special law ∇∘Δ : {A : Obj} → ∇ ∘ Δ ≈ id {A} ∇∘Δ = begin - ∇ ∘ Δ ≈⟨ refl⟩∘⟨ introˡ id×₁id ⟩ - ∇ ∘ id ×₁ id ∘ Δ ≈⟨ idempotent ⟩ - id ∎ + ∇ ∘ Δ ≈⟨ +-∇∘⟨⟩ ⟨ + id + id ≈⟨ idempotent ⟩ + id ∎ dagger-2-poset : Dagger-2-Poset dagger-2-poset = record |