Mercurial > hg > Members > kono > Proof > category

comparison CCChom.agda @ 814:e4986625ddd7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add <= and <,>
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 27 Apr 2019 10:10:40 +0900
parents 4ff300e1e98c
children bb9fd483f560
comparison
equal deleted inserted replaced
813:9b8ee2ddd92d 814:e4986625ddd7
604 arrow : {a b : vertex G} → (edge G) a b → Arrow G (atom a) (atom b) 604 arrow : {a b : vertex G} → (edge G) a b → Arrow G (atom a) (atom b)
605 ○ : (a : Objs G ) → Arrow G a ⊤ 605 ○ : (a : Objs G ) → Arrow G a ⊤
606 π : {a b : Objs G } → Arrow G ( a ∧ b ) a 606 π : {a b : Objs G } → Arrow G ( a ∧ b ) a
607 π' : {a b : Objs G } → Arrow G ( a ∧ b ) b 607 π' : {a b : Objs G } → Arrow G ( a ∧ b ) b
608 ε : {a b : Objs G } → Arrow G ((a <= b) ∧ b ) a 608 ε : {a b : Objs G } → Arrow G ((a <= b) ∧ b ) a
609 -- <_,_> : {a b c : Objs } → Arrow c a → Arrow c b → Arrow c (a ∧ b) 609 <_,_> : {a b c : Objs G } → Arrow G c a → Arrow G c b → Arrow G c (a ∧ b)
610 -- _* : {a b c : Objs } → Arrow (c ∧ b ) a → Arrow c ( a <= b ) 610 _* : {a b c : Objs G } → Arrow G (c ∧ b ) a → Arrow G c ( a <= b )
611 611
612 record SM : Set (suc Level.zero) where 612 record SM : Set (suc Level.zero) where
613 field 613 field
614 graph : Graph 614 graph : Graph
615 sobj : vertex graph → Set 615 sobj : vertex graph → Set
635 amap {G} {.(atom _)} {.(atom _)} (arrow x) = smap G x 635 amap {G} {.(atom _)} {.(atom _)} (arrow x) = smap G x
636 amap {G} {a} {.⊤} (○ a) _ = OneObj' 636 amap {G} {a} {.⊤} (○ a) _ = OneObj'
637 amap {G} {.(b ∧ _)} {b} π ( x , _) = x 637 amap {G} {.(b ∧ _)} {b} π ( x , _) = x
638 amap {G} {.(_ ∧ b)} {b} π'( _ , x) = x 638 amap {G} {.(_ ∧ b)} {b} π'( _ , x) = x
639 amap {G} {.((b <= _) ∧ _)} {b} ε ( f , x ) = f x 639 amap {G} {.((b <= _) ∧ _)} {b} ε ( f , x ) = f x
640 amap {G} {a} {.(_ ∧ _)} < f , g > x = (amap f x , amap g x)
641 amap {G} {a} {.(_ <= _)} (f *) x = λ y → amap f ( x , y )
640 fmap : {G : SM} { a b : Objs (graph G) } → Hom (DX G) a b → fobj {G} a → fobj {G} b 642 fmap : {G : SM} { a b : Objs (graph G) } → Hom (DX G) a b → fobj {G} a → fobj {G} b
641 fmap {G} {a} {a} (id a) = λ z → z 643 fmap {G} {a} {a} (id a) = λ z → z
642 fmap {G} {a} {b} (next x f ) = Sets [ amap {G} x o fmap f ] 644 fmap {G} {a} {b} (next x f ) = Sets [ amap {G} x o fmap f ]
643 645
644 CS : (G : SM ) → Functor (DX G) (Sets {Level.zero}) 646 CS : (G : SM ) → Functor (DX G) (Sets {Level.zero})
646 FMap (CS G) {a} {b} f = fmap {G} {a} {b} f 648 FMap (CS G) {a} {b} f = fmap {G} {a} {b} f
647 isFunctor (CS G) = isf where 649 isFunctor (CS G) = isf where
648 _++_ = Category._o_ (DX G) 650 _++_ = Category._o_ (DX G)
649 ++idR = IsCategory.identityR ( Category.isCategory ( DX G ) ) 651 ++idR = IsCategory.identityR ( Category.isCategory ( DX G ) )
650 distr : {a b c : Obj (DX G)} { f : Hom (DX G) a b } { g : Hom (DX G) b c } → (z : fobj {G} a ) → fmap (g ++ f) z ≡ fmap g (fmap f z) 652 distr : {a b c : Obj (DX G)} { f : Hom (DX G) a b } { g : Hom (DX G) b c } → (z : fobj {G} a ) → fmap (g ++ f) z ≡ fmap g (fmap f z)
653 distr {a} {b} {e ∧ e1} {f} {next {b} {d} {e ∧ e1} < x , y > g} z = begin
654 fmap (next < x , y > g ++ f) z
655 ≡⟨⟩
656 amap x (fmap (g ++ f) z) , amap y (fmap (g ++ f) z)
657 ≡⟨ cong ( λ k → ( amap x k , amap y k )) (distr {a} {b} {d} {f} {g} z) ⟩
658 amap x (fmap g (fmap f z)) , amap y (fmap g (fmap f z))
659 ≡⟨⟩
660 fmap (next < x , y > g) (fmap f z)
661 ∎ where open ≡-Reasoning
662 distr {a} {b} {c <= d} {f} {next {b} {e} {c <= d} (x *) g} z = begin
663 fmap (next (x *) g ++ f) z
664 ≡⟨⟩
665 (λ y → amap x (fmap (g ++ f) z , y) )
666 ≡⟨ extensionality Sets ( λ y → cong ( λ k → (amap x (k , y )) ) (distr {a} {b} {e} {f} {g} z) ) ⟩
667 (λ y → amap x (fmap g (fmap f z) , y))
668 ≡⟨⟩
669 fmap (next (x *) g) (fmap f z)
670 ∎ where open ≡-Reasoning
651 distr {a} {b} {c} {f} {next {.b} {.c ∧ x} {.c} π g} z = begin 671 distr {a} {b} {c} {f} {next {.b} {.c ∧ x} {.c} π g} z = begin
652 fmap (DX G [ next π g o f ]) z 672 fmap (DX G [ next π g o f ]) z
653 ≡⟨⟩ 673 ≡⟨⟩
654 fmap {G} {a} {c} (next {PL G} {a} {c ∧ x} {c} π ( g ++ f)) z 674 fmap {G} {a} {c} (next {PL G} {a} {c ∧ x} {c} π ( g ++ f)) z
655 ≡⟨⟩ 675 ≡⟨⟩
713 isf : IsFunctor (DX G) Sets fobj fmap 733 isf : IsFunctor (DX G) Sets fobj fmap
714 IsFunctor.identity isf = extensionality Sets ( λ x → refl ) 734 IsFunctor.identity isf = extensionality Sets ( λ x → refl )
715 IsFunctor.≈-cong isf refl = refl 735 IsFunctor.≈-cong isf refl = refl
716 IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) 736 IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z )
717 737
718 <_,_> : { G : SM } → {a b c : Objs (graph G)} → Arrow (graph G) c a → Arrow (graph G) c b → Hom Sets (FObj (CS G) c ) (FObj (CS G) (a ∧ b) )
719 <_,_> {G} {a} {b} {c} f g = λ z → ( (FMap (CS G) ( next f (id c))) z , FMap (CS G) (next g (id c)) z )
720
721 _* : { G : SM } → {a b c : Objs (graph G)} → Arrow (graph G) (c ∧ b ) a → Hom Sets (FObj (CS G) c) (FObj (CS G) ( a <= b ))
722 _* {G} {a} {b} {c} f = λ z y → FMap (CS G) ( next f (id (c ∧ b) ) ) ( z , y )