Skip to content

Commit

Permalink
golf fubini proofs
Browse files Browse the repository at this point in the history
  • Loading branch information
@4e554c4c
4e554c4c committed Jun 19, 2024
1 parent cb8c7b6 commit f4e7e5e
Showing 1 changed file with 58 additions and 42 deletions.
100 changes: 58 additions & 42 deletions src/Categories/Diagram/End/Fubini.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ open import Level
open import Data.Product using (Σ; _,_; _×_) renaming (proj₁ to fst; proj₂ to snd)
open import Function using (_$_)

open import Categories.Category using (Category)
open import Categories.Category using (Category; _[_,_]; _[_∘_])
open import Categories.Category.Construction.Functors using (Functors; curry)
open import Categories.Category.Product using (πˡ; πʳ; _⁂_; _※_; Swap) renaming (Product to _×ᶜ_)
open import Categories.Diagram.End using () renaming (End to ∫)
Expand Down Expand Up @@ -49,6 +49,8 @@ module _ (F : Bifunctor (Category.op C ×ᶜ Category.op P) (C ×ᶜ P) D)
module C = Category C
module P = Category P
module D = Category D
C×P = (C ×ᶜ P)
module C×P = Category C×P
open module F = Functor F using (F₀; F₁; F-resp-≈)
∫F = (⨏ (F ′) {ω})
module ∫F = Functor ∫F
Expand All @@ -57,7 +59,7 @@ module _ (F : Bifunctor (Category.op C ×ᶜ Category.op P) (C ×ᶜ P) D)

