# HG changeset patch # User Shinji KONO # Date 1613846076 -32400 # Node ID 6aa6cbf630a05dc076427b2fc9c2845fd1bd9e1b # Parent eb62812b5885d1cb0aa3cd72c679ecd89d5118fc fix Burroni diff -r eb62812b5885 -r 6aa6cbf630a0 src/CCC.agda --- a/src/CCC.agda Fri Feb 19 12:09:48 2021 +0900 +++ b/src/CCC.agda Sun Feb 21 03:34:36 2021 +0900 @@ -125,8 +125,17 @@ ---- -- -- Sub Object Classifier as Topos +-- pull back on +-- ○ b +-- b ----------------------→ 1 +-- | | +-- | | +-- m | | ⊤ +-- | | +-- ↓ ↓ +-- a ----------------------→ Ω +-- h -- - open Equalizer record Mono {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {b a : Obj A} (mono : Hom A b a) : Set (c₁ ⊔ c₂ ⊔ ℓ) where @@ -143,9 +152,9 @@ (Ker : {a : Obj A} → ( h : Hom A a Ω ) → Equalizer A h (A [ ⊤ o (○ 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-id : {a b : Obj A } {h : Hom A a Ω} → (m : Hom A b a) → (mono : Mono A m) + char-ker : {a b : Obj A } {h : Hom A a Ω} → A [ char (equalizer (Ker h)) record { isMono = monic (Ker h) } ≈ h ] - ker-char-iso : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m) → Iso A b ( equalizer-c (Ker ( char m mono ))) + ker-char : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m) → Iso A b ( equalizer-c (Ker ( char m mono ))) record Topos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( １ : Obj A) (○ : (a : Obj A ) → Hom A a １) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where field diff -r eb62812b5885 -r 6aa6cbf630a0 src/CatExponetial.agda --- a/src/CatExponetial.agda Fri Feb 19 12:09:48 2021 +0900 +++ b/src/CatExponetial.agda Sun Feb 21 03:34:36 2021 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --allow-unsolved-metas #-} + ---- -- -- B^A @@ -12,7 +14,9 @@ open import HomReasoning open import cat-utility - +-- open import Relation.Binary hiding (_⇔_) +-- open import Relation.Binary.Core hiding (_⇔_) +-- open import Relation.Binary.PropositionalEquality hiding ( [_] ) -- Object is a Functor : A → B -- Hom is a natural transformation @@ -70,20 +74,16 @@ open import Relation.Binary.Core isB^A : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ' ) → IsCategory (CObj A B) (CHom A B) _==_ _+_ (Cid A B) isB^A {c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} A B = - record { isEquivalence = record {refl = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory B )); - sym = λ {i j} → sym1 {_} {_} {i} {j} ; - trans = λ {i j k} → trans1 {_} {_} {i} {j} {k} } + record { isEquivalence = record {refl = ≈-Reasoning.refl-hom B + ; sym = λ {i j} → sym1 {_} {_} {i} {j} + ; trans = λ {i j k} → trans1 {_} {_} {i} {j} {k} } ; identityL = IsCategory.identityL ( Category.isCategory B ) ; identityR = IsCategory.identityR ( Category.isCategory B ) ; o-resp-≈ = λ{a b c f g h i } → o-resp-≈1 {a} {b} {c} {f} {g} {h} {i} ; associative = IsCategory.associative ( Category.isCategory B ) } where sym1 : {a b : CObj A B } {i j : CHom A B a b } → i == j → j == i - sym1 {a} {b} {i} {j} eq {x} = let open ≈-Reasoning B in begin - TMap j x - ≈⟨ sym eq ⟩ - TMap i x - ∎ + sym1 {a} {b} {i} {j} eq {x} = ≈-Reasoning.sym B eq trans1 : {a b : CObj A B } {i j k : CHom A B a b} → i == j → j == k → i == k trans1 {a} {b} {i} {j} {k} i=j j=k {x} = let open ≈-Reasoning B in begin TMap i x diff -r eb62812b5885 -r 6aa6cbf630a0 src/equalizer.agda --- a/src/equalizer.agda Fri Feb 19 12:09:48 2021 +0900 +++ b/src/equalizer.agda Sun Feb 21 03:34:36 2021 +0900 @@ -1,4 +1,3 @@ -{-# OPTIONS --allow-unsolved-metas #-} --- -- -- Equalizer @@ -21,18 +20,6 @@ open import HomReasoning open import cat-utility --- in cat-utility --- record Equalizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {c a b : Obj A} (e : Hom A c a) (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where --- field --- fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] --- k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c --- ek=h : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → A [ A [ e o k {d} h eq ] ≈ h ] --- uniqueness : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → {k' : Hom A d c } → --- A [ A [ e o k' ] ≈ h ] → A [ k {d} h eq ≈ k' ] --- equalizer : Hom A c a --- equalizer = e - - -- -- Burroni's Flat Equational Definition of Equalizer -- @@ -56,6 +43,20 @@ β : { d a b : Obj A} → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) → Hom A d c β {d} {a} {b} f g h = A [ γ {a} {b} {c} f g h o δ {d} {b} {d} (id1 A d) (A [ f o h ]) ] +record Burroni' { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A} (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where + field + equ : {a b : Obj A } → (f g : Hom A a b) → Obj A + α : {a b : Obj A } → (f g : Hom A a b) → Hom A (equ f g) a + γ : {a b d : Obj A } → (f g : Hom A a b) → (h : Hom A d a ) → Hom A (equ (A [ f o h ]) (A [ g o h ])) (equ f g) + δ : {a b : Obj A } → (f g : Hom A a b) → A [ f ≈ g ] → Hom A a (equ f g) + b1 : A [ A [ f o α f g ] ≈ A [ g o α f g ] ] + b1k : {d : Obj A } {k : Hom A d (equ f g)} → A [ A [ f o A [ α f g o k ] ] ≈ A [ g o A [ α f g o k ] ] ] + b1k {d} {k} = ≈-Reasoning.trans-hom A (≈-Reasoning.assoc A) (≈-Reasoning.trans-hom A (≈-Reasoning.car A b1) (≈-Reasoning.sym A (≈-Reasoning.assoc A))) + field + b2 : {d : Obj A } → {h : Hom A d a } → A [ A [ ( α f g ) o (γ f g h) ] ≈ A [ h o α (A [ f o h ]) (A [ g o h ]) ] ] + b3 : {d : Obj A} → {h : Hom A d a } → A [ A [ α f f o δ f f (≈-Reasoning.refl-hom A) ] ≈ id1 A a ] + b4 : {d : Obj A } {h : Hom A d a } {k : Hom A d (equ f g)} → + A [ A [ γ f g ( A [ α f g o k ] ) o ( δ (A [ f o A [ α f g o k ] ] ) (A [ g o A [ α f g o k ] ] ) b1k )] ≈ k ] open Equalizer open IsEqualizer @@ -98,10 +99,10 @@ -- || -- d -monic : { a b d : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A f g) - → ( i j : Hom A d (equalizer-c eqa) ) +monoic : { c a b d : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A f g) + → { i j : Hom A d (equalizer-c eqa) } → A [ A [ equalizer eqa o i ] ≈ A [ equalizer eqa o j ] ] → A [ i ≈ j ] -monic {a} {b} {d} {f} {g} eqa i j ei=ej = let open ≈-Reasoning (A) in begin +monoic {c} {a} {b} {d} {f} {g} eqa {i} {j} ei=ej = let open ≈-Reasoning (A) in begin i ≈↑⟨ uniqueness (isEqualizer eqa) ( begin equalizer eqa o i @@ -238,6 +239,22 @@ -- c-iso-rl is obvious from the symmetry +-- +-- we cannot have equalizer ≈ id. we only have Iso A (equalizer-c equ) a +-- +equ-ff : {a b : Obj A} → (f : Hom A a b ) → IsEqualizer A (id1 A a) f f +equ-ff {a} {b} f = record { + fe=ge = ≈-Reasoning.refl-hom A ; + k = λ {d} h eq → h ; + ek=h = λ {d} {h} {eq} → ≈-Reasoning.idL A ; + uniqueness = λ {d} {h} {eq} {k'} ek=h → begin + h + ≈↑⟨ ek=h ⟩ + id1 A a o k' + ≈⟨ idL ⟩ + k' + ∎ + } where open ≈-Reasoning A -------------------------------- @@ -247,25 +264,26 @@ -- ---- -lemma-equ1 : {a b c : Obj A} (f g : Hom A a b) → (e : Hom A c a ) → - ( eqa-e : {a b c : Obj A} → (f g : Hom A a b) → Hom A c a ) - ( eqa : {a b c : Obj A} → (f g : Hom A a b) → IsEqualizer A (eqa-e f g) f g ) - → Burroni A {c} {a} {b} f g e -lemma-equ1 {a} {b} {c} f g e eqa-e eqa = record { - α = λ {a} {b} {c} f g e → equalizer1 (eqa {a} {b} {c} f g ) ; -- Hom A c a -- eqa-e f g - γ = λ {a} {b} {c} {d} f g h → k (eqa {a} {b} {c} f g ) {d} ( A [ h o (equalizer1 ( eqa (A [ f o h ] ) (A [ g o h ] ))) ] ) +lemma-equ1 : {a b c : Obj A} (f g : Hom A a b) + → ( eqa-e : {a b c : Obj A} → (f g : Hom A a b) → Hom A c a ) + → ( eqa : {a b c : Obj A} → (f g : Hom A a b) → IsEqualizer A (eqa-e f g) f g ) + → Burroni A {c} {a} {b} f g (eqa-e f g) +lemma-equ1 {a} {b} {c} f g eqa-e eqa = record { + α = λ {a} {b} {c} f g e → equalizer1 (eqa {a} {b} {c} f g ) ; -- Hom A c a + γ = λ {a} {b} {c} {d} f g h → k (eqa {a} {b} {c} f g ) {d} ( A [ h o (equalizer1 ( eqa (A [ f o h ] ) (A [ g o h ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h ) ; -- Hom A c d - δ = λ {a} {b} {c} e f → k (eqa {a} {b} {c} f f ) {a} (id1 A a) (f1=f1 f); -- Hom A a c + δ = λ {a} {b} {c} e f → k (eqa {a} {b} {c} f f ) {a} (id1 A a) (f1=f1 f); -- Hom A a c cong-α = λ {a b c e f g g'} eq → cong-α1 {a} {b} {c} {e} {f} {g} {g'} eq ; cong-γ = λ {a} {_} {c} {d} {f} {g} {h} {h'} eq → cong-γ1 {a} {c} {d} {f} {g} {h} {h'} eq ; - cong-δ = λ {a b c e f f'} f=f' → cong-δ1 {a} {b} {c} {e} {f} {f'} f=f' ; + cong-δ = λ {a b c e f f'} f=f' → cong-δ1 {a} {b} {c} {f} {f'} f=f' ; b1 = fe=ge (eqa {a} {b} {c} f g ) ; b2 = λ {d} {h} → lemma-b2 {d} {h}; b3 = lemma-b3 ; b4 = lemma-b4 } where -- - -- e eqa f g f -- c ---------→ a ------→b + -- e eqa f g f + -- c ---------→ a ------→b -- ^ g -- | -- |k₁ = e eqa (f o (e (eqa f g))) (g o (e (eqa f g)))) @@ -295,23 +313,45 @@ g o ( h o equalizer1 (eqa (f o h) ( g o h ))) ∎ cong-α1 : {a b c : Obj A } → { e : Hom A c a } - → {f g g' : Hom A a b } → A [ g ≈ g' ] → A [ equalizer1 (eqa {a} {b} {c} f g )≈ equalizer1 (eqa {a} {b} {c} f g' ) ] - cong-α1 {a} {b} {c} {e} {f} {g} {g'} eq = {!!} -- let open ≈-Reasoning (A) in refl-hom - cong-γ1 : {a c d : Obj A } → {f g : Hom A a b} {h h' : Hom A d a } → A [ h ≈ h' ] → - A [ k (eqa f g ) {d} ( A [ h o (equalizer1 ( eqa (A [ f o h ] ) (A [ g o h ] ) )) ] ) (lemma-equ4 {a} {b} {c} {d} f g h ) - ≈ k (eqa f g ) {d} ( A [ h' o (equalizer1 ( eqa (A [ f o h' ] ) (A [ g o h' ] ) )) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' ) ] + → {f g g' : Hom A a b } → A [ g ≈ g' ] → A [ equalizer1 (eqa {a} {b} {c} f g ) ≈ equalizer1 (eqa {a} {b} {c} f g' ) ] + cong-α1 {a} {b} {c} {e} {f} {g} {g'} eq = begin + equalizer1 (eqa f g) + ≈↑⟨ ek=h (eqa f g') ⟩ + equalizer1 (eqa f g') o k (eqa f g') (eqa-e f g) {!!} + ≈⟨ cdr ( uniqueness (eqa f g') {!!}) ⟩ + equalizer1 (eqa f g') o id1 A c + ≈⟨ idR ⟩ + equalizer1 (eqa f g') + ∎ where open ≈-Reasoning (A) + cong-γ1 : {a c d : Obj A } → {f g : Hom A a b} {h h' : Hom A d a } → A [ h ≈ h' ] → + A [ k (eqa f g ) {d} ( A [ h o (equalizer1 ( eqa (A [ f o h ] ) (A [ g o h ] ) )) ] ) (lemma-equ4 {a} {b} {c} {d} f g h ) + ≈ k (eqa f g ) {d} ( A [ h' o (equalizer1 ( eqa (A [ f o h' ] ) (A [ g o h' ] ) )) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' ) ] cong-γ1 {a} {c} {d} {f} {g} {h} {h'} h=h' = let open ≈-Reasoning (A) in begin k (eqa f g ) {d} ( A [ h o (equalizer1 ( eqa (A [ f o h ] ) (A [ g o h ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h ) - ≈⟨ uniqueness (eqa f g) {!!} ⟩ + ≈⟨ {!!} ⟩ + k (eqa f g) (A [ h o (eqa-e (A [ f o h' ]) (A [ g o h' ])) ] ) {!!} + ≈⟨ uniqueness (eqa f g) ( begin + eqa-e f g o k (eqa f g ) {d} ( A [ h' o (equalizer1 ( eqa (A [ f o h' ] ) (A [ g o h' ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' ) + ≈⟨ ek=h (eqa f g ) ⟩ + h' o (equalizer1 ( eqa (A [ f o h' ] ) (A [ g o h' ] ))) + ≈↑⟨ car h=h' ⟩ + h o (equalizer1 ( eqa (A [ f o h' ] ) (A [ g o h' ] ))) + ∎ )⟩ k (eqa f g ) {d} ( A [ h' o (equalizer1 ( eqa (A [ f o h' ] ) (A [ g o h' ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' ) ∎ - cong-δ1 : {a b c : Obj A} {e : Hom A c a } {f f' : Hom A a b} → A [ f ≈ f' ] → A [ k (eqa {a} {b} {c} f f ) (id1 A a) (f1=f1 f) ≈ - k (eqa {a} {b} {c} f' f' ) (id1 A a) (f1=f1 f') ] - cong-δ1 {a} {b} {c} {e} {f} {f'} f=f' = let open ≈-Reasoning (A) in + cong-δ1 : {a b c : Obj A} {f f' : Hom A a b} → A [ f ≈ f' ] → A [ k (eqa {a} {b} {c} f f ) (id1 A a) (f1=f1 f) ≈ + k (eqa {a} {b} {c} f' f' ) (id1 A a) (f1=f1 f') ] + cong-δ1 {a} {b} {c} {f} {f'} f=f' = let open ≈-Reasoning (A) in begin - k (eqa {a} {b} {c} f f ) (id a) (f1=f1 f) - ≈⟨ uniqueness (eqa f f) {!!} ⟩ - k (eqa {a} {b} {c} f' f' ) (id a) (f1=f1 f') + k (eqa {a} {b} {c} f f ) (id a) (f1=f1 f) + ≈⟨ uniqueness (eqa f f) ( begin + eqa-e f f o k (eqa {a} {b} {c} f' f' ) (id a) (f1=f1 f') + ≈⟨ {!!} ⟩ -- ≈⟨ ek=h (eqa {a} {b} {c} f' f' ) ⟩ + eqa-e f' f' o k (eqa {a} {b} {c} f' f' ) (id a) (f1=f1 f') + ≈⟨ ek=h (eqa {a} {b} {c} f' f' ) ⟩ + id a + ∎ )⟩ + k (eqa {a} {b} {c} f' f' ) (id a) (f1=f1 f') ∎ lemma-b2 : {d : Obj A} {h : Hom A d a} → A [ @@ -341,7 +381,7 @@ ≈↑⟨ idR ⟩ (equalizer1 (eqa f g) o j ) o id d ≈⟨ {!!} ⟩ -- here we decide e (fej) (gej)' is id d - {!!} + ((equalizer1 (eqa f g) o j) o equalizer1 (eqa (f o equalizer1 (eqa f g ) o j) (g o equalizer1 (eqa f g ) o j))) ∎ ))) ⟩ j o k (eqa (( f o ( equalizer1 (eqa f g) o j ) )) (( f o ( equalizer1 (eqa f g) o j ) ))) (id1 A d) (f1=f1 (( f o ( equalizer1 (eqa f g) o j ) ))) ≈⟨ cdr ((uniqueness (eqa (( f o ( equalizer1 (eqa f g) o j ) )) (( f o ( equalizer1 (eqa f g) o j ) ))) ( begin @@ -349,7 +389,7 @@ ≈⟨ idR ⟩ equalizer1 (eqa (f o equalizer1 (eqa f g ) o j) (f o equalizer1 (eqa f g ) o j)) ≈⟨ {!!} ⟩ -- here we decide e (fej) (fej)' is id d - {!!} + id d ∎ ))) ⟩ j o id d ≈⟨ idR ⟩ @@ -384,9 +424,9 @@ ≈⟨ car (b2 bur) ⟩ ( h o ( α bur ( f o h ) ( g o h ) (id d))) o δ bur {d} {b} {d} (id d) (f o h) ≈↑⟨ assoc ⟩ - h o ((( α bur ( f o h ) ( g o h ) (id d) )) o δ bur {d} {b} {d} (id d) (f o h) ) - ≈↑⟨ cdr ( car ( cong-α bur eq)) ⟩ - h o ((( α bur ( f o h ) ( f o h ) (id d)))o δ bur {d} {b} {d} (id d) (f o h) ) + h o ((( α bur ( f o h ) ( g o h ) (id d ))) o δ bur {d} {b} {d} (id d) (f o h) ) + ≈⟨ {!!} ⟩ + h o ((( α bur ( f o h ) ( f o h ) (id d ))) o δ bur {d} {b} {d} (id d) (f o h) ) ≈⟨ cdr (b3 bur {d} {b} {d} (f o h) {id d} ) ⟩ h o id d ≈⟨ idR ⟩