module SOAS.Families.BCCC {T : Set} where
open import SOAS.Common
open import SOAS.Context {T}
open import SOAS.Sorting {T}
open import SOAS.Families.Core {T}
open import SOAS.Families.Isomorphism {T}
import Categories.Category.CartesianClosed.Canonical as Canonical
import Categories.Category.CartesianClosed as CCC
import Categories.Category.Cartesian as Cart
open import Categories.Category.Cocartesian
open import Categories.Category.BicartesianClosed
import Categories.Object.Initial as Initial
open import Categories.Category.Monoidal
import Data.Unit as Unit
import Data.Empty as Empty
𝔽am-CanCCC : Canonical.CartesianClosed 𝔽amilies
𝔽am-CanCCC = record
{ ⊤ = λ Γ → Unit.⊤
; _×_ = λ X Y Γ → X Γ × Y Γ
; ! = λ _ → Unit.tt
; π₁ = proj₁
; π₂ = proj₂
; ⟨_,_⟩ = λ f g x → f x , g x
; !-unique = λ f → refl
; π₁-comp = refl
; π₂-comp = refl
; ⟨,⟩-unique = λ p₁ p₂ {Γ}{x} → sym (cong₂ _,_ p₁ p₂)
; _^_ = λ X Y Γ → Y Γ → X Γ
; eval = λ{ (f , x) → f x}
; curry = λ f x y → f (x , y)
; eval-comp = refl
; curry-resp-≈ = λ{X}{Y}{Z}{f}{g} p → ext (λ x → p)
; curry-unique = λ p → ext (λ x → p)
}
𝔽am-CCC : CCC.CartesianClosed 𝔽amilies
𝔽am-CCC = Canonical.Equivalence.fromCanonical _ 𝔽am-CanCCC
module 𝔽am-CCC = CCC.CartesianClosed 𝔽am-CCC
𝔽am-Cocartesian : Cocartesian 𝔽amilies
𝔽am-Cocartesian = record
{ initial = record { ⊥ = λ Γ → Empty.⊥ ; ⊥-is-initial = record { ! = λ () ; !-unique = λ{ f {Γ} {()}} } }
; coproducts = record { coproduct = λ{X}{Y} → record
{ A+B = λ Γ → X Γ ⊎ Y Γ
; i₁ = inj₁
; i₂ = inj₂
; [_,_] = λ{ f g (inj₁ x) → f x ; f g (inj₂ y) → g y}
; inject₁ = refl
; inject₂ = refl
; unique = λ{ p₁ p₂ {Γ} {inj₁ x} → sym p₁ ; p₁ p₂ {Γ} {inj₂ y} → sym p₂}
} }
}
module 𝔽am-Cocart = Cocartesian 𝔽am-Cocartesian
𝔽am-BCCC : BicartesianClosed 𝔽amilies
𝔽am-BCCC = record { cartesianClosed = 𝔽am-CCC ; cocartesian = 𝔽am-Cocartesian }
module 𝔽am-BCCC = BicartesianClosed 𝔽am-BCCC
_×ₘ_ : Family → Family → Family
_×ₘ_ = 𝔽am-CCC._×_
_+ₘ_ : Family → Family → Family
_+ₘ_ = 𝔽am-Cocart._+_
_⇨_ : Family → Family → Family
_⇨_ = 𝔽am-CCC._⇨_
infixr 25 _⇨_
⊤ₘ : Family
⊤ₘ Γ = Unit.⊤
private variable X Y Z W : Family
curryₘ-iso : (X ×ₘ Y ⇾ Z) ≅ₛ (X ⇾ Y ⇨ Z)
curryₘ-iso = record
{ from = λ f x y → f (x , y)
; to = λ{ f (x , y) → f x y }
; iso = record { isoˡ = refl ; isoʳ = refl }
}
⇾-cong : X ≅ₘ Y → W ≅ₘ Z → (X ⇾ W) ≅ₛ (Y ⇾ Z)
⇾-cong X≅Y W≅Z = record
{ from = λ f y → _≅ₘ_.from W≅Z (f (_≅ₘ_.to X≅Y y))
; to = λ g x → _≅ₘ_.to W≅Z (g (_≅ₘ_.from X≅Y x))
; iso = record
{ isoˡ = λ {f} → dext′ (trans (_≅ₘ_.isoˡ W≅Z) (cong f (_≅ₘ_.isoˡ X≅Y)))
; isoʳ = λ {g} → dext′ (trans (_≅ₘ_.isoʳ W≅Z) (cong g (_≅ₘ_.isoʳ X≅Y)))
}
}
⇾-≅dom : X ≅ₘ Y → (X ⇾ W) ≅ₛ (Y ⇾ W)
⇾-≅dom X≅Y = ⇾-cong X≅Y ≅ₘ.refl
⇾-≅cod : W ≅ₘ Z → (X ⇾ W) ≅ₛ (X ⇾ Z)
⇾-≅cod W≅Z = ⇾-cong ≅ₘ.refl W≅Z
𝔽amₛ-CanCCC : Canonical.CartesianClosed 𝔽amiliesₛ
𝔽amₛ-CanCCC = 𝕊orted-CanCCC 𝔽am-CanCCC
𝔽amₛ-CCC : CCC.CartesianClosed 𝔽amiliesₛ
𝔽amₛ-CCC = Canonical.Equivalence.fromCanonical _ 𝔽amₛ-CanCCC
𝔽amₛ-Cocartesian : Cocartesian 𝔽amiliesₛ
𝔽amₛ-Cocartesian = 𝕊orted-Cocartesian 𝔽am-Cocartesian
𝔽amₛ-BCCC : BicartesianClosed 𝔽amiliesₛ
𝔽amₛ-BCCC = 𝕊orted-BCCC 𝔽am-BCCC
module 𝔽amₛ-CCC = CCC.CartesianClosed 𝔽amₛ-CCC
module 𝔽amₛ-Cocart = Cocartesian 𝔽amₛ-Cocartesian
𝔽amₛ-Mon : Monoidal 𝔽amiliesₛ
𝔽amₛ-Mon = Cart.CartesianMonoidal.monoidal 𝔽amiliesₛ 𝔽amₛ-CCC.cartesian
_×̣ₘ_ : Familyₛ → Familyₛ → Familyₛ
_×̣ₘ_ = 𝔽amₛ-CCC._×_
_+̣ₘ_ : Familyₛ → Familyₛ → Familyₛ
_+̣ₘ_ = 𝔽amₛ-Cocart._+_
_⇨̣_ : Familyₛ → Familyₛ → Familyₛ
_⇨̣_ = 𝔽amₛ-CCC._⇨_
infixr 25 _⇨̣_