Mercurial > hg > Members > kono > Proof > category
changeset 986:e2e11014b0f8
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 04 Mar 2021 18:51:10 +0900 |
| parents | 74728d51177b |
| children | 99c91423b871 |
| files | src/CCC.agda src/CCCGraph.agda src/SetsCompleteness.agda src/ToposEx.agda src/cat-utility.agda |
| diffstat | 5 files changed, 271 insertions(+), 97 deletions(-) [+] |
line wrap: on
line diff
--- a/src/CCC.agda Wed Mar 03 16:30:40 2021 +0900 +++ b/src/CCC.agda Thu Mar 04 18:51:10 2021 +0900 @@ -183,9 +183,9 @@ (Ker : {a : Obj A} → ( h : Hom A a Ω ) → Equalizer A h (A [ ⊤ o (CCC.○ c a) ])) (char : {a b : Obj A} → (m : Hom A b a) → Mono A m → Hom A a Ω) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where field - char-ker : {a b : Obj A } {h : Hom A a Ω} (m : Hom A b a) → (mono : Mono A m) + char-uniqueness : {a b : Obj A } {h : Hom A a Ω} (m : Hom A b a) → (mono : Mono A m) → A [ char m mono ≈ h ] - ker-char : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m) → IsoL A m (equalizer (Ker ( char m mono ))) + ker-iso : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m) → IsoL A m (equalizer (Ker ( char m mono ))) record Topos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where field @@ -200,7 +200,7 @@ Monik h = record { isMono = λ f g → monic (Ker h ) } char-m=⊤ : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m) → A [ A [ char m mono o m ] ≈ A [ ⊤ o CCC.○ c b ] ] char-m=⊤ {a} {b} m mono = begin - char m mono o m ≈⟨ car (IsTopos.char-ker isTopos m mono) ⟩ + char m mono o m ≈⟨ car (IsTopos.char-uniqueness isTopos m mono) ⟩ (⊤ o CCC.○ c a) o m ≈↑⟨ assoc ⟩ ⊤ o (CCC.○ c a o m ) ≈⟨ cdr (IsCCC.e2 (CCC.isCCC c)) ⟩ ⊤ o CCC.○ c b ∎ where open ≈-Reasoning A @@ -213,20 +213,20 @@ open NatD -record IsToposNat {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( １ : Obj A) (TNat : NatD A １ ) - ( gNat : (nat : NatD A １ ) → Hom A (Nat TNat) (Nat nat) ) +record IsToposNat {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( １ : Obj A) (iNat : NatD A １ ) + ( initialNat : (nat : NatD A １ ) → Hom A (Nat iNat) (Nat nat) ) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where field - izero : (nat : NatD A １ ) → A [ A [ gNat nat o nzero TNat ] ≈ nzero nat ] - isuc : (nat : NatD A １ ) → A [ A [ gNat nat o nsuc TNat ] ≈ A [ nsuc nat o gNat nat ] ] + izero : (nat : NatD A １ ) → A [ A [ initialNat nat o nzero iNat ] ≈ nzero nat ] + isuc : (nat : NatD A １ ) → A [ A [ initialNat nat o nsuc iNat ] ≈ A [ nsuc nat o initialNat nat ] ] record ToposNat {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( １ : Obj A) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where field - TNat : NatD A １ - gNat : (nat : NatD A １ ) → Hom A (Nat TNat) (Nat nat) - nat-unique : (nat : NatD A １ ) → {g : Hom A (Nat TNat) (Nat nat) } - → A [ A [ g o nzero TNat ] ≈ nzero nat ] - → A [ A [ g o nsuc TNat ] ≈ A [ nsuc nat o g ] ] - → A [ g ≈ gNat nat ] - isToposN : IsToposNat A １ TNat gNat + iNat : NatD A １ + initialNat : (nat : NatD A １ ) → Hom A (Nat iNat) (Nat nat) + nat-unique : (nat : NatD A １ ) → {g : Hom A (Nat iNat) (Nat nat) } + → A [ A [ g o nzero iNat ] ≈ nzero nat ] + → A [ A [ g o nsuc iNat ] ≈ A [ nsuc nat o g ] ] + → A [ g ≈ initialNat nat ] + isToposN : IsToposNat A １ iNat initialNat
--- a/src/CCCGraph.agda Wed Mar 03 16:30:40 2021 +0900 +++ b/src/CCCGraph.agda Thu Mar 04 18:51:10 2021 +0900 @@ -96,6 +96,17 @@ *-cong refl = refl +tooos : {c : Level } → Topos (Sets {c}) sets +tooos = record { + Ω = {!!} + ; ⊤ = {!!} + ; Ker = {!!} + ; char = {!!} + ; isTopos = record { + + } + } + open import graph
--- a/src/SetsCompleteness.agda Wed Mar 03 16:30:40 2021 +0900 +++ b/src/SetsCompleteness.agda Thu Mar 04 18:51:10 2021 +0900 @@ -9,7 +9,9 @@ open import Function import Relation.Binary.PropositionalEquality -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → ( λ x → f x ≡ λ x → g x ) -postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ +import Axiom.Extensionality.Propositional +postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂ +-- Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ ≡cong = Relation.Binary.PropositionalEquality.cong @@ -53,6 +55,8 @@ open iproduct +open Small + SetsIProduct : { c₂ : Level} → (I : Obj Sets) (ai : I → Obj Sets ) → IProduct I ( Sets { c₂} ) ai SetsIProduct I fi = record { @@ -83,6 +87,61 @@ ip-cong : {q : Obj Sets} {qi qi' : (i : I) → Hom Sets q (fi i)} → ((i : I) → Sets [ qi i ≈ qi' i ]) → Sets [ iproduct1 qi ≈ iproduct1 qi' ] ip-cong {q} {qi} {qi'} qi=qi = extensionality Sets ( ipcx qi=qi ) +data coproduct {c} (a b : Set c) : Set c where + k1 : ( i : a ) → coproduct a b + k2 : ( i : b ) → coproduct a b + +SetsCoProduct : { c₂ : Level} → (a b : Obj (Sets {c₂})) → coProduct Sets a b +SetsCoProduct a b = record { + coproduct = coproduct a b + ; κ1 = λ i → k1 i + ; κ2 = λ i → k2 i + ; isProduct = record { + _+_ = sum + ; κ1f+g=f = extensionality Sets (λ x → refl ) + ; κ2f+g=g = extensionality Sets (λ x → refl ) + ; uniqueness = λ {c} {h} → extensionality Sets (λ x → uniq {c} {h} x ) + ; +-cong = λ {c} {f} {f'} {g} {g'} feq geq → extensionality Sets (pccong feq geq) + } + } where + sum : {c : Obj Sets} → Hom Sets a c → Hom Sets b c → Hom Sets (coproduct a b ) c + sum {c} f g (k1 i) = f i + sum {c} f g (k2 i) = g i + uniq : {c : Obj Sets} {h : Hom Sets (coproduct a b) c} → (x : coproduct a b ) → sum (Sets [ h o (λ i → k1 i) ]) (Sets [ h o (λ i → k2 i) ]) x ≡ h x + uniq {c} {h} (k1 i) = refl + uniq {c} {h} (k2 i) = refl + pccong : {c : Obj Sets} {f f' : Hom Sets a c} {g g' : Hom Sets b c} → f ≡ f' → g ≡ g' → (x : coproduct a b ) → sum f g x ≡ sum f' g' x + pccong refl refl (k1 i) = refl + pccong refl refl (k2 i) = refl + + +data icoproduct {a} (I : Set a) (ki : I → Set a) : Set a where + ki1 : (i : I) (x : ki i ) → icoproduct I ki + +SetsICoProduct : { c₂ : Level} → (I : Obj (Sets {c₂})) (ci : I → Obj Sets ) + → ICoProduct I ( Sets { c₂} ) ci +SetsICoProduct I fi = record { + icoprod = icoproduct I fi + ; ki = λ i x → ki1 i x + ; isICoProduct = record { + icoproduct = isum + ; kif=q = λ {q} {qi} {i} → kif=q {q} {qi} {i} + ; icp-uniqueness = uniq + ; icp-cong = iccong + } + } where + isum : {q : Obj Sets} → ((i : I) → Hom Sets (fi i) q) → Hom Sets (icoproduct I fi) q + isum {q} fi (ki1 i x) = fi i x + kif=q : {q : Obj Sets} {qi : (i : I) → Hom Sets (fi i) q} {i : I} → Sets [ Sets [ isum qi o (λ x → ki1 i x) ] ≈ qi i ] + kif=q {q} {qi} {i} = extensionality Sets (λ x → refl ) + uniq : {q : Obj Sets} {h : Hom Sets (icoproduct I fi) q} → Sets [ isum (λ i → Sets [ h o (λ x → ki1 i x) ]) ≈ h ] + uniq {q} {h} = extensionality Sets u1 where + u1 : (x : icoproduct I fi ) → isum (λ i → Sets [ h o (λ x₁ → ki1 i x₁) ]) x ≡ h x + u1 (ki1 i x) = refl + iccong : {q : Obj Sets} {qi qi' : (i : I) → Hom Sets (fi i) q} → ((i : I) → Sets [ qi i ≈ qi' i ]) → Sets [ isum qi ≈ isum qi' ] + iccong {q} {qi} {qi'} ieq = extensionality Sets u2 where + u2 : (x : icoproduct I fi ) → isum qi x ≡ isum qi' x + u2 (ki1 i x) = cong (λ k → k x ) (ieq i) -- -- e f @@ -143,22 +202,46 @@ open import Relation.Binary.PropositionalEquality open ≡-Reasoning +-- data cequ {c : Level} (A B : Set c) ( f g : A → B ) : Set c where +-- casef : (a : A) → {!!} + +record cequ {c : Level} (A B : Set c) ( f g : A → B ) : Set c where + field + q : B → B + qo : (a : A) → q (f a) ≡ q (g a) + +data cequ' {c : Level} {A B : Set c} ( f g : A → B ) : {a : A } → (f a ≡ g a) → Set c where + celem : {a : A } → (f=g : f a ≡ g a) → cequ' f g f=g + +c-equ : { c₂ : Level} {a b : Obj (Sets {c₂}) } ( f g : Hom (Sets {c₂}) a b ) → (x : b) → cequ a b f g +c-equ {_} {a} {b} f g x = record { q = {!!} ; qo = {!!} } + +SetsIsCoEqualizer : { c₂ : Level} → (a b : Obj (Sets {c₂}) ) (f g : Hom (Sets {c₂}) a b) → IsCoEqualizer Sets (λ x → c-equ {c₂} f g x) f g +SetsIsCoEqualizer {c₂} a b f g = record { + ef=eg = extensionality Sets {!!} + ; k = k + ; ke=h = λ {d} {h} {eq} → ke=h {d} {h} {eq} + ; uniqueness = {!!} + } where + k : {d : Obj Sets} (h : Hom Sets b d) → Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] → Hom Sets (cequ a b f g) d + k = {!!} + ke=h : {d : Obj Sets } {h : Hom Sets b d } → { eq : Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] } + → Sets [ Sets [ k h eq o c-equ f g ] ≈ h ] + ke=h = {!!} open Functor ---- -- C is locally small i.e. Hom C i j is a set c₁ -- -record Small { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) - : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where - field - hom→ : {i j : Obj C } → Hom C i j → I - hom← : {i j : Obj C } → ( f : I ) → Hom C i j - hom-iso : {i j : Obj C } → { f : Hom C i j } → C [ hom← ( hom→ f ) ≈ f ] - hom-rev : {i j : Obj C } → { f : I } → hom→ ( hom← {i} {j} f ) ≡ f - ≡←≈ : {i j : Obj C } → { f g : Hom C i j } → C [ f ≈ g ] → f ≡ g - -open Small +-- record Small { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) +-- : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where +-- field +-- hom→ : {i j : Obj C } → Hom C i j → I +-- hom← : {i j : Obj C } → ( f : I ) → Hom C i j +-- hom-iso : {i j : Obj C } → { f : Hom C i j } → C [ hom← ( hom→ f ) ≈ f ] +-- hom-rev : {i j : Obj C } → { f : I } → hom→ ( hom← {i} {j} f ) ≡ f +-- ≡←≈ : {i j : Obj C } → { f g : Hom C i j } → C [ f ≈ g ] → f ≡ g ΓObj : { c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I : Set c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} )) (i : Obj C ) → Set c₁
--- a/src/ToposEx.agda Wed Mar 03 16:30:40 2021 +0900 +++ b/src/ToposEx.agda Thu Mar 04 18:51:10 2021 +0900 @@ -30,6 +30,10 @@ ⊤ t o ( ○ a o p1 ) ≈⟨ assoc ⟩ (⊤ t o ○ a ) o p1 ∎ + ---- + -- + -- pull back from h + -- topos-pullback : {a : Obj A} → (h : Hom A a (Ω t)) → Pullback A h (⊤ t) topos-pullback {a} h = record { ab = equalizer-c (Ker t h) -- b @@ -63,6 +67,10 @@ IsEqualizer.k (isEqualizer (Ker t h)) p1' (mh=⊤ h p1' p2' eq) ≈⟨ IsEqualizer.uniqueness (isEqualizer (Ker t h)) pe1 ⟩ p' ∎ + ---- + -- + -- pull back from m + -- topos-m-pullback : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m ) → Pullback A (char t m mono ) (⊤ t) topos-m-pullback {a} {b} m mono = record { ab = b @@ -76,15 +84,15 @@ ; uniqueness = uniq } } where - f← = Iso.≅← (IsoL.iso-L (IsTopos.ker-char (isTopos t) m mono )) - f→ = Iso.≅→ (IsoL.iso-L (IsTopos.ker-char (isTopos t) m mono )) + f← = Iso.≅← (IsoL.iso-L (IsTopos.ker-iso (isTopos t) m mono )) + f→ = Iso.≅→ (IsoL.iso-L (IsTopos.ker-iso (isTopos t) m mono )) k : {d : Obj A} (p1 : Hom A d a) → (p2 : Hom A d １) → A [ A [ char t m mono o p1 ] ≈ A [ ⊤ t o p2 ] ] → Hom A d (equalizer-c (Ker t (char t m mono))) k p1 p2 eq = IsEqualizer.k (isEqualizer (Ker t (char t m mono))) p1 (mh=⊤ (char t m mono) p1 p2 eq ) lemma3 : {d : Obj A} (p1 : Hom A d a) → (p2 : Hom A d １) → (eq : A [ A [ char t m mono o p1 ] ≈ A [ ⊤ t o p2 ] ] ) → m o (f← o k p1 p2 eq ) ≈ p1 lemma3 {d} p1 p2 eq = begin m o (f← o k p1 p2 eq ) ≈⟨ assoc ⟩ - (m o f← ) o k p1 p2 eq ≈⟨ car (IsoL.iso≈L (IsTopos.ker-char (isTopos t) m mono )) ⟩ + (m o f← ) o k p1 p2 eq ≈⟨ car (IsoL.iso≈L (IsTopos.ker-iso (isTopos t) m mono )) ⟩ equalizer (Ker t (char t m mono)) o k p1 p2 eq ≈⟨ IsEqualizer.ek=h (isEqualizer (Ker t (char t m mono))) ⟩ p1 ∎ uniq : {d : Obj A} (p' : Hom A d b) (π1' : Hom A d a) (π2' : Hom A d １) @@ -93,13 +101,13 @@ uniq {d} p p1 p2 eq pe1 pe2 = begin f← o k p1 p2 eq ≈⟨ cdr ( IsEqualizer.uniqueness (isEqualizer (Ker t (char t m mono))) lemma4) ⟩ f← o (f→ o p ) ≈⟨ assoc ⟩ - (f← o f→ ) o p ≈⟨ car (Iso.iso→ (IsoL.iso-L (IsTopos.ker-char (isTopos t) m mono ))) ⟩ + (f← o f→ ) o p ≈⟨ car (Iso.iso→ (IsoL.iso-L (IsTopos.ker-iso (isTopos t) m mono ))) ⟩ id1 A _ o p ≈⟨ idL ⟩ p ∎ where lemma4 : A [ A [ equalizer (Ker t (char t m mono)) o (f→ o p) ] ≈ p1 ] lemma4 = begin equalizer (Ker t (char t m mono)) o (f→ o p) ≈⟨ assoc ⟩ - (equalizer (Ker t (char t m mono)) o f→ ) o p ≈⟨ car (IsoL.L≈iso (IsTopos.ker-char (isTopos t) m mono )) ⟩ + (equalizer (Ker t (char t m mono)) o f→ ) o p ≈⟨ car (IsoL.L≈iso (IsTopos.ker-iso (isTopos t) m mono )) ⟩ m o p ≈⟨ pe1 ⟩ p1 ∎ where @@ -120,6 +128,10 @@ g ∎ -- +-- +-- Hom equality and Ω +-- +-- -- a -----------→ + -- f||g ○ a | -- ↓↓ | @@ -161,6 +173,11 @@ < id1 A b , id1 A b > o k ≈⟨ IsCCC.distr-π isCCC ⟩ < id1 A b o k , id1 A b o k > ≈⟨ IsCCC.π-cong isCCC idL idL ⟩ < k , k > ∎ +-- +-- +-- Initial Natural number diagram +-- +-- open NatD open ToposNat n @@ -174,13 +191,13 @@ -- <0,z> <suc o π , h > N : Obj A - N = Nat TNat + N = Nat iNat record prop33 {a : Obj A} (f : Hom A １ a ) ( h : Hom A (N ∧ a) a ) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where field g : Hom A N a - g0=f : A [ A [ g o nzero TNat ] ≈ f ] - gs=h : A [ A [ g o nsuc TNat ] ≈ A [ h o < id1 A _ , g > ] ] + g0=f : A [ A [ g o nzero iNat ] ≈ f ] + gs=h : A [ A [ g o nsuc iNat ] ≈ A [ h o < id1 A _ , g > ] ] xnat : NatD A １ p33 : {a : Obj A} (z : Hom A １ a ) ( h : Hom A (N ∧ a) a ) → prop33 z h @@ -191,54 +208,54 @@ ; xnat = xnat } where xnat : NatD A １ - xnat = record { Nat = N ∧ a ; nzero = < nzero TNat , z > ; nsuc = < nsuc TNat o π , h > } + xnat = record { Nat = N ∧ a ; nzero = < nzero iNat , z > ; nsuc = < nsuc iNat o π , h > } fg : Hom A N (N ∧ a ) - fg = gNat xnat -- < f , g > + fg = initialNat xnat -- < f , g > f : Hom A N N f = π o fg g : Hom A N a g = π' o fg - i : f o nzero TNat ≈ nzero TNat + i : f o nzero iNat ≈ nzero iNat i = begin - f o nzero TNat ≈⟨⟩ - (π o fg) o nzero TNat ≈↑⟨ assoc ⟩ - π o (fg o nzero TNat ) ≈⟨ cdr (IsToposNat.izero isToposN xnat ) ⟩ + f o nzero iNat ≈⟨⟩ + (π o fg) o nzero iNat ≈↑⟨ assoc ⟩ + π o (fg o nzero iNat ) ≈⟨ cdr (IsToposNat.izero isToposN xnat ) ⟩ π o nzero xnat ≈⟨ IsCCC.e3a isCCC ⟩ - nzero TNat ∎ - ii : f o nsuc TNat ≈ nsuc TNat o f + nzero iNat ∎ + ii : f o nsuc iNat ≈ nsuc iNat o f ii = begin - f o nsuc TNat ≈⟨⟩ - (π o fg ) o nsuc TNat ≈↑⟨ assoc ⟩ - π o ( fg o nsuc TNat ) ≈⟨ cdr (IsToposNat.isuc isToposN xnat ) ⟩ - π o (nsuc xnat o gNat xnat) ≈⟨ assoc ⟩ - (π o < nsuc TNat o π , h > ) o gNat xnat ≈⟨ car (IsCCC.e3a isCCC) ⟩ - ( nsuc TNat o π ) o gNat xnat ≈↑⟨ assoc ⟩ - nsuc TNat o ( π o gNat xnat ) ≈⟨⟩ - nsuc TNat o f ∎ + f o nsuc iNat ≈⟨⟩ + (π o fg ) o nsuc iNat ≈↑⟨ assoc ⟩ + π o ( fg o nsuc iNat ) ≈⟨ cdr (IsToposNat.isuc isToposN xnat ) ⟩ + π o (nsuc xnat o initialNat xnat) ≈⟨ assoc ⟩ + (π o < nsuc iNat o π , h > ) o initialNat xnat ≈⟨ car (IsCCC.e3a isCCC) ⟩ + ( nsuc iNat o π ) o initialNat xnat ≈↑⟨ assoc ⟩ + nsuc iNat o ( π o initialNat xnat ) ≈⟨⟩ + nsuc iNat o f ∎ ig : f ≈ id1 A N ig = begin - f ≈⟨ nat-unique TNat i ii ⟩ - gNat TNat ≈↑⟨ nat-unique TNat idL (trans-hom idL (sym idR) ) ⟩ + f ≈⟨ nat-unique iNat i ii ⟩ + initialNat iNat ≈↑⟨ nat-unique iNat idL (trans-hom idL (sym idR) ) ⟩ id1 A _ ∎ - iii : g o nzero TNat ≈ z + iii : g o nzero iNat ≈ z iii = begin - g o nzero TNat ≈⟨⟩ (π' o gNat xnat ) o nzero TNat ≈↑⟨ assoc ⟩ - π' o ( gNat xnat o nzero TNat) ≈⟨ cdr (IsToposNat.izero isToposN xnat) ⟩ - π' o < nzero TNat , z > ≈⟨ IsCCC.e3b isCCC ⟩ + g o nzero iNat ≈⟨⟩ (π' o initialNat xnat ) o nzero iNat ≈↑⟨ assoc ⟩ + π' o ( initialNat xnat o nzero iNat) ≈⟨ cdr (IsToposNat.izero isToposN xnat) ⟩ + π' o < nzero iNat , z > ≈⟨ IsCCC.e3b isCCC ⟩ z ∎ - iv : g o nsuc TNat ≈ h o < f , g > + iv : g o nsuc iNat ≈ h o < f , g > iv = begin - g o nsuc TNat ≈⟨⟩ - (π' o gNat xnat) o nsuc TNat ≈↑⟨ assoc ⟩ - π' o (gNat xnat o nsuc TNat ) ≈⟨ cdr (IsToposNat.isuc isToposN xnat) ⟩ - π' o (nsuc xnat o gNat xnat ) ≈⟨ assoc ⟩ - (π' o nsuc xnat ) o gNat xnat ≈⟨ car (IsCCC.e3b isCCC) ⟩ - h o gNat xnat ≈↑⟨ cdr (IsCCC.e3c isCCC) ⟩ + g o nsuc iNat ≈⟨⟩ + (π' o initialNat xnat) o nsuc iNat ≈↑⟨ assoc ⟩ + π' o (initialNat xnat o nsuc iNat ) ≈⟨ cdr (IsToposNat.isuc isToposN xnat) ⟩ + π' o (nsuc xnat o initialNat xnat ) ≈⟨ assoc ⟩ + (π' o nsuc xnat ) o initialNat xnat ≈⟨ car (IsCCC.e3b isCCC) ⟩ + h o initialNat xnat ≈↑⟨ cdr (IsCCC.e3c isCCC) ⟩ h o < π o fg , π' o fg > ≈⟨⟩ h o < f , g > ∎ - v : A [ A [ g o nsuc TNat ] ≈ A [ h o < id1 A N , g > ] ] + v : A [ A [ g o nsuc iNat ] ≈ A [ h o < id1 A N , g > ] ] v = begin - g o nsuc TNat ≈⟨ iv ⟩ + g o nsuc iNat ≈⟨ iv ⟩ h o < f , g > ≈⟨ cdr ( IsCCC.π-cong isCCC ig refl-hom) ⟩ h o < id1 A N , g > ∎ @@ -248,11 +265,11 @@ -- / ↓ \ -- N --→ N ←-- a -- - cor33 : coProduct A １ (Nat TNat ) -- N ≅ N + 1 + cor33 : coProduct A １ (Nat iNat ) -- N ≅ N + 1 cor33 = record { coproduct = N - ; κ1 = nzero TNat - ; κ2 = nsuc TNat + ; κ1 = nzero iNat + ; κ2 = nsuc iNat ; isProduct = record { _+_ = λ {a} f g → prop33.g (p f ( g o π )) -- Hom A (N n ∧ a) a ; κ1f+g=f = λ {a} {f} {g} → prop33.g0=f (p f (g o π ) ) @@ -263,55 +280,55 @@ } where p : {a : Obj A} (f : Hom A １ a) ( h : Hom A (N ∧ a) a ) → prop33 f h p f h = p33 f h - k2 : {a : Obj A} {f : Hom A １ a} {g : Hom A (Nat TNat) a } - → A [ A [ prop33.g (p f (g o π)) o nsuc TNat ] ≈ g ] + k2 : {a : Obj A} {f : Hom A １ a} {g : Hom A (Nat iNat) a } + → A [ A [ prop33.g (p f (g o π)) o nsuc iNat ] ≈ g ] k2 {a} {f} {g} = begin - (prop33.g (p f (g o π)) o nsuc TNat) ≈⟨ prop33.gs=h (p f (g o π )) ⟩ + (prop33.g (p f (g o π)) o nsuc iNat) ≈⟨ prop33.gs=h (p f (g o π )) ⟩ ( g o π ) o < id1 A N , prop33.g (p f (g o π)) > ≈⟨ sym assoc ⟩ g o ( π o < id1 A N , prop33.g (p f (g o π)) >) ≈⟨ cdr (IsCCC.e3a isCCC ) ⟩ g o id1 A N ≈⟨ idR ⟩ g ∎ - pp : {c : Obj A} {h : Hom A (Nat TNat) c} → prop33 ( h o nzero TNat ) ( (h o nsuc TNat) o π) - pp {c} {h} = p ( h o nzero TNat ) ( (h o nsuc TNat) o π) - uniq : {c : Obj A} {h : Hom A (Nat TNat) c} → + pp : {c : Obj A} {h : Hom A (Nat iNat) c} → prop33 ( h o nzero iNat ) ( (h o nsuc iNat) o π) + pp {c} {h} = p ( h o nzero iNat ) ( (h o nsuc iNat) o π) + uniq : {c : Obj A} {h : Hom A (Nat iNat) c} → prop33.g pp ≈ h uniq {c} {h} = begin prop33.g pp ≈⟨⟩ - π' o gNat (prop33.xnat pp) ≈↑⟨ cdr (nat-unique (prop33.xnat pp) ( + π' o initialNat (prop33.xnat pp) ≈↑⟨ cdr (nat-unique (prop33.xnat pp) ( begin - < id1 A _ , h > o nzero TNat ≈⟨ IsCCC.distr-π isCCC ⟩ - < id1 A _ o nzero TNat , h o nzero TNat > ≈⟨ IsCCC.π-cong isCCC idL refl-hom ⟩ - < nzero TNat , h o nzero TNat > ≈⟨⟩ + < id1 A _ , h > o nzero iNat ≈⟨ IsCCC.distr-π isCCC ⟩ + < id1 A _ o nzero iNat , h o nzero iNat > ≈⟨ IsCCC.π-cong isCCC idL refl-hom ⟩ + < nzero iNat , h o nzero iNat > ≈⟨⟩ nzero (prop33.xnat pp) ∎ ) (begin - < id1 A _ , h > o nsuc TNat ≈⟨ IsCCC.distr-π isCCC ⟩ - < id1 A _ o nsuc TNat , h o nsuc TNat > ≈⟨ IsCCC.π-cong isCCC idL refl-hom ⟩ - < nsuc TNat , h o nsuc TNat > ≈↑⟨ IsCCC.π-cong isCCC idR idR ⟩ - < nsuc TNat o id1 A _ , (h o nsuc TNat ) o id1 A _ > ≈↑⟨ IsCCC.π-cong isCCC (cdr (IsCCC.e3a isCCC)) (cdr (IsCCC.e3a isCCC)) ⟩ - < nsuc TNat o ( π o < id1 A _ , h > ) , (h o nsuc TNat ) o ( π o < id1 A _ , h > ) > ≈⟨ IsCCC.π-cong isCCC assoc assoc ⟩ - < (nsuc TNat o π ) o < id1 A _ , h > , ((h o nsuc TNat ) o π ) o < id1 A _ , h > > ≈↑⟨ IsCCC.distr-π isCCC ⟩ - < nsuc TNat o π , (h o nsuc TNat ) o π > o < id1 A _ , h > ≈⟨⟩ + < id1 A _ , h > o nsuc iNat ≈⟨ IsCCC.distr-π isCCC ⟩ + < id1 A _ o nsuc iNat , h o nsuc iNat > ≈⟨ IsCCC.π-cong isCCC idL refl-hom ⟩ + < nsuc iNat , h o nsuc iNat > ≈↑⟨ IsCCC.π-cong isCCC idR idR ⟩ + < nsuc iNat o id1 A _ , (h o nsuc iNat ) o id1 A _ > ≈↑⟨ IsCCC.π-cong isCCC (cdr (IsCCC.e3a isCCC)) (cdr (IsCCC.e3a isCCC)) ⟩ + < nsuc iNat o ( π o < id1 A _ , h > ) , (h o nsuc iNat ) o ( π o < id1 A _ , h > ) > ≈⟨ IsCCC.π-cong isCCC assoc assoc ⟩ + < (nsuc iNat o π ) o < id1 A _ , h > , ((h o nsuc iNat ) o π ) o < id1 A _ , h > > ≈↑⟨ IsCCC.distr-π isCCC ⟩ + < nsuc iNat o π , (h o nsuc iNat ) o π > o < id1 A _ , h > ≈⟨⟩ nsuc (prop33.xnat pp) o < id1 A _ , h > ∎ )) ⟩ π' o < id1 A _ , h > ≈⟨ IsCCC.e3b isCCC ⟩ h ∎ - pcong : {a : Obj A } {f f' : Hom A １ a } {g g' : Hom A (Nat TNat) a } → (f=f' : f ≈ f' ) → ( g=g' : g ≈ g' ) + pcong : {a : Obj A } {f f' : Hom A １ a } {g g' : Hom A (Nat iNat) a } → (f=f' : f ≈ f' ) → ( g=g' : g ≈ g' ) → prop33.g (p f (g o π)) ≈ prop33.g (p f' (g' o π)) pcong {a} {f} {f'} {g} {g'} f=f' g=g' = begin prop33.g (p f (g o π)) ≈⟨⟩ - π' o (gNat (prop33.xnat (p f (g o π)))) ≈↑⟨ cdr (nat-unique (prop33.xnat (p f (g o π))) lem1 lem2 ) ⟩ - π' o (gNat (prop33.xnat (p f' (g' o π)))) ≈⟨⟩ + π' o (initialNat (prop33.xnat (p f (g o π)))) ≈↑⟨ cdr (nat-unique (prop33.xnat (p f (g o π))) lem1 lem2 ) ⟩ + π' o (initialNat (prop33.xnat (p f' (g' o π)))) ≈⟨⟩ prop33.g (p f' (g' o π)) ∎ where - lem1 : A [ A [ gNat (prop33.xnat (p f' ((A Category.o g') π))) o nzero TNat ] ≈ nzero (prop33.xnat (p f ((A Category.o g) π))) ] + lem1 : A [ A [ initialNat (prop33.xnat (p f' ((A Category.o g') π))) o nzero iNat ] ≈ nzero (prop33.xnat (p f ((A Category.o g) π))) ] lem1 = begin - gNat (prop33.xnat (p f' (g' o π))) o nzero TNat ≈⟨ IsToposNat.izero isToposN _ ⟩ + initialNat (prop33.xnat (p f' (g' o π))) o nzero iNat ≈⟨ IsToposNat.izero isToposN _ ⟩ nzero (prop33.xnat (p f' (g' o π))) ≈⟨⟩ - < nzero TNat , f' > ≈⟨ IsCCC.π-cong isCCC refl-hom (sym f=f') ⟩ - < nzero TNat , f > ≈⟨⟩ + < nzero iNat , f' > ≈⟨ IsCCC.π-cong isCCC refl-hom (sym f=f') ⟩ + < nzero iNat , f > ≈⟨⟩ nzero (prop33.xnat (p f (g o π))) ∎ - lem2 : A [ A [ gNat (prop33.xnat (p f' (g' o π))) o nsuc TNat ] ≈ A [ nsuc (prop33.xnat (p f (g o π))) o gNat (prop33.xnat (p f' (g' o π))) ] ] + lem2 : A [ A [ initialNat (prop33.xnat (p f' (g' o π))) o nsuc iNat ] ≈ A [ nsuc (prop33.xnat (p f (g o π))) o initialNat (prop33.xnat (p f' (g' o π))) ] ] lem2 = begin - gNat (prop33.xnat (p f' (g' o π))) o nsuc TNat ≈⟨ IsToposNat.isuc isToposN _ ⟩ - nsuc (prop33.xnat (p f' (g' o π))) o gNat (prop33.xnat (p f' (g' o π))) ≈⟨⟩ - < (nsuc TNat) o π , g' o π > o gNat (prop33.xnat (p f' (g' o π))) ≈⟨ car ( IsCCC.π-cong isCCC refl-hom (car (sym g=g')) ) ⟩ - < (nsuc TNat) o π , g o π > o gNat (prop33.xnat (p f' (g' o π))) ≈⟨⟩ - nsuc (prop33.xnat (p f (g o π))) o gNat (prop33.xnat (p f' (g' o π))) ∎ + initialNat (prop33.xnat (p f' (g' o π))) o nsuc iNat ≈⟨ IsToposNat.isuc isToposN _ ⟩ + nsuc (prop33.xnat (p f' (g' o π))) o initialNat (prop33.xnat (p f' (g' o π))) ≈⟨⟩ + < (nsuc iNat) o π , g' o π > o initialNat (prop33.xnat (p f' (g' o π))) ≈⟨ car ( IsCCC.π-cong isCCC refl-hom (car (sym g=g')) ) ⟩ + < (nsuc iNat) o π , g o π > o initialNat (prop33.xnat (p f' (g' o π))) ≈⟨⟩ + nsuc (prop33.xnat (p f (g o π))) o initialNat (prop33.xnat (p f' (g' o π))) ∎
--- a/src/cat-utility.agda Wed Mar 03 16:30:40 2021 +0900 +++ b/src/cat-utility.agda Thu Mar 04 18:51:10 2021 +0900 @@ -247,6 +247,22 @@ equalizer : Hom A equalizer-c a isEqualizer : IsEqualizer A equalizer f g + record IsCoEqualizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {c a b : Obj A} (e : Hom A b c) (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where + field + ef=eg : A [ A [ e o f ] ≈ A [ e o g ] ] + k : {d : Obj A} (h : Hom A b d) → A [ A [ h o f ] ≈ A [ h o g ] ] → Hom A c d + ke=h : {d : Obj A} → ∀ {h : Hom A b d } → {eq : A [ A [ h o f ] ≈ A [ h o g ] ] } → A [ A [ k {d} h eq o e ] ≈ h ] + uniqueness : {d : Obj A} → ∀ {h : Hom A b d } → {eq : A [ A [ h o f ] ≈ A [ h o g ] ] } → {k' : Hom A c d} → + A [ A [ k' o e ] ≈ h ] → A [ k {d} h eq ≈ k' ] + equalizer1 : Hom A b c + equalizer1 = e + + record CoEqualizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A} (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where + field + coEqualizer-c : Obj A + coEqualizer : Hom A coEqualizer-c a + isCoEqualizer : IsEqualizer A coEqualizer f g + -- -- Product -- @@ -296,6 +312,19 @@ κ2 : Hom A b coproduct isProduct : IsCoProduct A a b coproduct κ1 κ2 + ---- + -- C is locally small i.e. Hom C i j is a set c₁ + -- + open import Relation.Binary.PropositionalEquality using (_≡_) + record Small { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where + field + hom→ : {i j : Obj C } → Hom C i j → I + hom← : {i j : Obj C } → ( f : I ) → Hom C i j + hom-iso : {i j : Obj C } → { f : Hom C i j } → C [ hom← ( hom→ f ) ≈ f ] + hom-rev : {i j : Obj C } → { f : I } → hom→ ( hom← {i} {j} f ) ≡ f + ≡←≈ : {i j : Obj C } → { f g : Hom C i j } → C [ f ≈ g ] → f ≡ g + ----- -- -- product on arbitrary index @@ -335,6 +364,40 @@ pi : (i : I ) → Hom A iprod ( ai i ) isIProduct : IsIProduct I A iprod ai pi + record IsICoProduct { c c₁ c₂ ℓ : Level} ( I : Set c) ( A : Category c₁ c₂ ℓ ) + ( p : Obj A ) -- coproduct + ( ci : I → Obj A ) -- cases + ( ki : (i : I ) → Hom A ( ci i ) p ) -- coprojections + : Set (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where + field + icoproduct : {q : Obj A} → ( qi : (i : I) → Hom A (ci i) q ) → Hom A p q + kif=q : {q : Obj A} → { qi : (i : I) → Hom A (ci i) q } + → ∀ { i : I } → A [ A [ ( icoproduct qi ) o ( ki i ) ] ≈ (qi i) ] + icp-uniqueness : {q : Obj A} { h : Hom A p q } → A [ icoproduct ( λ (i : I) → A [ h o (ki i) ] ) ≈ h ] + icp-cong : {q : Obj A} → { qi : (i : I) → Hom A (ci i) q} → { qi' : (i : I) → Hom A (ci i) q } + → ( ∀ (i : I ) → A [ qi i ≈ qi' i ] ) → A [ icoproduct qi ≈ icoproduct qi' ] + -- another form of uniquness + icp-uniqueness1 : {q : Obj A} → ( qi : (i : I) → Hom A (ci i) q ) → ( product' : Hom A p q ) + → ( ∀ { i : I } → A [ A [ product' o ( ki i )] ≈ (qi i) ] ) + → A [ product' ≈ icoproduct qi ] + icp-uniqueness1 {a} qi product' eq = let open ≈-Reasoning (A) in begin + product' + ≈↑⟨ icp-uniqueness ⟩ + icoproduct (λ i₁ → A [ product' o ki i₁ ]) + ≈⟨ icp-cong ( λ i → begin + product' o ki i + ≈⟨ eq {i} ⟩ + qi i + ∎ ) ⟩ + icoproduct qi + ∎ + + record ICoProduct { c c₁ c₂ ℓ : Level} ( I : Set c) ( A : Category c₁ c₂ ℓ ) (ci : I → Obj A) : Set (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where + field + icoprod : Obj A + ki : (i : I ) → Hom A ( ci i ) icoprod + isICoProduct : IsICoProduct I A icoprod ci ki + -- Pullback -- f