open _≅_
open Iso
open DinaturalTransformation using (α)
open DinaturalTransformation
open NaturalTransformation using (η)
open Wedge renaming (E to apex)
open Category D
Expand All @@ -71,85 +73,100 @@ module _ (F : Bifunctor (Category.op C ×ᶜ Category.op P) (C ×ᶜ P) D)
-- first, our wedge gives us a wedge in the product
ξ : Wedge F
ξ .apex = x
ξ .dinatural = dtHelper record
{ α = λ { (c , p) → ω.dinatural.α (p , p) c ∘ ρ.dinatural.α p }
; commute = λ { {c , p} {d , q} (f , s) → begin
F₁ ((C.id , P.id) , (f , s)) ∘ (ω.dinatural.α (p , p) c ∘ ρ.dinatural.α p) ∘ id
ξ .dinatural .α (c , p) = ω.dinatural.α (p , p) c ∘ ρ.dinatural.α p
-- unfolded because dtHelper means opening up a record (i.e. no where clause)
ξ .dinatural .op-commute (f , s) = assoc ○ ⟺ (ξ .dinatural .commute (f , s)) ○ sym-assoc
ξ .dinatural .commute {c , p} {d , q} (f , s) = begin
F₁ (C×P.id , (f , s)) ∘ (ωp,p c ∘ ρp) ∘ id
≈⟨ refl⟩∘⟨ identityʳ ⟩
-- First we show dinaturality in C, which is 'trivial'
F₁ ((C.id , P.id) , (f , s)) ∘ (ω.dinatural.α (p , p) c ∘ ρ.dinatural.α p)
≈⟨ (F-resp-≈ ((C.Equiv.sym C.identity² , P.Equiv.sym P.identity²) , (C.Equiv.sym C.identityˡ , P.Equiv.sym P.identityʳ)) ○ F.homomorphism) ⟩∘⟨refl ○ pullˡ assoc ⟩
(F₁ ((C.id , P.id) , (C.id , s)) ∘ F₁ ((C.id , P.id) , (f , P.id)) ∘ ω.dinatural.α (p , p) c) ∘ ρ.dinatural.α p
F₁ (C×P.id , (f , s)) ∘ (ωp,p c ∘ ρp)
≈⟨ F-resp-≈ ((C.Equiv.sym C.identity² , P.Equiv.sym P.identity²) , (C.Equiv.sym C.identityˡ , P.Equiv.sym P.identityʳ)) ⟩∘⟨refl ⟩
F₁ (C×P [ C×P.id ∘ C×P.id ] , C [ C.id ∘ f ] , P [ s ∘ P.id ]) ∘ (ωp,p c ∘ ρ.dinatural.α p)
≈⟨ F.homomorphism ⟩∘⟨refl ⟩
(F₁ (C×P.id , (C.id , s)) ∘ F₁ (C×P.id , (f , P.id))) ∘ (ωp,p c ∘ ρp)
≈⟨ assoc²γβ ⟩
(F₁ (C×P.id , (C.id , s)) ∘ F₁ (C×P.id , (f , P.id)) ∘ ωp,p c) ∘ ρp
≈⟨ (refl⟩∘⟨ refl⟩∘⟨ ⟺ identityʳ) ⟩∘⟨refl ⟩
(F₁ ((C.id , P.id) , (C.id , s)) ∘ F₁ ((C.id , P.id) , (f , P.id)) ∘ ω.dinatural.α (p , p) c ∘ id) ∘ ρ.dinatural.α p
(F₁ (C×P.id , (C.id , s)) ∘ F₁ (C×P.id , (f , P.id)) ∘ ωp,p c ∘ id) ∘ ρp
≈⟨ (refl⟩∘⟨ ω.dinatural.commute (p , p) f) ⟩∘⟨refl ⟩
(F₁ ((C.id , P.id) , (C.id , s)) ∘ F₁ ((f , P.id) , (C.id , P.id)) ∘ ω.dinatural.α (p , p) d ∘ id) ∘ ρ.dinatural.α p
(F₁ (C×P.id , (C.id , s)) ∘ F₁ ((f , P.id) , C×P.id) ∘ ωp,p d ∘ id) ∘ ρp
≈⟨ extendʳ (⟺ F.homomorphism ○ F-resp-≈ ((MR.id-comm C , P.Equiv.refl) , (C.Equiv.refl , MR.id-comm P)) ○ F.homomorphism) ⟩∘⟨refl ⟩
-- now, we must show dinaturality in P
-- First, some reassosiations to make things easier
(F₁ ((f , P.id) , (C.id , P.id)) ∘ F₁ ((C.id , P.id) , (C.id , s)) ∘ ω.dinatural.α (p , p) d ∘ id) ∘ ρ.dinatural.α p
≈⟨ assoc ○ refl⟩∘⟨ assoc ○ refl⟩∘⟨ refl⟩∘⟨ identityʳ ⟩∘⟨refl ⟩
F₁ ((f , P.id) , (C.id , P.id)) ∘ (F₁ ((C.id , P.id) , (C.id , s)) ∘ ω.dinatural.α (p , p) d ∘ ρ.dinatural.α p)
-- First, we get rid of the identity and reassoc
(F₁ ((f , P.id) , C×P.id) ∘ F₁ (C×P.id , (C.id , s)) ∘ ωp,p d ∘ id) ∘ ρp
≈⟨ assoc²βε ⟩
F₁ ((f , P.id) , C×P.id) ∘ F₁ (C×P.id , (C.id , s)) ∘ (ωp,p d ∘ id) ∘ ρp
≈⟨ refl⟩∘⟨ refl⟩∘⟨ identityʳ ⟩∘⟨refl ⟩
F₁ ((f , P.id) , C×P.id) ∘ F₁ (C×P.id , (C.id , s)) ∘ ωp,p d ∘ ρp
-- this is the hard part: we use commutativity from the bottom face of the cube.
-- The fact that this exists (an arrow between ∫ F (p,p,- ,-) to ∫ F (p,q,- ,-)) is due to functorality of ∫ and curry₀.
-- The square commutes by universiality of ω
≈⟨ refl⟩∘⟨ extendʳ (⟺ (end-η-commute ⦃ ω (p , p) ⦄ ⦃ ω (p , q) ⦄ (curry.₀.₁ (F ′) (P.id , s)) d)) ⟩
-- now we can use dinaturality in ρ, which annoyingly has an `id` tacked on the end
F₁ ((f , P.id) , (C.id , P.id)) ∘ ω.dinatural.α (p , q) d ∘ ∫F.F₁ (P.id , s) ∘ ρ.dinatural.α p
F₁ ((f , P.id) , C×P.id) ∘ ωp,q d ∘ ∫F.F₁ (P.id , s) ∘ ρp
≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⟺ identityʳ ⟩
F₁ ((f , P.id) , (C.id , P.id)) ∘ ω.dinatural.α (p , q) d ∘ ∫F.F₁ (P.id , s) ∘ ρ.dinatural.α p ∘ id
F₁ ((f , P.id) , C×P.id) ∘ ωp,q d ∘ ∫F.F₁ (P.id , s) ∘ ρp ∘ id
≈⟨ refl⟩∘⟨ refl⟩∘⟨ ρ.dinatural.commute s ⟩
F₁ ((f , P.id) , (C.id , P.id)) ∘ ω.dinatural.α (p , q) d ∘ ∫F.F₁ (s , P.id) ∘ ρ.dinatural.α q ∘ id
F₁ ((f , P.id) , C×P.id) ∘ ωp,q d ∘ ∫F.F₁ (s , P.id) ∘ ρq ∘ id
≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ identityʳ ⟩
F₁ ((f , P.id) , (C.id , P.id)) ∘ ω.dinatural.α (p , q) d ∘ ∫F.F₁ (s , P.id) ∘ ρ.dinatural.α q
F₁ ((f , P.id) , C×P.id) ∘ ωp,q d ∘ ∫F.F₁ (s , P.id) ∘ ρq
-- and now we're done. step backward through the previous isomorphisms to get dinaturality in f and s together
≈⟨ refl⟩∘⟨ extendʳ (end-η-commute ⦃ ω (q , q) ⦄ ⦃ ω (p , q) ⦄ (curry.₀.₁ (F ′) (s , P.id)) d) ⟩
F₁ ((f , P.id) , (C.id , P.id)) ∘ (F₁ ((C.id , s) , (C.id , P.id)) ∘ ω.dinatural.α (q , q) d ∘ ρ.dinatural.α q)
F₁ ((f , P.id) , C×P.id) ∘ (F₁ ((C.id , s) , C×P.id) ∘ ωq,q d ∘ ρq)
≈⟨ pullˡ (⟺ F.homomorphism ○ F-resp-≈ ((C.identityˡ , P.identityʳ) , (C.identity² , P.identity²))) ⟩
F₁ ((f , s) , (C.id , P.id)) ∘ ω.dinatural.α (q , q) d ∘ ρ.dinatural.α q
F₁ ((f , s) , C×P.id) ∘ ωq,q d ∘ ρq
≈˘⟨ refl⟩∘⟨ identityʳ ⟩
F₁ ((f , s) , (C.id , P.id)) ∘ (ω.dinatural.α (q , q) d ∘ ρ.dinatural.α q) ∘ id
F₁ ((f , s) , C×P.id) ∘ (ωq,q d ∘ ρq) ∘ id
∎
}
}
where ωp,p = ω.dinatural.α (p , p)
ωp,q = ω.dinatural.α (p , q)
ωq,q = ω.dinatural.α (q , q)
ρp = ρ.dinatural.α p
ρq = ρ.dinatural.α q


