Mercurial > hg > Members > kono > Proof > category
changeset 999:d89f2c8cf0f4
separate CCCSets
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 08 Mar 2021 08:25:30 +0900 |
| parents | 98f412058488 |
| children | 3ef1b472e9f9 |
| files | src/CCCGraph.agda src/CCCSets.agda src/SetsCompleteness.agda src/cat-utility.agda |
| diffstat | 4 files changed, 367 insertions(+), 301 deletions(-) [+] |
line wrap: on
line diff
--- a/src/CCCGraph.agda Sun Mar 07 15:57:49 2021 +0900 +++ b/src/CCCGraph.agda Mon Mar 08 08:25:30 2021 +0900 @@ -17,258 +17,10 @@ open import Category.Sets --- Sets is a CCC - import Axiom.Extensionality.Propositional postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂ -data One {c : Level } : Set c where - OneObj : One -- () in Haskell ( or any one object set ) - -sets : {c : Level } → CCC (Sets {c}) -sets = record { - １ = One - ; ○ = λ _ → λ _ → OneObj - ; _∧_ = _∧_ - ; <_,_> = <,> - ; π = π - ; π' = π' - ; _<=_ = _<=_ - ; _* = _* - ; ε = ε - ; isCCC = isCCC - } where - １ : Obj Sets - １ = One - ○ : (a : Obj Sets ) → Hom Sets a １ - ○ a = λ _ → OneObj - _∧_ : Obj Sets → Obj Sets → Obj Sets - _∧_ a b = a /\ b - <,> : {a b c : Obj Sets } → Hom Sets c a → Hom Sets c b → Hom Sets c ( a ∧ b) - <,> f g = λ x → ( f x , g x ) - π : {a b : Obj Sets } → Hom Sets (a ∧ b) a - π {a} {b} = proj₁ - π' : {a b : Obj Sets } → Hom Sets (a ∧ b) b - π' {a} {b} = proj₂ - _<=_ : (a b : Obj Sets ) → Obj Sets - a <= b = b → a - _* : {a b c : Obj Sets } → Hom Sets (a ∧ b) c → Hom Sets a (c <= b) - f * = λ x → λ y → f ( x , y ) - ε : {a b : Obj Sets } → Hom Sets ((a <= b ) ∧ b) a - ε {a} {b} = λ x → ( proj₁ x ) ( proj₂ x ) - isCCC : CCC.IsCCC Sets １ ○ _∧_ <,> π π' _<=_ _* ε - isCCC = record { - e2 = e2 - ; e3a = λ {a} {b} {c} {f} {g} → e3a {a} {b} {c} {f} {g} - ; e3b = λ {a} {b} {c} {f} {g} → e3b {a} {b} {c} {f} {g} - ; e3c = e3c - ; π-cong = π-cong - ; e4a = e4a - ; e4b = e4b - ; *-cong = *-cong - } where - e2 : {a : Obj Sets} {f : Hom Sets a １} → Sets [ f ≈ ○ a ] - e2 {a} {f} = extensionality Sets ( λ x → e20 x ) - where - e20 : (x : a ) → f x ≡ ○ a x - e20 x with f x - e20 x | OneObj = refl - e3a : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} → - Sets [ ( Sets [ π o ( <,> f g) ] ) ≈ f ] - e3a = refl - e3b : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} → - Sets [ Sets [ π' o ( <,> f g ) ] ≈ g ] - e3b = refl - e3c : {a b c : Obj Sets} {h : Hom Sets c (a ∧ b)} → - Sets [ <,> (Sets [ π o h ]) (Sets [ π' o h ]) ≈ h ] - e3c = refl - π-cong : {a b c : Obj Sets} {f f' : Hom Sets c a} {g g' : Hom Sets c b} → - Sets [ f ≈ f' ] → Sets [ g ≈ g' ] → Sets [ <,> f g ≈ <,> f' g' ] - π-cong refl refl = refl - e4a : {a b c : Obj Sets} {h : Hom Sets (c ∧ b) a} → - Sets [ Sets [ ε o <,> (Sets [ h * o π ]) π' ] ≈ h ] - e4a = refl - e4b : {a b c : Obj Sets} {k : Hom Sets c (a <= b)} → - Sets [ (Sets [ ε o <,> (Sets [ k o π ]) π' ]) * ≈ k ] - e4b = refl - *-cong : {a b c : Obj Sets} {f f' : Hom Sets (a ∧ b) c} → - Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ] - *-cong refl = refl - --- ○ b --- b -----------→ 1 --- | | --- m | | ⊤ --- ↓ char m ↓ --- a -----------→ Ω --- h - -data II {c : Level } : Set c where - true : II - false : II - -data Tker {c : Level} {a : Set c} ( f : a → II {c} ) : Set c where - isTrue : (x : a ) → f x ≡ true → Tker f - -topos : {c : Level } → Topos (Sets {c}) sets -topos = record { - Ω = II - ; ⊤ = λ _ → true - ; Ker = tker - ; char = tchar - ; isTopos = record { - char-uniqueness = {!!} - ; ker-iso = {!!} - } - } where - etker : {a : Obj Sets} (h : Hom Sets a II) → Hom Sets ( Tker h ) a - etker h (isTrue x eq) = x - e-eq : {a : Obj Sets} (h : Hom Sets a II) → Sets [ Sets [ h o etker h ] ≈ Sets [ Sets [ (λ _ → true) o CCC.○ sets a ] o etker h ] ] - e-eq h = {!!} - tker : {a : Obj Sets} (h : Hom Sets a II) → Equalizer Sets h (Sets [ (λ _ → true) o CCC.○ sets a ]) - tker {a} h = record { - equalizer-c = Tker h - ; equalizer = etker h - ; isEqualizer = record { - fe=ge = e-eq h - ; k = {!!} - ; ek=h = {!!} - ; uniqueness = {!!} - } - } - tchar : {a b : Obj Sets} (m : Hom Sets b a) → Mono Sets m → Hom Sets a II - tchar {a} {b} m mono x = true - - - -open import graph -module ccc-from-graph {c₁ c₂ : Level } (G : Graph {c₁} {c₂}) where - - open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] ) - open Graph - - V = vertex G - E : V → V → Set c₂ - E = edge G - - data Objs : Set c₁ where - atom : V → Objs - ⊤ : Objs - _∧_ : Objs → Objs → Objs - _<=_ : Objs → Objs → Objs - - data Arrows : (b c : Objs ) → Set (c₁ ⊔ c₂) - data Arrow : Objs → Objs → Set (c₁ ⊔ c₂) where --- case i - arrow : {a b : V} → E a b → Arrow (atom a) (atom b) - π : {a b : Objs } → Arrow ( a ∧ b ) a - π' : {a b : Objs } → Arrow ( a ∧ b ) b - ε : {a b : Objs } → Arrow ((a <= b) ∧ b ) a - _* : {a b c : Objs } → Arrows (c ∧ b ) a → Arrow c ( a <= b ) --- case v - - data Arrows where - id : ( a : Objs ) → Arrows a a --- case i - ○ : ( a : Objs ) → Arrows a ⊤ --- case i - <_,_> : {a b c : Objs } → Arrows c a → Arrows c b → Arrows c (a ∧ b) -- case iii - iv : {b c d : Objs } ( f : Arrow d c ) ( g : Arrows b d ) → Arrows b c -- cas iv - - _・_ : {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c - id a ・ g = g - ○ a ・ g = ○ _ - < f , g > ・ h = < f ・ h , g ・ h > - iv f g ・ h = iv f ( g ・ h ) - - - identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) ≡ f - identityL = refl - - identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) ≡ f - identityR {a} {a} {id a} = refl - identityR {a} {⊤} {○ a} = refl - identityR {a} {_} {< f , f₁ >} = cong₂ (λ j k → < j , k > ) identityR identityR - identityR {a} {b} {iv f g} = cong (λ k → iv f k ) identityR - - assoc≡ : {a b c d : Objs} (f : Arrows c d) (g : Arrows b c) (h : Arrows a b) → - (f ・ (g ・ h)) ≡ ((f ・ g) ・ h) - assoc≡ (id a) g h = refl - assoc≡ (○ a) g h = refl - assoc≡ < f , f₁ > g h = cong₂ (λ j k → < j , k > ) (assoc≡ f g h) (assoc≡ f₁ g h) - assoc≡ (iv f f1) g h = cong (λ k → iv f k ) ( assoc≡ f1 g h ) - - -- positive intutionistic calculus - PL : Category c₁ (c₁ ⊔ c₂) (c₁ ⊔ c₂) - PL = record { - Obj = Objs; - Hom = λ a b → Arrows a b ; - _o_ = λ{a} {b} {c} x y → x ・ y ; - _≈_ = λ x y → x ≡ y ; - Id = λ{a} → id a ; - isCategory = record { - isEquivalence = record {refl = refl ; trans = trans ; sym = sym} ; - identityL = λ {a b f} → identityL {a} {b} {f} ; - identityR = λ {a b f} → identityR {a} {b} {f} ; - o-resp-≈ = λ {a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ; - associative = λ{a b c d f g h } → assoc≡ f g h - } - } where - o-resp-≈ : {A B C : Objs} {f g : Arrows A B} {h i : Arrows B C} → - f ≡ g → h ≡ i → (h ・ f) ≡ (i ・ g) - o-resp-≈ refl refl = refl - --------- --- --- Functor from Positive Logic to Sets --- - - -- open import Category.Sets - -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionalit y c₂ c₂ - - open import Data.List - - C = graphtocat.Chain G - - tr : {a b : vertex G} → edge G a b → ((y : vertex G) → C y a) → (y : vertex G) → C y b - tr f x y = graphtocat.next f (x y) - - fobj : ( a : Objs ) → Set (c₁ ⊔ c₂) - fobj (atom x) = ( y : vertex G ) → C y x - fobj ⊤ = One - fobj (a ∧ b) = ( fobj a /\ fobj b) - fobj (a <= b) = fobj b → fobj a - - fmap : { a b : Objs } → Hom PL a b → fobj a → fobj b - amap : { a b : Objs } → Arrow a b → fobj a → fobj b - amap (arrow x) y = tr x y -- tr x - amap π ( x , y ) = x - amap π' ( x , y ) = y - amap ε (f , x ) = f x - amap (f *) x = λ y → fmap f ( x , y ) - fmap (id a) x = x - fmap (○ a) x = OneObj - fmap < f , g > x = ( fmap f x , fmap g x ) - fmap (iv x f) a = amap x ( fmap f a ) - --- CS is a map from Positive logic to Sets --- Sets is CCC, so we have a cartesian closed category generated by a graph --- as a sub category of Sets - - CS : Functor PL (Sets {c₁ ⊔ c₂}) - FObj CS a = fobj a - FMap CS {a} {b} f = fmap {a} {b} f - isFunctor CS = isf where - _+_ = Category._o_ PL - ++idR = IsCategory.identityR ( Category.isCategory PL ) - distr : {a b c : Obj PL} { f : Hom PL a b } { g : Hom PL b c } → (z : fobj a ) → fmap (g + f) z ≡ fmap g (fmap f z) - distr {a} {a₁} {a₁} {f} {id a₁} z = refl - distr {a} {a₁} {⊤} {f} {○ a₁} z = refl - distr {a} {b} {c ∧ d} {f} {< g , g₁ >} z = cong₂ (λ j k → j , k ) (distr {a} {b} {c} {f} {g} z) (distr {a} {b} {d} {f} {g₁} z) - distr {a} {b} {c} {f} {iv {_} {_} {d} x g} z = adistr (distr {a} {b} {d} {f} {g} z) x where - adistr : fmap (g + f) z ≡ fmap g (fmap f z) → - ( x : Arrow d c ) → fmap ( iv x (g + f) ) z ≡ fmap ( iv x g ) (fmap f z ) - adistr eq x = cong ( λ k → amap x k ) eq - isf : IsFunctor PL Sets fobj fmap - IsFunctor.identity isf = extensionality Sets ( λ x → refl ) - IsFunctor.≈-cong isf refl = refl - IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) +open import CCCSets --- --- SubCategoy SC F A is a category with Obj = FObj F, Hom = FMap @@ -455,6 +207,26 @@ → [ cat b ] f ~ g → a ≡ a' → c ≡ c' → [ uobj b ] f == g cc11 f g (refl eqv) refl refl = mrefl (≡←≈ b eqv) + UC : Functor (CAT {c₁} {c₁} {c₁}) (Grph {c₁} {c₁}) + FObj UC a = record { vertex = Obj a ; edge = Hom a } + FMap UC {a} {b} f = record { vmap = λ e → FObj f e ; emap = λ e → FMap f e } + isFunctor UC = isf where + isf : IsFunctor CAT Grph (λ z → {!!}) {!!} + IsFunctor.identity isf {a} {b} {f} = {!!} + IsFunctor.distr isf {a} {b} {c} {f} {g} = {!!} + IsFunctor.≈-cong isf {a} {b} {f} {g} f=g e = {!!} + +cat-graph-univ : {c₁ : Level} → UniversalMapping (Grph {c₁} {c₁}) (CAT {c₁ } {c₁} {c₁}) forgetful.UC +cat-graph-univ {c₁} = record { + F = {!!} ; + η = {!!} ; + _* = {!!} ; + isUniversalMapping = record { + universalMapping = {!!} ; + uniquness = {!!} + } + } + open ccc-from-graph.Objs open ccc-from-graph.Arrow open ccc-from-graph.Arrows @@ -470,19 +242,19 @@ FCat : Obj (Cart {c₁} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) FCat = record { cat = record { Obj = Obj PL - ; Hom = λ a b → Hom B (FObj CS a) (FObj CS b) - ; _o_ = Category._o_ B - ; _≈_ = Category._≈_ B - ; Id = λ {a} → id1 B (FObj CS a) + ; Hom = λ a b → Hom PL a b + ; _o_ = Category._o_ PL + ; _≈_ = λ {a} {b} f g → FMap CS f ≡ FMap CS g + ; Id = λ {a} → id1 PL a ; isCategory = record { - isEquivalence = IsCategory.isEquivalence (Category.isCategory B) ; - identityL = λ {a b f} → IsCategory.identityL (Category.isCategory B) ; - identityR = λ {a b f} → IsCategory.identityR (Category.isCategory B) ; - o-resp-≈ = λ {a b c f g h i} → IsCategory.o-resp-≈ (Category.isCategory B); - associative = λ {a} {b} {c} {f} {g} {h} → {!!} -- IsCategory.associative (Category.isCategory B) {{!!}} {{!!}} {{!!}} {{!!}} {{!!}} {{!!}} + isEquivalence = {!!} ; + identityL = λ {a b f} → {!!} ; + identityR = λ {a b f} → {!!} ; + o-resp-≈ = λ {a b c f g h i} → {!!} ; + associative = λ {a} {b} {c} {f} {g} {h} → {!!} } } ; - ≡←≈ = λ eq → eq ; + ≡←≈ = λ eq → {!!} ; ccc = {!!} } where B = Sets {c₁ ⊔ c₂} @@ -490,8 +262,7 @@ -- Hom FCat is an image of Fucntor CS, but I don't know how to write it postulate fcat-pl : {a b : Obj (cat FCat) } → Hom (cat FCat) a b → Hom PL a b - fcat-eq : {a b : Obj (cat FCat) } → (f : Hom (cat FCat) a b ) → FMap CS (fcat-pl f) ≡ f - + fcat-eq : {a b : Obj (cat FCat) } → (f : Hom (cat FCat) a b ) → {!!} -- FMap CS (fcat-pl f) ≡ f ccc-graph-univ : {c₁ : Level} → UniversalMapping (Grph {c₁} {c₁}) (Cart {c₁ } {c₁} {c₁}) forgetful.UX ccc-graph-univ {c₁} = record { @@ -526,7 +297,7 @@ vm : (y : vertex a ) → vertex (FObj UX (F a)) vm y = atom y em : { x y : vertex a } (f : edge a x y ) → edge (FObj UX (F a)) (vm x) (vm y) - em {x} {y} f = fmap a (iv (arrow f) (id _)) + em {x} {y} f = {!!} -- fmap a (iv (arrow f) (id _)) cobj : {g : Obj (Grph {c₁} {c₁} ) } {c : Obj Cart} → Hom Grph g (FObj UX c) → Objs g → Obj (cat c) cobj {g} {c} f (atom x) = vmap f x cobj {g} {c} f ⊤ = CCC.１ (ccc c) @@ -546,6 +317,6 @@ solution : {g : Obj Grph } {c : Obj Cart } → Hom Grph g (FObj UX c) → Hom Cart (F g) c solution {g} {c} f = record { cmap = record { FObj = λ x → cobj {g} {c} f x ; - FMap = λ {x} {y} h → c-map {g} {c} {x} {y} f h ; + FMap = λ {x} {y} h → c-map {g} {c} {x} {y} f {!!} ; isFunctor = {!!} } ; ccf = {!!} }
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/CCCSets.agda Mon Mar 08 08:25:30 2021 +0900 @@ -0,0 +1,285 @@ +{-# OPTIONS --allow-unsolved-metas #-} +module CCCSets where + +open import Level +open import Category +open import HomReasoning +open import cat-utility +open import Data.Product renaming (_×_ to _/\_ ) hiding ( <_,_> ) +open import Category.Constructions.Product +open import Relation.Binary.PropositionalEquality hiding ( [_] ) +open import CCC + +open Functor + +-- ccc-1 : Hom A a 1 ≅ {*} +-- ccc-2 : Hom A c (a × b) ≅ (Hom A c a ) × ( Hom A c b ) +-- ccc-3 : Hom A a (c ^ b) ≅ Hom A (a × b) c + +open import Category.Sets + +-- Sets is a CCC + +import Axiom.Extensionality.Propositional +postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂ + +data One {c : Level } : Set c where + OneObj : One -- () in Haskell ( or any one object set ) + +sets : {c : Level } → CCC (Sets {c}) +sets = record { + １ = One + ; ○ = λ _ → λ _ → OneObj + ; _∧_ = _∧_ + ; <_,_> = <,> + ; π = π + ; π' = π' + ; _<=_ = _<=_ + ; _* = _* + ; ε = ε + ; isCCC = isCCC + } where + １ : Obj Sets + １ = One + ○ : (a : Obj Sets ) → Hom Sets a １ + ○ a = λ _ → OneObj + _∧_ : Obj Sets → Obj Sets → Obj Sets + _∧_ a b = a /\ b + <,> : {a b c : Obj Sets } → Hom Sets c a → Hom Sets c b → Hom Sets c ( a ∧ b) + <,> f g = λ x → ( f x , g x ) + π : {a b : Obj Sets } → Hom Sets (a ∧ b) a + π {a} {b} = proj₁ + π' : {a b : Obj Sets } → Hom Sets (a ∧ b) b + π' {a} {b} = proj₂ + _<=_ : (a b : Obj Sets ) → Obj Sets + a <= b = b → a + _* : {a b c : Obj Sets } → Hom Sets (a ∧ b) c → Hom Sets a (c <= b) + f * = λ x → λ y → f ( x , y ) + ε : {a b : Obj Sets } → Hom Sets ((a <= b ) ∧ b) a + ε {a} {b} = λ x → ( proj₁ x ) ( proj₂ x ) + isCCC : CCC.IsCCC Sets １ ○ _∧_ <,> π π' _<=_ _* ε + isCCC = record { + e2 = e2 + ; e3a = λ {a} {b} {c} {f} {g} → e3a {a} {b} {c} {f} {g} + ; e3b = λ {a} {b} {c} {f} {g} → e3b {a} {b} {c} {f} {g} + ; e3c = e3c + ; π-cong = π-cong + ; e4a = e4a + ; e4b = e4b + ; *-cong = *-cong + } where + e2 : {a : Obj Sets} {f : Hom Sets a １} → Sets [ f ≈ ○ a ] + e2 {a} {f} = extensionality Sets ( λ x → e20 x ) + where + e20 : (x : a ) → f x ≡ ○ a x + e20 x with f x + e20 x | OneObj = refl + e3a : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} → + Sets [ ( Sets [ π o ( <,> f g) ] ) ≈ f ] + e3a = refl + e3b : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} → + Sets [ Sets [ π' o ( <,> f g ) ] ≈ g ] + e3b = refl + e3c : {a b c : Obj Sets} {h : Hom Sets c (a ∧ b)} → + Sets [ <,> (Sets [ π o h ]) (Sets [ π' o h ]) ≈ h ] + e3c = refl + π-cong : {a b c : Obj Sets} {f f' : Hom Sets c a} {g g' : Hom Sets c b} → + Sets [ f ≈ f' ] → Sets [ g ≈ g' ] → Sets [ <,> f g ≈ <,> f' g' ] + π-cong refl refl = refl + e4a : {a b c : Obj Sets} {h : Hom Sets (c ∧ b) a} → + Sets [ Sets [ ε o <,> (Sets [ h * o π ]) π' ] ≈ h ] + e4a = refl + e4b : {a b c : Obj Sets} {k : Hom Sets c (a <= b)} → + Sets [ (Sets [ ε o <,> (Sets [ k o π ]) π' ]) * ≈ k ] + e4b = refl + *-cong : {a b c : Obj Sets} {f f' : Hom Sets (a ∧ b) c} → + Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ] + *-cong refl = refl + +-- ○ b +-- b -----------→ 1 +-- | | +-- m | | ⊤ +-- ↓ char m ↓ +-- a -----------→ Ω +-- h + +data II {c : Level } : Set c where + true : II + false : II + +data Tker {c : Level} {a : Set c} ( f : a → II {c} ) : Set c where + isTrue : (x : a ) → f x ≡ true → Tker f + +irr : { c₂ : Level} {d : Set c₂ } { x y : d } ( eq eq' : x ≡ y ) → eq ≡ eq' +irr refl refl = refl + +topos : {c : Level } → Topos (Sets {c}) sets +topos {c} = record { + Ω = II + ; ⊤ = λ _ → true + ; Ker = tker + ; char = tchar + ; isTopos = record { + char-uniqueness = λ {a} {b} {h} m mono → extensionality Sets ( λ x → {!!} ) + ; ker-iso = {!!} + } + } where + tker : {a : Obj Sets} (h : Hom Sets a II) → Equalizer Sets h (Sets [ (λ _ → true) o CCC.○ sets a ]) + tker {a} h = record { + equalizer-c = Tker h + ; equalizer = etker + ; isEqualizer = record { + fe=ge = extensionality Sets ( λ x → e-eq x ) + ; k = k + ; ek=h = λ {d} {h1} {eq} → extensionality Sets ( λ x → refl ) + ; uniqueness = λ {d} {h1} {eq} {k'} ek=h → extensionality Sets ( λ x → uniq h1 eq k' ek=h x ) + } + } where + etker : Hom Sets ( Tker h ) a + etker (isTrue x eq) = x + e-eq : (x : Tker h ) → h ( etker x ) ≡ true + e-eq (isTrue x eq ) = eq + k : {d : Obj Sets} (h₁ : Hom Sets d a) → + Sets [ Sets [ h o h₁ ] ≈ Sets [ Sets [ (λ _ → true) o CCC.○ sets a ] o h₁ ] ] → + Hom Sets d (Tker h) + k {d} h1 hf=hg x = isTrue (h1 x) ( cong ( λ k → k x) hf=hg ) + tker-cong : (x y : Tker h ) → etker x ≡ etker y → x ≡ y + tker-cong ( isTrue x eq ) (isTrue .x eq' ) refl = cong ( λ ee → isTrue x ee ) ( irr eq eq' ) + uniq : {d : Obj Sets} (h1 : Hom Sets d a) -- etker (k h1 eq x) ≡ etker (k' x) + (eq : Sets [ Sets [ h o h1 ] ≈ Sets [ Sets [ (λ _ → true) o (λ _ → OneObj) ] o h1 ] ]) + (k' : Hom Sets d (Tker h)) (ek=h : Sets [ Sets [ etker o k' ] ≈ h1 ]) (x : d) → k h1 eq x ≡ k' x + uniq h1 eq k' ek=h x with cong (λ j → j x) ek=h -- etker (k h1 eq x) ≡ etker (k' x) + ... | t = tker-cong (k h1 eq x) (k' x) (sym t) + tchar : {a b : Obj Sets} (m : Hom Sets b a) → Mono Sets m → Hom Sets a II + tchar {a} {b} m mono x = true + +open import graph +module ccc-from-graph {c₁ c₂ : Level } (G : Graph {c₁} {c₂}) where + + open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] ) + open Graph + + V = vertex G + E : V → V → Set c₂ + E = edge G + + data Objs : Set c₁ where + atom : V → Objs + ⊤ : Objs + _∧_ : Objs → Objs → Objs + _<=_ : Objs → Objs → Objs + + data Arrows : (b c : Objs ) → Set (c₁ ⊔ c₂) + data Arrow : Objs → Objs → Set (c₁ ⊔ c₂) where --- case i + arrow : {a b : V} → E a b → Arrow (atom a) (atom b) + π : {a b : Objs } → Arrow ( a ∧ b ) a + π' : {a b : Objs } → Arrow ( a ∧ b ) b + ε : {a b : Objs } → Arrow ((a <= b) ∧ b ) a + _* : {a b c : Objs } → Arrows (c ∧ b ) a → Arrow c ( a <= b ) --- case v + + data Arrows where + id : ( a : Objs ) → Arrows a a --- case i + ○ : ( a : Objs ) → Arrows a ⊤ --- case i + <_,_> : {a b c : Objs } → Arrows c a → Arrows c b → Arrows c (a ∧ b) -- case iii + iv : {b c d : Objs } ( f : Arrow d c ) ( g : Arrows b d ) → Arrows b c -- cas iv + + _・_ : {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c + id a ・ g = g + ○ a ・ g = ○ _ + < f , g > ・ h = < f ・ h , g ・ h > + iv f g ・ h = iv f ( g ・ h ) + + + identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) ≡ f + identityL = refl + + identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) ≡ f + identityR {a} {a} {id a} = refl + identityR {a} {⊤} {○ a} = refl + identityR {a} {_} {< f , f₁ >} = cong₂ (λ j k → < j , k > ) identityR identityR + identityR {a} {b} {iv f g} = cong (λ k → iv f k ) identityR + + assoc≡ : {a b c d : Objs} (f : Arrows c d) (g : Arrows b c) (h : Arrows a b) → + (f ・ (g ・ h)) ≡ ((f ・ g) ・ h) + assoc≡ (id a) g h = refl + assoc≡ (○ a) g h = refl + assoc≡ < f , f₁ > g h = cong₂ (λ j k → < j , k > ) (assoc≡ f g h) (assoc≡ f₁ g h) + assoc≡ (iv f f1) g h = cong (λ k → iv f k ) ( assoc≡ f1 g h ) + + -- positive intutionistic calculus + PL : Category c₁ (c₁ ⊔ c₂) (c₁ ⊔ c₂) + PL = record { + Obj = Objs; + Hom = λ a b → Arrows a b ; + _o_ = λ{a} {b} {c} x y → x ・ y ; + _≈_ = λ x y → x ≡ y ; + Id = λ{a} → id a ; + isCategory = record { + isEquivalence = record {refl = refl ; trans = trans ; sym = sym} ; + identityL = λ {a b f} → identityL {a} {b} {f} ; + identityR = λ {a b f} → identityR {a} {b} {f} ; + o-resp-≈ = λ {a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ; + associative = λ{a b c d f g h } → assoc≡ f g h + } + } where + o-resp-≈ : {A B C : Objs} {f g : Arrows A B} {h i : Arrows B C} → + f ≡ g → h ≡ i → (h ・ f) ≡ (i ・ g) + o-resp-≈ refl refl = refl +-------- +-- +-- Functor from Positive Logic to Sets +-- + + -- open import Category.Sets + -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionalit y c₂ c₂ + + open import Data.List + + C = graphtocat.Chain G + + tr : {a b : vertex G} → edge G a b → ((y : vertex G) → C y a) → (y : vertex G) → C y b + tr f x y = graphtocat.next f (x y) + + fobj : ( a : Objs ) → Set (c₁ ⊔ c₂) + fobj (atom x) = ( y : vertex G ) → C y x + fobj ⊤ = One + fobj (a ∧ b) = ( fobj a /\ fobj b) + fobj (a <= b) = fobj b → fobj a + + fmap : { a b : Objs } → Hom PL a b → fobj a → fobj b + amap : { a b : Objs } → Arrow a b → fobj a → fobj b + amap (arrow x) y = tr x y -- tr x + amap π ( x , y ) = x + amap π' ( x , y ) = y + amap ε (f , x ) = f x + amap (f *) x = λ y → fmap f ( x , y ) + fmap (id a) x = x + fmap (○ a) x = OneObj + fmap < f , g > x = ( fmap f x , fmap g x ) + fmap (iv x f) a = amap x ( fmap f a ) + +-- CS is a map from Positive logic to Sets +-- Sets is CCC, so we have a cartesian closed category generated by a graph +-- as a sub category of Sets + + CS : Functor PL (Sets {c₁ ⊔ c₂}) + FObj CS a = fobj a + FMap CS {a} {b} f = fmap {a} {b} f + isFunctor CS = isf where + _+_ = Category._o_ PL + ++idR = IsCategory.identityR ( Category.isCategory PL ) + distr : {a b c : Obj PL} { f : Hom PL a b } { g : Hom PL b c } → (z : fobj a ) → fmap (g + f) z ≡ fmap g (fmap f z) + distr {a} {a₁} {a₁} {f} {id a₁} z = refl + distr {a} {a₁} {⊤} {f} {○ a₁} z = refl + distr {a} {b} {c ∧ d} {f} {< g , g₁ >} z = cong₂ (λ j k → j , k ) (distr {a} {b} {c} {f} {g} z) (distr {a} {b} {d} {f} {g₁} z) + distr {a} {b} {c} {f} {iv {_} {_} {d} x g} z = adistr (distr {a} {b} {d} {f} {g} z) x where + adistr : fmap (g + f) z ≡ fmap g (fmap f z) → + ( x : Arrow d c ) → fmap ( iv x (g + f) ) z ≡ fmap ( iv x g ) (fmap f z ) + adistr eq x = cong ( λ k → amap x k ) eq + isf : IsFunctor PL Sets fobj fmap + IsFunctor.identity isf = extensionality Sets ( λ x → refl ) + IsFunctor.≈-cong isf refl = refl + IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) + +
--- a/src/SetsCompleteness.agda Sun Mar 07 15:57:49 2021 +0900 +++ b/src/SetsCompleteness.agda Mon Mar 08 08:25:30 2021 +0900 @@ -202,38 +202,48 @@ open import Relation.Binary.PropositionalEquality open ≡-Reasoning -equc : { c₂ : Level} {a b : Obj (Sets {c₂}) } ( f g : Hom (Sets {c₂}) a b ) → Hom Sets b ({y : a} → f y ≡ g y → sequ a b f g ) -equc {_} {a} {b} f g x {y} eq = elem y eq +record cequ {c : Level} (A B : Set c) ( f g : A → B ) : Set c where + field + sel : B + modh : (x : A ) → f x ≡ sel + modg : (x : A ) → g x ≡ sel + +-- λ f₁ x y → (λ x₁ → x (f₁ x₁)) ≡ (λ x₁ → y (f₁ x₁)) → x ≡ y +-- λ x y → (λ x₁ → x x₁ ≡ y x₁) → x ≡ y +-- Y / R + +-- equc : { c₂ : Level} {a b : Obj (Sets {c₂}) } ( f g : Hom (Sets {c₂}) a b ) +-- → (x : b ) → ((y : a) → f y ≡ x ) → ( (y : a) → g y ≡ x ) → cequ a b f g +-- equc {_} {a} {b} f g x fyx gyx = record { sel = x ; modh = fyx ; modg = gyx } -SetsIsCoEqualizer : { c₂ : Level} → (a b : Obj (Sets {c₂}) ) (f g : Hom (Sets {c₂}) a b) → IsCoEqualizer Sets (equc f g) f g -SetsIsCoEqualizer {c₂} a b f g = record { - ef=eg = extensionality Sets (λ x → refl ) - ; k = k - ; ke=h = λ {d} {h} {eq} → ke=h {d} {h} {eq} - ; uniqueness = {!!} - } where - c : Set c₂ - c = {y : a} → f y ≡ g y → sequ a b f g - e : Hom Sets b c - e x {y} eq = elem y eq - ee : Hom Sets (sequ a b f g) a - ee (elem y eq) = y - k : {d : Obj Sets} (h : Hom Sets b d) → Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] → Hom Sets c d - k {d} h hf=hg = cd where - ca : Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] → a -- (λ x → h (f x)) ≡ (λ x → h (g x)) - ca eq = {!!} - cd : ( {y : a} → f y ≡ g y → sequ a b f g ) → d - cd = {!!} - 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 equc f g ] ≈ h ] - ke=h {d} {h} {eq} = extensionality Sets ( λ x → begin - k h eq ( equc f g x) ≡⟨ {!!} ⟩ - h (f {!!}) ≡⟨ {!!} ⟩ - h (g {!!}) ≡⟨ {!!} ⟩ - h x - ∎ ) where - open import Relation.Binary.PropositionalEquality - open ≡-Reasoning +-- SetsIsCoEqualizer : { c₂ : Level} → (a b : Obj (Sets {c₂}) ) (f g : Hom (Sets {c₂}) a b) +-- → IsCoEqualizer Sets (λ x → ((y : a) → f y ≡ x ) → ( (y : a) → g y ≡ x ) → cequ a b f g) f g +-- SetsIsCoEqualizer {c₂} a b f g = record { +-- ef=eg = extensionality Sets (λ x → {!!} ) +-- ; k = {!!} +-- ; ke=h = λ {d} {h} {eq} → ke=h {d} {h} {eq} +-- ; uniqueness = {!!} +-- } where +-- epi : { c₂ : Level } {a b c : Obj (Sets { c₂})} (f : Hom Sets a b ) → (x y : Hom Sets b c) → Set c₂ +-- epi f x y = Sets [ Sets [ x o f ] ≈ Sets [ y o f ] ] → Sets [ x ≈ y ] +-- c : Set c₂ +-- c = (cequ a b f g ) +-- k : {d : Obj Sets} (h : Hom Sets b d) → Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] → Hom Sets c d +-- k {d} h hf=hg = {!!} where +-- ca : Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] → a -- (λ x → h (f x)) ≡ (λ x → h (g x)) +-- ca eq = {!!} +-- cd : ( {y : a} → f y ≡ g y → sequ a b f g ) → d +-- cd = {!!} +-- 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 {!!} ] ≈ h ] +-- ke=h {d} {h} {eq} = extensionality Sets ( λ x → begin +-- k h eq ( {!!}) ≡⟨ {!!} ⟩ +-- h (f {!!}) ≡⟨ {!!} ⟩ +-- h (g {!!}) ≡⟨ {!!} ⟩ +-- h x +-- ∎ ) where +-- open import Relation.Binary.PropositionalEquality +-- open ≡-Reasoning open Functor
--- a/src/cat-utility.agda Sun Mar 07 15:57:49 2021 +0900 +++ b/src/cat-utility.agda Mon Mar 08 08:25:30 2021 +0900 @@ -223,13 +223,13 @@ -- - -- e f - -- c -------→ a ---------→ b - -- ^ . ---------→ - -- | . g - -- |k . - -- | . h - -- d + -- e f e + -- c -------→ a ---------→ b -------→ c + -- ↑ . ---------→ . | + -- | . g . | + -- |k . . | k + -- | . h h . ↓ + -- d d record IsEqualizer { 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