Mercurial > hg > Members > kono > Proof > category

comparison CCChom.agda @ 805:979c0bf97a5a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 25 Apr 2019 17:56:30 +0900
parents 2716d2945730
children dd0d0a201990
comparison
equal deleted inserted replaced
804:2716d2945730 805:979c0bf97a5a
617 DX G = GraphtoCat ( record { vertex = Objs {G} ; edge = Arrow {G}} ) 617 DX G = GraphtoCat ( record { vertex = Objs {G} ; edge = Arrow {G}} )
618 618
619 -- open import Category.Sets 619 -- open import Category.Sets
620 -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ 620 -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
621 621
622 fobj : {G : Graph} ( a : Obj (DX G) ) → Set
623 fobj {G} (atom x) = vertex G
624 fobj (a ∧ b) = (fobj a ) /\ (fobj b )
625 fobj (a <= b) = fobj b → fobj a
626 fobj ⊤ = One'
627 {-# TERMINATING #-}
628 fmap : {G : Graph} { a b : Obj (DX G) } → Hom (DX G) a b → fobj a → fobj b
629 fmap {G} {a} {a} (id a) = id1 Sets (fobj a) where open ≈-Reasoning (Sets {Level.zero})
630 fmap {G} {a} {(atom b)} (next (arrow x) f) = λ _ → b
631 fmap {G} {a} {b} (next (id b) f) = fmap f
632 fmap {G} {a} {⊤} (next (○ b) f) = λ _ → OneObj'
633 fmap {G} {a} {b} (next π f) = λ z → proj₁ ( fmap f z )
634 fmap {G} {a} {b} (next π' f) = λ z → proj₂ ( fmap f z )
635 fmap {G} {a} {b} (next ε f) = λ z → ( proj₁ (fmap f z) )( proj₂ (fmap f z) )
636 fmap {G} {a} {b} (next (f ・ g) h) = λ z → fmap ( next f (next g h ) ) z
637 fmap {G} {a} {(_ ∧ _)} (next < f , g > h) = λ z → ( fmap (next f h) z , fmap (next g h) z)
638 fmap {G} {a} {(c <= b)} (next {_} {d} (f *) g ) = λ x y → fmap (next f (id (d ∧ b))) ( fmap g x , y )
639
622 CS : {G : Graph } → Functor (DX G) (Sets {Level.zero}) 640 CS : {G : Graph } → Functor (DX G) (Sets {Level.zero})
623 FObj (CS {G}) (atom x) = vertex G 641 FObj CS a = fobj a
624 FObj CS ⊤ = One' 642 FMap (CS {G}) {a} {b} f = fmap {G} {a} {b} f
625 FObj CS (a ∧ b) = (FObj CS a ) /\ (FObj CS b )
626 FObj CS (a <= b) = FObj CS b → FObj CS a
627 FMap CS {a} {a} (id a) = id1 Sets (FObj CS a) where open ≈-Reasoning (Sets {Level.zero})
628 FMap CS {a} {(atom b)} (next (arrow x) f) = λ _ → b
629 FMap CS {a} {.a₁} (next (id a₁) f) = FMap CS f
630 FMap CS {a} {.⊤} (next (○ a₁) f) = λ _ → OneObj'
631 FMap CS {a} {b} (next π f) = λ z → proj₁ ( FMap CS f z )
632 FMap CS {a} {b} (next π' f) = λ z → proj₂ ( FMap CS f z )
633 FMap CS {a} {b} (next ε f) = λ z → ( proj₁ (FMap CS f z) )( proj₂ (FMap CS f z) )
634 FMap CS {a} {.(_ ∧ _)} (next < f , g > h) = λ z → ( FMap CS (next f h) z , FMap CS (next g h) z)
635 FMap CS {a} {b} (next (f ・ g) h) = λ z → FMap CS ( next f (next g h ) ) z
636 FMap CS {a} {(c <= b)} (next (e *) f) = {!!}
637 isFunctor (CS {G}) = isf where 643 isFunctor (CS {G}) = isf where
638 distrCS : {a b c : Obj (DX G)} { g : Hom (DX G) b c } { f : Hom (DX G) a b } → Sets [ FMap CS ((DX G) [ g o f ]) ≈ Sets [ FMap CS g o FMap CS f ] ] 644 _++_ = Category._o_ (DX G)
639 distrCS = {!!} 645 distrCS : {a b c : Obj (DX G)} { f : Hom (DX G) a b } { g : Hom (DX G) b c } → Sets [ fmap ((DX G) [ g o f ]) ≈ Sets [ fmap g o fmap f ] ]
640 isf : IsFunctor (DX G) Sets (FObj CS) ( FMap CS ) 646 distrCS {a} {.a} {.a} {id a} {id .a} = refl
641 IsFunctor.identity isf = extensionality Sets ( λ x → {!!} ) 647 distrCS {a} {.a} {c} {id a} {next x g} = begin
642 IsFunctor.distr isf = distrCS 648 fmap (DX G [ next x g o Chain.id a ])
649 ≈⟨⟩
650 fmap ( next x ( g ++ (Chain.id a)))
651 ≈⟨ extensionality Sets ( λ y → cong ( λ k → fmap ( next x k ) y ) (idR1 (DX G)) ) ⟩
652 fmap ( next x g )
653 ≈↑⟨ idL ⟩
654 Sets [ fmap (next x g) o fmap (Chain.id a) ]
655 ∎ where open ≈-Reasoning Sets
656 distrCS {a} {b} {b} {f} {id b} = refl
657 distrCS {a} {b} {.(atom _)} {f} {next (arrow x) g} = refl
658 distrCS {a} {b} {c} {f} {next (id c) g} = begin
659 fmap (DX G [ next (Arrow.id c) g o f ])
660 ≈⟨ {!!} ⟩
661 Sets [ fmap (next (Arrow.id c) g) o fmap f ]
662 ∎ where open ≈-Reasoning Sets
663 distrCS {a} {b} {.⊤} {f} {next (○ a₁) g} = begin
664 fmap (DX G [ next (○ a₁) g o f ])
665 ≈⟨ extensionality Sets ( λ x → refl ) ⟩
666 Sets [ fmap (next (○ a₁) g) o fmap f ]
667 ∎ where open ≈-Reasoning Sets
668 distrCS {a} {b} {c} {f} {next π g} = {!!}
669 distrCS {a} {b} {c} {f} {next π' g} = {!!}
670 distrCS {a} {b} {c} {f} {next ε g} = {!!}
671 distrCS {a} {b} {.(_ ∧ _)} {f} {next < x , x₁ > g} = {!!}
672 distrCS {a} {b} {c} {f} {next (x ・ x₁) g} = extensionality Sets ( λ z → begin
673 fmap (DX G [ next (x ・ x₁) g o f ]) z
674 ≡⟨ {!!} ⟩
675 ( Sets [ fmap (next (x ・ x₁) g) o fmap f ] ) z
676 ∎ ) where open ≡-Reasoning
677 distrCS {a} {b} {.(_ <= _)} {f} {next (x *) g} = {!!}
678 isf : IsFunctor (DX G) Sets fobj fmap
679 IsFunctor.identity isf = extensionality Sets ( λ x → refl )
643 IsFunctor.≈-cong isf refl = refl 680 IsFunctor.≈-cong isf refl = refl
644 681 IsFunctor.distr isf {a} {b} {c} {g} {f} = distrCS {a} {b} {c} {g} {f}
682