-- now the opposite direction
private module _ (ξ : Wedge F) where
private
open module ξ = Wedge ξ using () renaming (E to x)
ρ : Wedge ∫F
ρ .apex = x
ρ .dinatural = dtHelper record
{ α = λ p → ω.factor (p , p) record
ρ .dinatural .α p = ω.factor (p , p) record
{ E = x
; dinatural = dtHelper record
{ α = λ c → ξ.dinatural.α (c , p)
; commute = λ f → ξ.dinatural.commute (f , P.id)
}
}
-- end-η-commute ⦃ ω (?) ⦄ ⦃ ω (?) ⦄ (curry.₀.₁ (F ′) (?)) ?
; commute = λ {p} {q} f → ω.unique′ (p , q) λ {c} → begin
ω.dinatural.α (p , q) c ∘ ∫F.₁ (P.id , f) ∘ ω.factor (p , p) _ ∘ id
ρ .dinatural .op-commute f = assoc ○ ⟺ (ρ .dinatural .commute f) ○ sym-assoc
ρ .dinatural .commute {p} {q} f = ω.unique′ (p , q) λ {c} → begin
ωp,q c ∘ ∫F.₁ (P.id , f) ∘ ρp ∘ id
≈⟨ refl⟩∘⟨ refl⟩∘⟨ identityʳ ⟩
ω.dinatural.α (p , q) c ∘ ∫F.₁ (P.id , f) ∘ ω.factor (p , p) _
ωp,q c ∘ ∫F.₁ (P.id , f) ∘ ρp
≈⟨ extendʳ $ end-η-commute ⦃ ω (p , p) ⦄ ⦃ ω (p , q) ⦄ (curry.₀.₁ (F ′) (P.id , f)) c ⟩
F₁ ((C.id , P.id) , (C.id , f)) ∘ ω.dinatural.α (p , p) c ∘ ∫.factor (ω (p , p)) _
F₁ (C×P.id , (C.id , f)) ∘ ωp,p c ∘ ρp
≈⟨ refl⟩∘⟨ ω.universal (p , p) ⟩
F₁ ((C.id , P.id) , (C.id , f)) ∘ ξ.dinatural.α (c , p)
F₁ (C×P.id , (C.id , f)) ∘ ξ.dinatural.α (c , p)
≈˘⟨ refl⟩∘⟨ identityʳ ⟩
F₁ ((C.id , P.id) , (C.id , f)) ∘ ξ.dinatural.α (c , p) ∘ id
F₁ (C×P.id , (C.id , f)) ∘ ξ.dinatural.α (c , p) ∘ id
≈⟨ ξ.dinatural.commute (C.id , f) ⟩
F₁ ((C.id , f) , (C.id , P.id)) ∘ ξ.dinatural.α (c , q) ∘ id
F₁ ((C.id , f) , C×P.id) ∘ ξ.dinatural.α (c , q) ∘ id
≈⟨ refl⟩∘⟨ identityʳ ⟩
F₁ ((C.id , f) , (C.id , P.id)) ∘ ξ.dinatural.α (c , q)
F₁ ((C.id , f) , C×P.id) ∘ ξ.dinatural.α (c , q)
≈˘⟨ refl⟩∘⟨ ω.universal (q , q) ⟩
F₁ ((C.id , f) , (C.id , P.id)) ∘ ω.dinatural.α (q , q) c ∘ ω.factor (q , q) _
F₁ ((C.id , f) , C×P.id) ∘ ωq,q c ∘ ρq
≈˘⟨ extendʳ $ end-η-commute ⦃ ω (q , q) ⦄ ⦃ ω (p , q) ⦄ (curry.₀.₁ (F ′) (f , P.id)) c ⟩
ω.dinatural.α (p , q) c ∘ ∫F.₁ (f , P.id) ∘ ω.factor (q , q) _
ωp,q c ∘ ∫F.₁ (f , P.id) ∘ ρq
≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ identityʳ ⟩
ω.dinatural.α (p , q) c ∘ ∫F.₁ (f , P.id) ∘ ω.factor (q , q) _ ∘ id
ωp,q c ∘ ∫F.₁ (f , P.id) ∘ ρq ∘ id
∎
}
where ωp,p = ω.dinatural.α (p , p)
ωp,q = ω.dinatural.α (p , q)
ωq,q = ω.dinatural.α (q , q)
ρp = ρ .dinatural.α p
ρq = ρ .dinatural.α q

