Mercurial > hg > Members > kono > Proof > category
changeset 942:5084433e0726
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 17 May 2020 11:55:30 +0900 |
| parents | d26f21112e1c |
| children | 3f2525c2b999 |
| files | CCCGraph.agda |
| diffstat | 1 files changed, 17 insertions(+), 11 deletions(-) [+] |
line wrap: on
line diff
--- a/CCCGraph.agda Sun May 17 10:32:22 2020 +0900 +++ b/CCCGraph.agda Sun May 17 11:55:30 2020 +0900 @@ -364,9 +364,9 @@ m21 : (g : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} ) → GMap {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁} {c₂} g (g21 g) m12 : (g : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} ) → GMap {c₁} {c₂} {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} (g21 g) g giso→ : { g : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} } - → {a b : vertex g } → {e : edge g a b } → (m12 g & m21 g) =m= id1 Grph g + → {a b : vertex g } → (m12 g & m21 g) =m= id1 Grph g giso← : { g : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} } - → {a b : vertex (g21 g) } → {e : edge (g21 g) a b } → (m21 g & m12 g ) =m= id1 Grph (g21 g) + → {a b : vertex (g21 g) } → (m21 g & m12 g ) =m= id1 Grph (g21 g) -- Grph [ Grph [ m21 g o m12 g ] ≈ id1 Grph (g21 g) ] fobj : Obj (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) → Obj Grph @@ -381,15 +381,13 @@ FMap UX f = fmap f isFunctor UX = isf where isf : IsFunctor Cart Grph (λ z → g21 (fobj z)) fmap - eff : (a : Obj Cart) (f : vertex (g21 (fobj a)) ) → edge (g21 (fobj a)) f f - eff a f = {!!} IsFunctor.identity isf {a} {b} {f} = begin fmap (id1 Cart a) ≈⟨⟩ fmap {a} {a} (record { cmap = identityFunctor ; ccf = λ x → x }) ≈⟨⟩ record { vmap = λ e → vmap (m21 (fobj a)) (vmap (m12 (fobj a)) e ) ; emap = λ e → emap (m21 (fobj a)) (emap (m12 (fobj a)) e )} - ≈⟨ giso← {fobj a} {f} {f} {eff a f } ⟩ + ≈⟨ giso← {fobj a} {f} {f} ⟩ record { vmap = λ y → y ; emap = λ f → f } ≈⟨⟩ id1 Grph (g21 (fobj a)) @@ -397,11 +395,15 @@ IsFunctor.distr isf {a} {b} {c} {f} {g} = begin fmap ( Cart [ g o f ] ) ≈⟨⟩ - record { vmap = λ e → vmap (m21 (fobj c)) (FObj (cmap (Cart [ g o f ] )) (vmap (m12 (fobj a)) e)) ; - emap = λ e → emap (m21 (fobj c)) (FMap (cmap (Cart [ g o f ] )) (emap (m12 (fobj a)) e)) } + ( m21 (fobj c) & ( record { vmap = λ e → FObj (cmap (( Cart [ g o f ] ))) e ; emap = λ e → FMap (cmap (( Cart [ g o f ] ))) e} & m12 (fobj a) ) ) ≈⟨ {!!} ⟩ - record { vmap = λ e → vmap (m21 (fobj c)) (FObj (cmap g) (vmap (m12 (fobj b)) (vmap (fmap f) e))); - emap = λ e → emap (m21 (fobj c)) (FMap (cmap g) (emap (m12 (fobj b)) (emap (fmap f) e))) } + ( m21 (fobj c) & (record { vmap = λ e → FObj (cmap g) (FObj (cmap f) e) ; emap = λ e → FMap (cmap g) (FMap (cmap f) e) } + & m12 (fobj a))) + ≈⟨ cdr (cdr (car (giso← {fobj b} ))) ⟩ + ( m21 (fobj c) & (record { vmap = λ e → FObj (cmap g) e ; emap = λ e → FMap (cmap g) e} + & ((m12 (fobj b) + & (m21 (fobj b))) & (record { vmap = λ e → FObj (cmap f) e ; emap = λ e → FMap (cmap f) e} + & (m12 (fobj a) ))))) ≈⟨⟩ Grph [ fmap g o fmap f ] ∎ where open ≈-Reasoning Grph @@ -446,8 +448,6 @@ -- ↓ | -- Sets ((z : vertx g) → C z x) ----> ((z : vertx g) → C z y) = h : Hom Sets (fobj (atom x)) (fobj (atom y)) -- - cs : {c₁ c₂ : Level} → (g : Graph {c₁} {c₂} ) → Functor (ccc-from-graph.PL g) (Sets {_}) - cs g = CS g F : Obj (Grph {c₁} {c₂}) → Obj (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) F g = record { cat = Sets {c₁ ⊔ c₂} ; ccc = sets ; ≡←≈ = λ eq → eq } η : (a : Obj (Grph {c₁} {c₂}) ) → Hom Grph a (FObj UX (F a)) @@ -484,6 +484,12 @@ ≈-cong = {!!} } } + submap : (g : Graph {c₁} {c₂}) → Functor (Sets {c₁ ⊔ c₂} )(Sets {c₁ ⊔ c₂} ) + submap g = record { + FObj = λ x → Objs {!!} ; + FMap = λ {x} {y} h → {!!} ; + isFunctor = {!!} + } 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 (xtog x ) ;