1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
|
{-# OPTIONS --without-K --safe #-}
open import Categories.Category.Core using (Category)
open import Level using (Level)
module Category.Cocomplete.Finitely.Product {o β e : Level} {π π : Category o β e} where
open import Categories.Category using (_[_,_])
open import Categories.Category.Cocomplete.Finitely using (FinitelyCocomplete)
open import Categories.Category.Cocartesian using (Cocartesian; BinaryCoproducts)
open import Categories.Category.Product using (Product)
open import Categories.Diagram.Coequalizer using (Coequalizer)
open import Categories.Object.Coproduct using (Coproduct)
open import Categories.Object.Initial using (IsInitial; Initial)
open import Data.Product.Base using (_,_; _Γ_; dmap; zip; map)
Initial-Γ : Initial π β Initial π β Initial (Product πΒ π)
Initial-Γ initial-π initial-π = record
{ β₯ = π.β₯ , π.β₯
; β₯-is-initial = record
{ ! = π.! , π.!
; !-unique = dmap π.!-unique π.!-unique
}
}
where
module π = Initial initial-π
module π = Initial initial-π
Coproducts-Γ : BinaryCoproducts π β BinaryCoproducts π β BinaryCoproducts (Product π π)
Coproducts-Γ coproducts-π coproducts-π = record { coproduct = coproduct }
where
coproduct : β {(Aβ , Bβ) (Aβ , Bβ) : _ Γ _} β Coproduct (Product π π) (Aβ , Bβ) (Aβ , Bβ)
coproduct = record
{ A+B = π.A+B , π.A+B
; iβ = π.iβ , π.iβ
; iβ = π.iβ , π.iβ
; [_,_] = zip π.[_,_] π.[_,_]
; injectβ = π.injectβ , π.injectβ
; injectβ = π.injectβ , π.injectβ
; unique = zip π.unique π.unique
}
where
module Coprod {π} (coprods : BinaryCoproducts π) where
open BinaryCoproducts coprods using (coproduct)
open coproduct public
module π = Coprod coproducts-π
module π = Coprod coproducts-π
Coequalizer-Γ
: (β {A} {B} (f g : π [ A , B ]) β Coequalizer π f g)
β (β {A} {B} (f g : π [ A , B ]) β Coequalizer π f g)
β β {A} {B} {C} {D} ((fβ , gβ) (fβ , gβ) : π [ A , B ] Γ π [ C , D ])
β Coequalizer (Product π π) (fβ , gβ) (fβ , gβ)
Coequalizer-Γ coequalizer-π coequalizer-π (fβ , gβ) (fβ , gβ) = record
{ arr = π.arr , π.arr
; isCoequalizer = record
{ equality = π.equality , π.equality
; coequalize = map π.coequalize π.coequalize
; universal = π.universal , π.universal
; unique = map π.unique π.unique
}
}
where
module π = Coequalizer (coequalizer-π fβ fβ)
module π = Coequalizer (coequalizer-π gβ gβ)
Cocartesian-Γ : Cocartesian π β Cocartesian π β Cocartesian (Product π π)
Cocartesian-Γ cocartesian-π cocartesian-π = record
{ initial = Initial-Γ π.initial π.initial
; coproducts = Coproducts-Γ π.coproducts π.coproducts
}
where
module π = Cocartesian cocartesian-π
module π = Cocartesian cocartesian-π
FinitelyCocomplete-Γ : FinitelyCocomplete π β FinitelyCocomplete π β FinitelyCocomplete (Product π π)
FinitelyCocomplete-Γ finitelyCocomplete-π finitelyCocomplete-π = record
{ cocartesian = Cocartesian-Γ π.cocartesian π.cocartesian
; coequalizer = Coequalizer-Γ π.coequalizer π.coequalizer
}
where
module π = FinitelyCocomplete finitelyCocomplete-π
module π = FinitelyCocomplete finitelyCocomplete-π
|