-- This construction is actually stronger than Fubini. It states that the
-- iterated end _is_ an end in the product category.
-- Thus the product end need not exist.
Expand All @@ -160,9 +177,8 @@ module _ (F : Bifunctor (Category.op C ×ᶜ Category.op P) (C ×ᶜ P) D)
eₚ .∫.wedge = ξ eᵢ.wedge
eₚ .∫.factor W = eᵢ.factor (ρ W)
eₚ .∫.universal {W} {c , p} = begin
ξ eᵢ.wedge .dinatural.α (c , p) ∘ eᵢ.factor (ρ W) ≈⟨ Equiv.refl ⟩
(ω.dinatural.α (p , p) c ∘ eᵢ.dinatural.α p) ∘ eᵢ.factor (ρ W) ≈⟨ assoc ⟩
ω.dinatural.α (p , p) c ∘ (eᵢ.dinatural.α p ∘ eᵢ.factor (ρ W)) ≈⟨ refl⟩∘⟨ eᵢ.universal {ρ W} {p} ⟩
ξ eᵢ.wedge .dinatural.α (c , p) ∘ eᵢ.factor (ρ W) ≡⟨⟩
(ω.dinatural.α (p , p) c ∘ eᵢ.dinatural.α p) ∘ eᵢ.factor (ρ W) ≈⟨ pullʳ (eᵢ.universal {ρ W} {p}) ⟩
ω.dinatural.α (p , p) c ∘ (ρ W) .dinatural.α p ≈⟨ ω.universal (p , p) ⟩
W .dinatural.α (c , p) ∎
eₚ .∫.unique {W} {g} h = eᵢ.unique λ {A = p} → Equiv.sym $ ω.unique (p , p) (sym-assoc ○ h)
Expand Down

0 comments on commit f4e7e5e

Please sign in to comment.