Mercurial > hg > Members > kono > Proof > category
changeset 1035:b6dbec7e535b
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 02 Apr 2021 02:48:12 +0900 |
| parents | 40c39d3e6a75 |
| children | b836c3dc7a29 |
| files | src/ToposEx.agda src/cat-utility.agda src/freyd2.agda |
| diffstat | 3 files changed, 102 insertions(+), 84 deletions(-) [+] |
line wrap: on
line diff
--- a/src/ToposEx.agda Wed Mar 31 15:58:02 2021 +0900 +++ b/src/ToposEx.agda Fri Apr 02 02:48:12 2021 +0900 @@ -115,7 +115,7 @@ -- -- --- Hom equality and Ω +-- Hom equality and Ω (p.94 cl(Δ a) in Takeuchi ) -- -- -- a -----------→ + @@ -319,19 +319,42 @@ < (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 π))) ∎ --- --- open Functor --- open import Category.Sets --- open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym) --- record SubObjectFuntor : Set ( suc (suc c₁ ) ⊔ suc (suc c₂) ⊔ suc ℓ ) where --- field --- Sub : Functor A (Sets {c₂}) --- smonic : Mono A {!!} --- --- open SubObjectFuntor --- postulate ≡←≈ : {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y --- sub→topos : (Ω : Obj A) → (S : SubObjectFuntor) → Representable A ≡←≈ (Sub S) Ω → Topos A c --- sub→topos Ω S R = record { + +-- open Functor +-- open import Category.Sets +-- open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym) +-- +-- record SubObject (a : Obj A) : Set (c₁ ⊔ c₂ ⊔ ℓ) where +-- field +-- sb : Obj A +-- sm : Hom A sb a +-- smono : Mono A sm +-- +-- postulate +-- S : (a : Set (c₁ ⊔ c₂ ⊔ ℓ)) → Set c₂ +-- solv← : (x : Obj A) → S (SubObject x) → SubObject x +-- solv→ : (x : Obj A) → SubObject x → S (SubObject x) +-- -- soiso← : (x : Set (c₁ ⊔ c₂ ⊔ ℓ)) → solv← (solv→ x) ≡ x +-- -- soiso→ : (x : Set c₂ ) → solv→ (solv← x) ≡ x +-- ≡←≈ : {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y +-- open SubObject +-- +-- smap : {x y : Obj A} → Hom A y x → SubObject x → SubObject y +-- smap h s = record { sb = sb s ; sm = A [ {!!} o sm s ] ; smono = record { isMono = λ f g eq → Mono.isMono (smono s) f g {!!} } } +-- -- A [ A [ A [ h o (sm s) ] o f ] ≈ A [ A [ h o (sm s) ] o g ] → A [ A [ sm s o f ] ≈ A [ sm s o g ] ] +-- +-- Smap : {x y : Obj A} → Hom A y x → Hom Sets (S (SubObject x)) (S (SubObject y)) +-- Smap {x} {y} h s = solv→ y (smap h (solv← x s)) +-- +-- SubObjectFuntor : Functor (Category.op A) (Sets {c₂}) +-- SubObjectFuntor = record { +-- FObj = λ x → S (SubObject x) +-- ; FMap = Smap +-- ; isFunctor = {!!} +-- } +-- +-- sub→topos : (Ω : Obj A) → Representable A ≡←≈ SubObjectFuntor Ω → Topos A c +-- sub→topos Ω R = record { -- Ω = Ω -- ; ⊤ = {!!} -- ; Ker = {!!} @@ -341,16 +364,15 @@ -- ; ker-m = {!!} -- } } -- --- topos→sub : (t : Topos A c ) → SubObjectFuntor --- topos→sub t = record { --- Sub = record { --- FObj = {!!} --- ; FMap = {!!} --- ; isFunctor = {!!} --- } ; smonic = {!!} --- } --- --- topos→rep : (t : Topos A c ) → Representable A ≡←≈ (Sub (topos→sub t)) (Topos.Ω t) --- topos→rep t = {!!} +-- topos→rep : (t : Topos A c ) → Representable A ≡←≈ SubObjectFuntor (Topos.Ω t) +-- topos→rep t = record { +-- repr→ = record { TMap = λ a Sa → Topos.char t (sm (solv← a Sa)) (smono (solv← a Sa)) ; isNTrans = record { commute = {!!} } } -- Hom A a Ω +-- ; repr← = record { TMap = λ a h → solv→ a record {sb = equalizer-c (Ker t h) ; sm = equalizer (Ker t h) ; smono = +-- {!!} } ; isNTrans = {!!} } -- FObj (Sub S) a +-- ; reprId→ = {!!} +-- ; reprId← = {!!} +-- } -- -- +-- +--
--- a/src/cat-utility.agda Wed Mar 31 15:58:02 2021 +0900 +++ b/src/cat-utility.agda Fri Apr 02 02:48:12 2021 +0900 @@ -534,37 +534,37 @@ postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂ Yoneda : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( ≡←≈ : {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y ) - (a : Obj A) → Functor A (Sets {c₂}) + (a : Obj A) → Functor (Category.op A) (Sets {c₂}) Yoneda {c₁} {c₂} {ℓ} A ≡←≈ a = record { - FObj = λ b → Hom A a b - ; FMap = λ {x} {y} (f : Hom A x y ) → λ ( g : Hom A a x ) → A [ f o g ] -- f : Hom A x y → Hom Sets (Hom A a x ) (Hom A a y) + FObj = λ b → Hom (Category.op A) a b + ; FMap = λ {x} {y} (f : Hom A y x ) → λ ( g : Hom A x a ) → (Category.op A) [ f o g ] -- f : Hom A x y → Hom Sets (Hom A a x ) (Hom A a y) ; isFunctor = record { - identity = λ {b} → extensionality A ( λ x → lemma-y-obj1 {b} x ) ; + identity = λ {b} → extensionality (Category.op A) ( λ x → lemma-y-obj1 {b} x ) ; distr = λ {a} {b} {c} {f} {g} → extensionality A ( λ x → lemma-y-obj2 a b c f g x ) ; - ≈-cong = λ eq → extensionality A ( λ x → lemma-y-obj3 x eq ) + ≈-cong = λ eq → extensionality (Category.op A) ( λ x → lemma-y-obj3 x eq ) } } where - lemma-y-obj1 : {b : Obj A } → (x : Hom A a b) → A [ id1 A b o x ] ≡ x - lemma-y-obj1 {b} x = let open ≈-Reasoning A in ≡←≈ idL - lemma-y-obj2 : (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c ) → (x : Hom A a a₁ )→ - A [ A [ g o f ] o x ] ≡ (Sets [ _[_o_] A g o _[_o_] A f ]) x - lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning A in ≡←≈ ( sym assoc ) - lemma-y-obj3 : {b c : Obj A} {f g : Hom A b c } → (x : Hom A a b ) → A [ f ≈ g ] → A [ f o x ] ≡ A [ g o x ] - lemma-y-obj3 {_} {_} {f} {g} x eq = let open ≈-Reasoning A in ≡←≈ ( resp refl-hom eq ) + lemma-y-obj1 : {b : Obj A } → (x : Hom A b a) → (Category.op A) [ id1 A b o x ] ≡ x + lemma-y-obj1 {b} x = let open ≈-Reasoning (Category.op A) in ≡←≈ idL + lemma-y-obj2 : (a₁ b c : Obj A) (f : Hom A b a₁) (g : Hom A c b ) → (x : Hom A a₁ a )→ + (Category.op A) [ (Category.op A) [ g o f ] o x ] ≡ (Sets [ _[_o_] (Category.op A) g o _[_o_] (Category.op A) f ]) x + lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning (Category.op A) in ≡←≈ ( sym assoc ) + lemma-y-obj3 : {b c : Obj A} {f g : Hom A c b } → (x : Hom A b a ) → (Category.op A) [ f ≈ g ] → (Category.op A) [ f o x ] ≡ (Category.op A) [ g o x ] + lemma-y-obj3 {_} {_} {f} {g} x eq = let open ≈-Reasoning (Category.op A) in ≡←≈ ( resp refl-hom eq ) -- Representable U ≈ Hom(A,-) record Representable { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) - ( ≡←≈ : {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y ) - ( U : Functor A (Sets {c₂}) ) (a : Obj A) : Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ )) where + ( ≡←≈ : {a b : Obj A } { x y : Hom A b a } → (x≈y : (Category.op A) [ x ≈ y ]) → x ≡ y ) + ( U : Functor (Category.op A) (Sets {c₂}) ) (a : Obj A) : Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ )) where field -- FObj U x : A → Set -- FMap U f = Set → Set (locally small) -- λ b → Hom (a,b) : A → Set -- λ f → Hom (a,-) = λ b → Hom a b - repr→ : NTrans A (Sets {c₂}) U (Yoneda A ≡←≈ a ) - repr← : NTrans A (Sets {c₂}) (Yoneda A ≡←≈ a) U + repr→ : NTrans (Category.op A) (Sets {c₂}) U (Yoneda A ≡←≈ a ) + repr← : NTrans (Category.op A) (Sets {c₂}) (Yoneda A ≡←≈ a) U reprId→ : {x : Obj A} → Sets [ Sets [ TMap repr→ x o TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (Yoneda A ≡←≈ a) x )] reprId← : {x : Obj A} → Sets [ Sets [ TMap repr← x o TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)]
--- a/src/freyd2.agda Wed Mar 31 15:58:02 2021 +0900 +++ b/src/freyd2.agda Fri Apr 02 02:48:12 2021 +0900 @@ -6,7 +6,7 @@ where open import HomReasoning -open import cat-utility hiding (Yoneda) +open import cat-utility hiding (Yoneda ; Representable ) open import Relation.Binary.Core open import Function @@ -24,10 +24,6 @@ -- A is localy small postulate ≡←≈ : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y -Yoneda : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Functor A (Sets {c₂}) -Yoneda {c₁} {c₂} {ℓ} A a = cat-utility.Yoneda A (≡←≈ A) a - - import Axiom.Extensionality.Propositional -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x ) -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂ @@ -44,47 +40,47 @@ open IsLimit open import Category.Cat --- Yoneda : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Functor A (Sets {c₂}) --- Yoneda {c₁} {c₂} {ℓ} A a = record { --- FObj = λ b → Hom A a b --- ; FMap = λ {x} {y} (f : Hom A x y ) → λ ( g : Hom A a x ) → A [ f o g ] -- f : Hom A x y → Hom Sets (Hom A a x ) (Hom A a y) --- ; isFunctor = record { --- identity = λ {b} → extensionality A ( λ x → lemma-y-obj1 {b} x ) ; --- distr = λ {a} {b} {c} {f} {g} → extensionality A ( λ x → lemma-y-obj2 a b c f g x ) ; --- ≈-cong = λ eq → extensionality A ( λ x → lemma-y-obj3 x eq ) --- } --- } where --- lemma-y-obj1 : {b : Obj A } → (x : Hom A a b) → A [ id1 A b o x ] ≡ x --- lemma-y-obj1 {b} x = let open ≈-Reasoning A in ≡←≈ A idL --- lemma-y-obj2 : (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c ) → (x : Hom A a a₁ )→ --- A [ A [ g o f ] o x ] ≡ (Sets [ _[_o_] A g o _[_o_] A f ]) x --- lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning A in ≡←≈ A ( begin --- A [ A [ g o f ] o x ] --- ≈↑⟨ assoc ⟩ --- A [ g o A [ f o x ] ] --- ≈⟨⟩ --- ( λ x → A [ g o x ] ) ( ( λ x → A [ f o x ] ) x ) --- ∎ ) --- lemma-y-obj3 : {b c : Obj A} {f g : Hom A b c } → (x : Hom A a b ) → A [ f ≈ g ] → A [ f o x ] ≡ A [ g o x ] --- lemma-y-obj3 {_} {_} {f} {g} x eq = let open ≈-Reasoning A in ≡←≈ A ( begin --- A [ f o x ] --- ≈⟨ resp refl-hom eq ⟩ --- A [ g o x ] --- ∎ ) +Yoneda : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Functor A (Sets {c₂}) +Yoneda {c₁} {c₂} {ℓ} A a = record { + FObj = λ b → Hom A a b + ; FMap = λ {x} {y} (f : Hom A x y ) → λ ( g : Hom A a x ) → A [ f o g ] -- f : Hom A x y → Hom Sets (Hom A a x ) (Hom A a y) + ; isFunctor = record { + identity = λ {b} → extensionality A ( λ x → lemma-y-obj1 {b} x ) ; + distr = λ {a} {b} {c} {f} {g} → extensionality A ( λ x → lemma-y-obj2 a b c f g x ) ; + ≈-cong = λ eq → extensionality A ( λ x → lemma-y-obj3 x eq ) + } + } where + lemma-y-obj1 : {b : Obj A } → (x : Hom A a b) → A [ id1 A b o x ] ≡ x + lemma-y-obj1 {b} x = let open ≈-Reasoning A in ≡←≈ A idL + lemma-y-obj2 : (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c ) → (x : Hom A a a₁ )→ + A [ A [ g o f ] o x ] ≡ (Sets [ _[_o_] A g o _[_o_] A f ]) x + lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning A in ≡←≈ A ( begin + A [ A [ g o f ] o x ] + ≈↑⟨ assoc ⟩ + A [ g o A [ f o x ] ] + ≈⟨⟩ + ( λ x → A [ g o x ] ) ( ( λ x → A [ f o x ] ) x ) + ∎ ) + lemma-y-obj3 : {b c : Obj A} {f g : Hom A b c } → (x : Hom A a b ) → A [ f ≈ g ] → A [ f o x ] ≡ A [ g o x ] + lemma-y-obj3 {_} {_} {f} {g} x eq = let open ≈-Reasoning A in ≡←≈ A ( begin + A [ f o x ] + ≈⟨ resp refl-hom eq ⟩ + A [ g o x ] + ∎ ) -- -- Representable U ≈ Hom(A,-) --- record Representable { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( U : Functor A (Sets {c₂}) ) (a : Obj A) : Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ )) where --- field --- -- FObj U x : A → Set --- -- FMap U f = Set → Set (locally small) --- -- λ b → Hom (a,b) : A → Set --- -- λ f → Hom (a,-) = λ b → Hom a b +record Representable { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( U : Functor A (Sets {c₂}) ) (a : Obj A) : Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ )) where + field + -- FObj U x : A → Set + -- FMap U f = Set → Set (locally small) + -- λ b → Hom (a,b) : A → Set + -- λ f → Hom (a,-) = λ b → Hom a b --- repr→ : NTrans A (Sets {c₂}) U (Yoneda A a ) --- repr← : NTrans A (Sets {c₂}) (Yoneda A a) U --- reprId→ : {x : Obj A} → Sets [ Sets [ TMap repr→ x o TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (Yoneda A a) x )] --- reprId← : {x : Obj A} → Sets [ Sets [ TMap repr← x o TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)] + repr→ : NTrans A (Sets {c₂}) U (Yoneda A a ) + repr← : NTrans A (Sets {c₂}) (Yoneda A a) U + reprId→ : {x : Obj A} → Sets [ Sets [ TMap repr→ x o TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (Yoneda A a) x )] + reprId← : {x : Obj A} → Sets [ Sets [ TMap repr← x o TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)] open Representable @@ -285,7 +281,7 @@ (U : Functor A (Sets {c₂}) ) ( i : Obj ( K A Sets * ↓ U) ) (In : HasInitialObject ( K A Sets * ↓ U) i ) - → Representable A (≡←≈ A) U (obj i) + → Representable A U (obj i) UisRepresentable A U i In = record { repr→ = record { TMap = tmap1 ; isNTrans = record { commute = comm1 } } ; repr← = record { TMap = tmap2 ; isNTrans = record { commute = comm2 } }