Mercurial > hg > Members > kono > Proof > category

comparison CCChom.agda @ 812:4ff300e1e98c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
graph to CCC done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 27 Apr 2019 08:42:36 +0900
parents 2de0358ea10a
children e4986625ddd7
comparison
equal deleted inserted replaced
811:2de0358ea10a 812:4ff300e1e98c
592 open import discrete 592 open import discrete
593 open graphtocat 593 open graphtocat
594 594
595 open Graph 595 open Graph
596 596
597 data Objs {G : Graph } : Set where 597 data Objs (G : Graph ) : Set where
598 atom : (vertex G) → Objs 598 atom : (vertex G) → Objs G
599 ⊤ : Objs 599 ⊤ : Objs G
600 _∧_ : Objs {G} → Objs {G} → Objs 600 _∧_ : Objs G → Objs G → Objs G
601 _<=_ : Objs {G} → Objs {G} → Objs 601 _<=_ : Objs G → Objs G → Objs G
602 602
603 data Arrow {G : Graph } : Objs {G} → Objs {G} → Set where 603 data Arrow (G : Graph ) : Objs G → Objs G → Set where
604 arrow : {a b : vertex G} → (edge G) a b → Arrow (atom a) (atom b) 604 arrow : {a b : vertex G} → (edge G) a b → Arrow G (atom a) (atom b)
605 ○ : (a : Objs ) → Arrow a ⊤ 605 ○ : (a : Objs G ) → Arrow G a ⊤
606 π : {a b : Objs } → Arrow ( a ∧ b ) a 606 π : {a b : Objs G } → Arrow G ( a ∧ b ) a
607 π' : {a b : Objs } → Arrow ( a ∧ b ) b 607 π' : {a b : Objs G } → Arrow G ( a ∧ b ) b
608 ε : {a b : Objs } → Arrow ((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 } → Arrow c a → Arrow c b → Arrow c (a ∧ b)
610 -- _* : {a b c : Objs } → Arrow (c ∧ b ) a → Arrow c ( a <= b ) 610 -- _* : {a b c : Objs } → Arrow (c ∧ b ) a → Arrow 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
617 617
618 open SM 618 open SM
619 619
620 -- positive intutionistic calculus 620 -- positive intutionistic calculus
621 PL : (G : SM) → Graph 621 PL : (G : SM) → Graph
622 PL G = record { vertex = Objs {graph G} ; edge = Arrow {graph G}} 622 PL G = record { vertex = Objs (graph G) ; edge = Arrow (graph G) }
623 DX : (G : SM) → Category Level.zero Level.zero Level.zero 623 DX : (G : SM) → Category Level.zero Level.zero Level.zero
624 DX G = GraphtoCat (PL G) 624 DX G = GraphtoCat (PL G)
625 625
626 -- open import Category.Sets 626 -- open import Category.Sets
627 -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ 627 -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
628 628
629 fobj : {G : SM} ( a : Obj (DX G) ) → Set 629 fobj : {G : SM} ( a : Objs (graph G) ) → Set
630 fobj {G} (atom x) = sobj G x 630 fobj {G} (atom x) = sobj G x
631 fobj {G} (a ∧ b) = (fobj {G} a ) /\ (fobj {G} b ) 631 fobj {G} (a ∧ b) = (fobj {G} a ) /\ (fobj {G} b )
632 fobj {G} (a <= b) = fobj {G} b → fobj {G} a 632 fobj {G} (a <= b) = fobj {G} b → fobj {G} a
633 fobj ⊤ = One' 633 fobj ⊤ = One'
634 fmap : {G : SM} { a b : Obj (DX G) } → Hom (DX G) a b → fobj {G} a → fobj {G} b 634 amap : {G : SM} { a b : Objs (graph G) } → Arrow (graph G) a b → fobj {G} a → fobj {G} b
635 amap {G} {.(atom _)} {.(atom _)} (arrow x) = smap G x
636 amap {G} {a} {.⊤} (○ a) _ = OneObj'
637 amap {G} {.(b ∧ _)} {b} π ( x , _) = x
638 amap {G} {.(_ ∧ b)} {b} π'( _ , x) = x
639 amap {G} {.((b <= _) ∧ _)} {b} ε ( f , x ) = f x
640 fmap : {G : SM} { a b : Objs (graph G) } → Hom (DX G) a b → fobj {G} a → fobj {G} b
635 fmap {G} {a} {a} (id a) = λ z → z 641 fmap {G} {a} {a} (id a) = λ z → z
636 fmap {G} {a} {(atom b)} (next {a} {c} (arrow x) f) = λ (z : fobj a) → smap G x ( fmap f z ) 642 fmap {G} {a} {b} (next x f ) = Sets [ amap {G} x o fmap f ]
637 fmap {G} {a} {⊤} (next (○ b) f) = λ _ → OneObj'
638 fmap {G} {a} {b} (next {a} {.b ∧ y} {b} π f) = λ z → proj₁ ( fmap {G} {a} {b ∧ y} f z )
639 fmap {G} {a} {b} (next {.a} {x ∧ .b} {.b} π' f) = λ z → proj₂ ( fmap f z ) where
640 fmap {G} {a} {b} (next {.a} {(x <= y) ∧ y} {.b} ε f) = λ z → ( proj₁ (fmap f z))( proj₂ (fmap f z))
641 643
642 CS : (G : SM ) → Functor (DX G) (Sets {Level.zero}) 644 CS : (G : SM ) → Functor (DX G) (Sets {Level.zero})
643 FObj (CS G) a = fobj a 645 FObj (CS G) a = fobj a
644 FMap (CS G) {a} {b} f = fmap {G} {a} {b} f 646 FMap (CS G) {a} {b} f = fmap {G} {a} {b} f
645 isFunctor (CS G) = isf where 647 isFunctor (CS G) = isf where
646 _++_ = Category._o_ (DX G) 648 _++_ = Category._o_ (DX G)
647 ++idR = IsCategory.identityR ( Category.isCategory ( DX G ) ) 649 ++idR = IsCategory.identityR ( Category.isCategory ( DX G ) )
648 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) 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)
651 distr {a} {b} {c} {f} {next {.b} {.c ∧ x} {.c} π g} z = begin
652 fmap (DX G [ next π g o f ]) z
653 ≡⟨⟩
654 fmap {G} {a} {c} (next {PL G} {a} {c ∧ x} {c} π ( g ++ f)) z
655 ≡⟨⟩
656 proj₁ ( fmap {G} {a} {c ∧ x} (g ++ f ) z )
657 ≡⟨ cong ( λ k → proj₁ k ) ( distr {a} {b} {(c ∧ x)} {f} {g} z ) ⟩
658 proj₁ ( fmap g ( fmap f z ))
659 ≡⟨⟩
660 (Sets [ fmap (next π g) o fmap f ]) z
661 ∎ where open ≡-Reasoning
662 distr {a} {b} {c} {f} {next {b} {x ∧ c} π' g} z = begin
663 fmap (DX G [ next π' g o f ]) z
664 ≡⟨⟩
665 fmap (next π' (g ++ f)) z
666 ≡⟨⟩
667 proj₂ (fmap (g ++ f) z)
668 ≡⟨ cong ( λ k → proj₂ k ) ( distr {a} {b} {x ∧ c} {f} {g} z ) ⟩
669 ( Sets [ fmap (next π' g) o fmap f ] ) z
670 ∎ where open ≡-Reasoning
671 distr {a} {b} {c} {f} {next {b} {(c <= x) ∧ x} {c} ε g} z = begin
672 fmap (DX G [ next ε g o f ] ) z
673 ≡⟨⟩
674 fmap (next ε (g ++ f)) z
675 ≡⟨⟩
676 proj₁ (fmap (g ++ f) z) ( proj₂ (fmap (g ++ f) z) )
677 ≡⟨ cong ( λ k → proj₁ k ( proj₂ k)) (distr {a} {b} {(c <= x) ∧ x} {f} {g} z) ⟩
678 proj₁ (fmap g (fmap f z)) ( proj₂ (fmap g (fmap f z)))
679 ≡⟨⟩
680 fmap (next ε g) (fmap f z)
681 ≡⟨⟩
682 ( Sets [ fmap (next ε g) o fmap f ] ) z
683 ∎ where open ≡-Reasoning
649 distr {a} {.a} {.a} {id a} {id .a} z = refl 684 distr {a} {.a} {.a} {id a} {id .a} z = refl
650 distr {a} {.a} {c} {id a} {next x g} z = begin 685 distr {a} {.a} {c} {id a} {next {a} {b} x g} z = begin
651 fmap (DX G [ next x g o Chain.id a ]) z 686 fmap (DX G [ next x g o Chain.id a ]) z
652 ≡⟨⟩ 687 ≡⟨⟩
653 fmap ( next x ( g ++ (Chain.id a))) z 688 fmap ( next x ( g ++ (Chain.id a))) z
654 ≡⟨ cong ( λ k → fmap ( next x k ) z ) ++idR ⟩ 689 ≡⟨ cong ( λ k → fmap ( next x k ) z ) ( ++idR {a} {b} {g} ) ⟩
655 fmap ( next x g ) z 690 fmap ( next x g ) z
656 ≡⟨ refl ⟩ 691 ≡⟨ refl ⟩
657 ( Sets [ fmap (next x g) o fmap (Chain.id a) ] ) z 692 ( Sets [ fmap (next x g) o fmap (Chain.id a) ] ) z
658 ∎ where open ≡-Reasoning 693 ∎ where open ≡-Reasoning
659 distr {a} {b} {b} {f} {id b} z = refl 694 distr {a} {b} {b} {f} {id b} z = refl
673 distr {a} {b} {.⊤} {f} {next (○ a₁) g} z = begin 708 distr {a} {b} {.⊤} {f} {next (○ a₁) g} z = begin
674 fmap (DX G [ next (○ a₁) g o f ]) z 709 fmap (DX G [ next (○ a₁) g o f ]) z
675 ≡⟨⟩ 710 ≡⟨⟩
676 (Sets [ fmap (next (○ a₁) g) o fmap f ]) z 711 (Sets [ fmap (next (○ a₁) g) o fmap f ]) z
677 ∎ where open ≡-Reasoning 712 ∎ where open ≡-Reasoning
678 distr {a} {b} {c} {f} {next {.b} {.c ∧ x} {.c} π g} z = begin
679 fmap (DX G [ next π g o f ]) z
680 ≡⟨⟩
681 fmap {G} {a} {c} (next {PL G} {a} {c ∧ x} {c} π ( g ++ f)) z
682 ≡⟨ {!!} ⟩
683 proj₁ ( fmap {G} {a} {c ∧ x} (g ++ f ) z )
684 ≡⟨ cong ( λ k → proj₁ k ) ( distr {a} {b} {(c ∧ x)} {f} {g} z ) ⟩
685 proj₁ ( fmap g ( fmap f z ))
686 ≡⟨ {!!} ⟩
687 (Sets [ fmap (next π g) o fmap f ]) z
688 ∎ where open ≡-Reasoning
689 distr {a} {b} {c} {f} {next π' g} z = begin
690 fmap (DX G [ next π' g o f ]) z
691 ≡⟨⟩
692 fmap (next π' (g ++ f)) z
693 ≡⟨ {!!} ⟩
694 proj₂ (fmap (g ++ f) z)
695 ≡⟨ {!!} ⟩
696 ( Sets [ fmap (next π' g) o fmap f ] ) z
697 ∎ where open ≡-Reasoning
698 distr {a} {b} {c} {f} {next {b} {(c <= x) ∧ x} {c} ε g} z = begin
699 fmap (DX G [ next ε g o f ] ) z
700 ≡⟨⟩
701 fmap (next ε (g ++ f)) z
702 ≡⟨ {!!} ⟩
703 proj₁ (fmap (g ++ f) z) ( proj₂ (fmap (g ++ f) z) )
704 ≡⟨ cong ( λ k → proj₁ k ( proj₂ k)) (distr {a} {b} {(c <= x) ∧ x} {f} {g} z) ⟩
705 proj₁ (fmap g (fmap f z)) ( proj₂ (fmap g (fmap f z)))
706 ≡⟨ {!!} ⟩
707 fmap (next ε g) (fmap f z)
708 ≡⟨⟩
709 ( Sets [ fmap (next ε g) o fmap f ] ) z
710 ∎ where open ≡-Reasoning
711 isf : IsFunctor (DX G) Sets fobj fmap 713 isf : IsFunctor (DX G) Sets fobj fmap
712 IsFunctor.identity isf = extensionality Sets ( λ x → refl ) 714 IsFunctor.identity isf = extensionality Sets ( λ x → refl )
713 IsFunctor.≈-cong isf refl = refl 715 IsFunctor.≈-cong isf refl = refl
714 IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) 716 IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z )
715 717
716 <_,_> : { G : SM } → {a b c : Objs {graph G}} → Arrow c a → Arrow c b → Hom Sets (FObj (CS G) c ) (FObj (CS G) (a ∧ b) ) 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) )
717 <_,_> {G} {a} {b} {c} f g = λ z → ( (FMap (CS G) ( next f (id c))) z , FMap (CS G) (next g (id c)) z ) 719 <_,_> {G} {a} {b} {c} f g = λ z → ( (FMap (CS G) ( next f (id c))) z , FMap (CS G) (next g (id c)) z )
718 720
719 _* : { G : SM } → {a b c : Objs {graph G}} → Arrow (c ∧ b ) a → Hom Sets (FObj (CS G) c) (FObj (CS G) ( a <= b )) 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 ))
720 _* {G} {a} {b} {c} f = λ z y → FMap (CS G) ( next f (id (c ∧ b) ) ) ( z , y ) 722 _* {G} {a} {b} {c} f = λ z y → FMap (CS G) ( next f (id (c ∧ b) ) ) ( z , y )