Mercurial > hg > Members > kono > Proof > category
view CCCGraph1.agda @ 877:66dfc4f80ba3
o-resp remains
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 10 Apr 2020 09:21:54 +0900 |
parents | d8ed393d7878 |
children | 0793d9adbbdd |
line wrap: on
line source
open import Level open import Category module CCCgraph1 where open import HomReasoning open import cat-utility open import Relation.Binary.PropositionalEquality hiding ( [_] ) open import CCC open import graph module ccc-from-graph {c₁ c₂ : Level} (G : Graph {c₁} {c₂} ) where open import Relation.Binary.PropositionalEquality hiding ( [_] ) open import Relation.Binary.Core open Graph data Objs : Set (c₁ ⊔ c₂) where atom : (vertex G) → Objs ⊤ : Objs _∧_ : Objs → Objs → Objs _<=_ : Objs → Objs → Objs data Arrow : Objs → Objs → Set (c₁ ⊔ c₂) where --- case i arrow : {a b : vertex G} → (edge G) 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 } → Arrow (c ∧ b ) a → Arrow c ( a <= b ) --- case v data Arrows : (b c : Objs ) → Set ( c₁ ⊔ c₂ ) 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 ) 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 identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) ≡ f identityL = refl associative : {a b c d : Objs} (f : Arrows c d) (g : Arrows b c) (h : Arrows a b) → (f ・ (g ・ h)) ≡ ((f ・ g) ・ h) associative (id a) g h = refl associative (○ a) g h = refl associative < f , f₁ > g h = cong₂ (λ j k → < j , k > ) (associative f g h) (associative f₁ g h) associative (iv f f1) g h = cong (λ k → iv f k ) ( associative f1 g h ) PL : Category (c₁ ⊔ 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 } → associative 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 eval : {a b : Objs } (f : Arrows a b ) → Arrows a b eval (id a) = id a eval (○ a) = ○ a eval < f , f₁ > = < eval f , eval f₁ > eval (iv f (id a)) = iv f (id a) eval (iv f (○ a)) = iv f (○ a) eval (iv π < g , h >) = eval g eval (iv π' < g , h >) = eval h eval (iv ε < g , h >) = iv ε < eval g , eval h > eval (iv (f *) < g , h >) = iv (f *) < eval g , eval h > eval (iv f (iv g h)) with eval (iv g h) eval (iv f (iv g h)) | id a = iv f (id a) eval (iv f (iv g h)) | ○ a = iv f (○ a) eval (iv π (iv g h)) | < t , t₁ > = t eval (iv π' (iv g h)) | < t , t₁ > = t₁ eval (iv ε (iv g h)) | < t , t₁ > = iv ε < t , t₁ > eval (iv (f *) (iv g h)) | < t , t₁ > = iv (f *) < t , t₁ > eval (iv f (iv g h)) | iv f1 t = iv f (iv f1 t) PL1 : Category (c₁ ⊔ c₂) (c₁ ⊔ c₂) (c₁ ⊔ c₂) PL1 = record { Obj = Objs; Hom = λ a b → Arrows a b ; _o_ = λ{a} {b} {c} x y → x ・ y ; _≈_ = λ x y → eval x ≡ eval y ; Id = λ{a} → id a ; isCategory = record { isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ; identityL = λ {a b f} → cong (λ k → eval k ) (identityL {a} {b} {f}); identityR = λ {a b f} → cong (λ k → eval k ) (identityR {a} {b} {f}); o-resp-≈ = λ {a b c f g h i} → o-resp-≈-e {a} {b} {c} {f} {g} {h} {i} ; associative = λ{a b c d f g h } → cong (λ k → eval k ) (associative f g h ) } } where o-resp-≈-e : {A B C : Objs} {f g : Arrows A B} {h i : Arrows B C} → eval f ≡ eval g → eval h ≡ eval i → eval (h ・ f) ≡ eval (i ・ g) o-resp-≈-e f=g h=i = {!!} fmap : {A B : Obj PL} → Hom PL A B → Hom PL A B fmap (id a) = id _ fmap (○ a) = ○ a fmap < f , g > = < fmap f , fmap g > fmap (iv (arrow x) g) = iv (arrow x) (fmap g) fmap (iv π (id _)) = {!!} fmap (iv π < g , g₁ >) = fmap g fmap (iv π (iv f g)) = {!!} fmap (iv π' (id _)) = {!!} fmap (iv π' < g , g₁ >) = fmap g₁ fmap (iv π' (iv f g)) = {!!} fmap (iv ε (id _)) = {!!} fmap (iv ε < f , g >) = {!!} fmap (iv ε (iv f g)) = {!!} fmap (iv (f *) g) = {!!} PLCCC : Functor PL PL PLCCC = record { FObj = λ x → x ; FMap = {!!} ; isFunctor = record { identity = {!!} ; distr = {!!} ; ≈-cong = {!!} } }