Members/kono/Proof/category: discrete.agda annotate

annotate discrete.agda @ 799:82a8c1ab4ef5

graph to category

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Tue, 23 Apr 2019 11:30:34 +0900
parents	340708e8d54f
children	984d20c10c87

rev	line source
448 c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	1 open import Category -- https://github.com/konn/category-agda
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	2 open import Level
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	3
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	4 module discrete where
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	5
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	6 open import Relation.Binary.Core
781 340708e8d54f fix for 2.5.4.2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 778 diff changeset	7 open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym )
340708e8d54f fix for 2.5.4.2 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 778 diff changeset	8
448 c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	9
799 82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	10
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	11 module graphtocat where
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	12
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	13 data Arrow { obj : Set } { hom : obj → obj → Set } : ( a b : obj ) → Set where
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	14 id : ( a : obj ) → Arrow a a
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	15 mono : { a b : obj } → hom a b → Arrow a b
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	16 connected : {a b : obj } → {c : obj} → hom b c → Arrow {obj} {hom} a b → Arrow a c
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	17
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	18 _+_ : { obj : Set } { hom : obj → obj → Set } {a b c : obj } (f : (Arrow {obj} {hom} b c )) → (g : (Arrow {obj} {hom} a b )) → Arrow {obj} {hom} a c
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	19 id a + id .a = id a
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	20 id b + mono x = mono x
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	21 id a + connected x y = connected x y
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	22 mono x + id a = mono x
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	23 mono x + mono y = connected x (mono y)
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	24 mono x + connected y z = connected x ( connected y z )
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	25 connected x y + z = connected x ( y + z )
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	26
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	27 assoc-+ : { obj : Set } { hom : obj → obj → Set } {a b c d : obj }
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	28 (f : (Arrow {obj} {hom} c d )) → (g : (Arrow {obj} {hom} b c )) → (h : (Arrow {obj} {hom} a b )) →
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	29 ( f + (g + h)) ≡ ((f + g) + h )
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	30 assoc-+ (id a) (id .a) (id .a) = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	31 assoc-+ (id a) (id .a) (mono x) = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	32 assoc-+ (id a) (id .a) (connected h h₁) = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	33 assoc-+ (id a) (mono x) (id a₁) = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	34 assoc-+ (id a) (mono x) (mono x₁) = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	35 assoc-+ (id a) (mono x) (connected h h₁) = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	36 assoc-+ (id a) (connected g h) _ = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	37 assoc-+ (mono x) (id a) (id .a) = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	38 assoc-+ (mono x) (id a) (mono x₁) = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	39 assoc-+ (mono x) (id a) (connected h h₁) = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	40 assoc-+ (mono x) (mono x₁) (id a) = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	41 assoc-+ (mono x) (mono x₁) (mono x₂) = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	42 assoc-+ (mono x) (mono x₁) (connected h h₁) = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	43 assoc-+ (mono x) (connected g g₁) _ = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	44 assoc-+ (connected f g) (x) (y) = cong (λ k → connected f k) (assoc-+ g x y )
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	45
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	46 open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong )
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	47
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	48 GraphtoCat : ( obj : Set ) ( hom : obj → obj → Set ) → Category Level.zero Level.zero Level.zero
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	49 GraphtoCat obj hom = record {
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	50 Obj = obj ;
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	51 Hom = λ a b → Arrow a b ;
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	52 _o_ = λ{a} {b} {c} x y → _+_ x y ;
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	53 _≈_ = λ x y → x ≡ y ;
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	54 Id = λ{a} → id a ;
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	55 isCategory = record {
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	56 isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ;
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	57 identityL = λ{a b f} → identityL {a} {b} {f} ;
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	58 identityR = λ{a b f} → identityR {a} {b} {f} ;
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	59 o-resp-≈ = λ{a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ;
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	60 associative = λ{a b c d f g h } → assoc-+ f g h
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	61 }
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	62 } where
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	63 identityL : {A B : obj } {f : ( Arrow A B) } → ((id B) + f) ≡ f
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	64 identityL {_} {_} {id a} = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	65 identityL {_} {_} {mono x} = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	66 identityL {_} {_} {connected x f} = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	67 identityR : {A B : obj } {f : ( Arrow {obj} {hom} A B) } → ( f + id A ) ≡ f
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	68 identityR {_} {_} {id a} = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	69 identityR {_} {_} {mono x} = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	70 identityR {_} {_} {connected x f} = cong (λ k → connected x k) ( identityR {_} {_} {f} )
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	71 o-resp-≈ : {A B C : obj } {f g : ( Arrow A B)} {h i : ( Arrow B C)} →
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	72 f ≡ g → h ≡ i → ( h + f ) ≡ ( i + g )
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	73 o-resp-≈ {a} {b} {c} {f} {.f} {h} {.h} refl refl = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	74
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	75
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	76 data TwoObject : Set where
448 c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	77 t0 : TwoObject
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	78 t1 : TwoObject
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	79
458 fd79b6d9f350 fix comment Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 457 diff changeset	80 ---
fd79b6d9f350 fix comment Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 457 diff changeset	81 --- two objects category ( for limit to equalizer proof )
448 c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	82 ---
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	83 --- f
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	84 --- -----→
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	85 --- 0 1
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	86 --- -----→
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	87 --- g
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 456 diff changeset	88 --
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 456 diff changeset	89 -- missing arrows are constrainted by TwoHom data
448 c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	90
799 82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	91 data TwoHom : TwoObject → TwoObject → Set where
466 44bd77c80555 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 461 diff changeset	92 id-t0 : TwoHom t0 t0
44bd77c80555 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 461 diff changeset	93 id-t1 : TwoHom t1 t1
455 55a9b6177ed4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 454 diff changeset	94 arrow-f : TwoHom t0 t1
55a9b6177ed4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 454 diff changeset	95 arrow-g : TwoHom t0 t1
448 c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	96
799 82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	97 TwoCat' : Category Level.zero Level.zero Level.zero
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	98 TwoCat' = GraphtoCat TwoObject TwoHom
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	99 where open graphtocat
448 c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	100
799 82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	101 _×_ : {a b c : TwoObject } → TwoHom b c → TwoHom a b → TwoHom a c
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	102 _×_ {t0} {t1} {t1} id-t1 arrow-f = arrow-f
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	103 _×_ {t0} {t1} {t1} id-t1 arrow-g = arrow-g
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	104 _×_ {t1} {t1} {t1} id-t1 id-t1 = id-t1
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	105 _×_ {t0} {t0} {t1} arrow-f id-t0 = arrow-f
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	106 _×_ {t0} {t0} {t1} arrow-g id-t0 = arrow-g
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	107 _×_ {t0} {t0} {t0} id-t0 id-t0 = id-t0
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	108
448 c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	109
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	110 open TwoHom
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	111
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	112 -- f g h
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	113 -- d <- c <- b <- a
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	114 --
455 55a9b6177ed4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 454 diff changeset	115 -- It can be proved without TwoHom constraints
448 c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	116
799 82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	117 assoc-× : {a b c d : TwoObject }
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	118 {f : (TwoHom c d )} → {g : (TwoHom b c )} → {h : (TwoHom a b )} →
455 55a9b6177ed4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 454 diff changeset	119 ( f × (g × h)) ≡ ((f × g) × h )
799 82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	120 assoc-× {t0} {t0} {t0} {t0} { id-t0 }{ id-t0 }{ id-t0 } = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	121 assoc-× {t0} {t0} {t0} {t1} { arrow-f }{ id-t0 }{ id-t0 } = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	122 assoc-× {t0} {t0} {t0} {t1} { arrow-g }{ id-t0 }{ id-t0 } = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	123 assoc-× {t0} {t0} {t1} {t1} { id-t1 }{ arrow-f }{ id-t0 } = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	124 assoc-× {t0} {t0} {t1} {t1} { id-t1 }{ arrow-g }{ id-t0 } = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	125 assoc-× {t0} {t1} {t1} {t1} { id-t1 }{ id-t1 }{ arrow-f } = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	126 assoc-× {t0} {t1} {t1} {t1} { id-t1 }{ id-t1 }{ arrow-g } = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	127 assoc-× {t1} {t1} {t1} {t1} { id-t1 }{ id-t1 }{ id-t1 } = refl
449 156e64d1bce0 on goinhg ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 448 diff changeset	128
799 82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	129 TwoId : (a : TwoObject ) → (TwoHom a a )
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	130 TwoId t0 = id-t0
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	131 TwoId t1 = id-t1
449 156e64d1bce0 on goinhg ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 448 diff changeset	132
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	133 open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong )
453 3c2ce4474d92 try incomplete pattern for discrete Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 451 diff changeset	134
799 82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	135 TwoCat : Category Level.zero Level.zero Level.zero
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	136 TwoCat = record {
461 8436a018f88a clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 458 diff changeset	137 Obj = TwoObject ;
8436a018f88a clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 458 diff changeset	138 Hom = λ a b → TwoHom a b ;
455 55a9b6177ed4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 454 diff changeset	139 _≈_ = λ x y → x ≡ y ;
461 8436a018f88a clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 458 diff changeset	140 Id = λ{a} → TwoId a ;
449 156e64d1bce0 on goinhg ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 448 diff changeset	141 isCategory = record {
453 3c2ce4474d92 try incomplete pattern for discrete Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 451 diff changeset	142 isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ;
799 82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	143 identityL = λ{a b f} → identityL {a} {b} {f} ;
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	144 identityR = λ{a b f} → identityR {a} {b} {f} ;
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	145 o-resp-≈ = λ{a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ;
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	146 associative = λ{a b c d f g h } → assoc-× {a} {b} {c} {d} {f} {g} {h}
449 156e64d1bce0 on goinhg ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 448 diff changeset	147 }
156e64d1bce0 on goinhg ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 448 diff changeset	148 } where
799 82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	149 identityL : {A B : TwoObject } {f : ( TwoHom A B) } → ((TwoId B) × f) ≡ f
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	150 identityL {t1} {t1} { id-t1 } = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	151 identityL {t0} {t0} { id-t0 } = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	152 identityL {t0} {t1} { arrow-f } = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	153 identityL {t0} {t1} { arrow-g } = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	154 identityR : {A B : TwoObject } {f : ( TwoHom A B) } → ( f × TwoId A ) ≡ f
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	155 identityR {t1} {t1} { id-t1 } = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	156 identityR {t0} {t0} { id-t0 } = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	157 identityR {t0} {t1} { arrow-f } = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	158 identityR {t0} {t1} { arrow-g } = refl
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	159 o-resp-≈ : {A B C : TwoObject } {f g : ( TwoHom A B)} {h i : ( TwoHom B C)} →
455 55a9b6177ed4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 454 diff changeset	160 f ≡ g → h ≡ i → ( h × f ) ≡ ( i × g )
799 82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	161 o-resp-≈ {a} {b} {c} {f} {.f} {h} {.h} refl refl = refl
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	162
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	163
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	164 -- Category with no arrow but identity
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	165
799 82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	166
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	167 open import Data.Empty
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	168
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	169 DiscreteCat' : (S : Set) → Category Level.zero Level.zero Level.zero
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	170 DiscreteCat' S = GraphtoCat S ( λ _ _ → ⊥ )
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	171 where open graphtocat
82a8c1ab4ef5 graph to category Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 781 diff changeset	172
778 06388660995b fix applicative for Agda version 2.5.4.1 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 475 diff changeset	173 record DiscreteHom { c₁ : Level} { S : Set c₁} (a : S) (b : S)
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	174 : Set c₁ where
469 65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	175 field
474 2d32ded94aaf clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 472 diff changeset	176 discrete : a ≡ b -- if f : a → b then a ≡ b
778 06388660995b fix applicative for Agda version 2.5.4.1 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 475 diff changeset	177 dom : S
472 f3d6d0275a0a discrete equality as a dom equality Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 469 diff changeset	178 dom = a
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	179
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	180 open DiscreteHom
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	181
778 06388660995b fix applicative for Agda version 2.5.4.1 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 475 diff changeset	182 _*_ : ∀ {c₁} → {S : Set c₁} {a b c : S} → DiscreteHom {c₁} b c → DiscreteHom {c₁} a b → DiscreteHom {c₁} a c
469 65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	183 _*_ {_} {a} {b} {c} x y = record {discrete = trans ( discrete y) (discrete x) }
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	184
778 06388660995b fix applicative for Agda version 2.5.4.1 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 475 diff changeset	185 DiscreteId : { c₁ : Level} { S : Set c₁} ( a : S ) → DiscreteHom {c₁} a a
469 65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	186 DiscreteId a = record { discrete = refl }
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	187
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	188 open import Relation.Binary.PropositionalEquality
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	189
778 06388660995b fix applicative for Agda version 2.5.4.1 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 475 diff changeset	190 assoc-* : {c₁ : Level } { S : Set c₁} {a b c d : S}
469 65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	191 {f : (DiscreteHom c d )} → {g : (DiscreteHom b c )} → {h : (DiscreteHom a b )} →
472 f3d6d0275a0a discrete equality as a dom equality Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 469 diff changeset	192 dom ( f * (g * h)) ≡ dom ((f * g) * h )
f3d6d0275a0a discrete equality as a dom equality Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 469 diff changeset	193 assoc-* {c₁} {S} {a} {b} {c} {d} {f} {g} {h } = refl
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	194
469 65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	195 DiscreteCat : {c₁ : Level } → (S : Set c₁) → Category c₁ c₁ c₁
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	196 DiscreteCat {c₁} S = record {
778 06388660995b fix applicative for Agda version 2.5.4.1 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 475 diff changeset	197 Obj = S ;
469 65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	198 Hom = λ a b → DiscreteHom {c₁} {S} a b ;
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	199 _o_ = λ{a} {b} {c} x y → _*_ {c₁ } {S} {a} {b} {c} x y ;
474 2d32ded94aaf clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 472 diff changeset	200 _≈_ = λ x y → dom x ≡ dom y ; -- x ≡ y does not work because refl ≡ discrete f is failed as it should be
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	201 Id = λ{a} → DiscreteId a ;
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	202 isCategory = record {
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	203 isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ;
469 65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	204 identityL = λ{a b f} → identityL {a} {b} {f} ;
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	205 identityR = λ{a b f} → identityR {a} {b} {f} ;
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	206 o-resp-≈ = λ{a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ;
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	207 associative = λ{a b c d f g h } → assoc-* { c₁} {S} {a} {b} {c} {d} {f} {g} {h}
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	208 }
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	209 } where
778 06388660995b fix applicative for Agda version 2.5.4.1 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 475 diff changeset	210 identityL : {a b : S} {f : ( DiscreteHom {c₁} a b) } → dom ((DiscreteId b) * f) ≡ dom f
472 f3d6d0275a0a discrete equality as a dom equality Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 469 diff changeset	211 identityL {a} {b} {f} = refl
778 06388660995b fix applicative for Agda version 2.5.4.1 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 475 diff changeset	212 identityR : {A B : S} {f : ( DiscreteHom {c₁} A B) } → dom ( f * DiscreteId A ) ≡ dom f
472 f3d6d0275a0a discrete equality as a dom equality Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 469 diff changeset	213 identityR {a} {b} {f} = refl
778 06388660995b fix applicative for Agda version 2.5.4.1 Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 475 diff changeset	214 o-resp-≈ : {A B C : S } {f g : ( DiscreteHom {c₁} A B)} {h i : ( DiscreteHom B C)} →
472 f3d6d0275a0a discrete equality as a dom equality Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 469 diff changeset	215 dom f ≡ dom g → dom h ≡ dom i → dom ( h * f ) ≡ dom ( i * g )
f3d6d0275a0a discrete equality as a dom equality Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 469 diff changeset	216 o-resp-≈ {a} {b} {c} {f} {g} {h} {i} refl refl = refl
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	217
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	218
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	219
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	220
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	221
472 f3d6d0275a0a discrete equality as a dom equality Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 469 diff changeset	222

Mercurial > hg > Members > kono > Proof > category

annotate discrete.agda @ 799:82a8c1ab4ef5