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

annotate discrete.agda @ 767:0f8e3b962c13

Added tag current for changeset c30ca91f3a76

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Tue, 12 Dec 2017 09:25:50 +0900
parents	4c0a955b651d
children	06388660995b

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
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	7
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	8 data TwoObject {c₁ : Level} : Set c₁ where
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	9 t0 : TwoObject
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	10 t1 : TwoObject
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	11
458 fd79b6d9f350 fix comment Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 457 diff changeset	12 ---
fd79b6d9f350 fix comment Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 457 diff changeset	13 --- 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	14 ---
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	15 --- f
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	16 --- -----→
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	17 --- 0 1
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	18 --- -----→
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	19 --- g
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 456 diff changeset	20 --
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 456 diff changeset	21 -- missing arrows are constrainted by TwoHom data
448 c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	22
455 55a9b6177ed4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 454 diff changeset	23 data TwoHom {c₁ c₂ : Level } : TwoObject {c₁} → TwoObject {c₁} → Set c₂ where
466 44bd77c80555 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 461 diff changeset	24 id-t0 : TwoHom t0 t0
44bd77c80555 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 461 diff changeset	25 id-t1 : TwoHom t1 t1
455 55a9b6177ed4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 454 diff changeset	26 arrow-f : TwoHom t0 t1
55a9b6177ed4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 454 diff changeset	27 arrow-g : TwoHom t0 t1
448 c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	28
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	29
461 8436a018f88a clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 458 diff changeset	30 _×_ : ∀ {c₁ c₂} → {a b c : TwoObject {c₁}} → TwoHom {c₁} {c₂} b c → TwoHom {c₁} {c₂} a b → TwoHom {c₁} {c₂} a c
466 44bd77c80555 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 461 diff changeset	31 _×_ {_} {_} {t0} {t1} {t1} id-t1 arrow-f = arrow-f
44bd77c80555 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 461 diff changeset	32 _×_ {_} {_} {t0} {t1} {t1} id-t1 arrow-g = arrow-g
44bd77c80555 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 461 diff changeset	33 _×_ {_} {_} {t1} {t1} {t1} id-t1 id-t1 = id-t1
44bd77c80555 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 461 diff changeset	34 _×_ {_} {_} {t0} {t0} {t1} arrow-f id-t0 = arrow-f
44bd77c80555 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 461 diff changeset	35 _×_ {_} {_} {t0} {t0} {t1} arrow-g id-t0 = arrow-g
44bd77c80555 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 461 diff changeset	36 _×_ {_} {_} {t0} {t0} {t0} id-t0 id-t0 = id-t0
448 c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	37
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	38 open TwoHom
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	39
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	40 -- f g h
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	41 -- d <- c <- b <- a
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	42 --
455 55a9b6177ed4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 454 diff changeset	43 -- It can be proved without TwoHom constraints
448 c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	44
c2616de4d208 discrete again with negation Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	45 assoc-× : {c₁ c₂ : Level } {a b c d : TwoObject {c₁} }
466 44bd77c80555 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 461 diff changeset	46 {f : (TwoHom {c₁} {c₂ } 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	47 ( f × (g × h)) ≡ ((f × g) × h )
466 44bd77c80555 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 461 diff changeset	48 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} { id-t0 }{ id-t0 }{ id-t0 } = refl
44bd77c80555 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 461 diff changeset	49 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} { arrow-f }{ id-t0 }{ id-t0 } = refl
44bd77c80555 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 461 diff changeset	50 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} { arrow-g }{ id-t0 }{ id-t0 } = refl
44bd77c80555 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 461 diff changeset	51 assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} { id-t1 }{ arrow-f }{ id-t0 } = refl
44bd77c80555 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 461 diff changeset	52 assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} { id-t1 }{ arrow-g }{ id-t0 } = refl
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 456 diff changeset	53 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} { id-t1 }{ id-t1 }{ arrow-f } = refl
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 456 diff changeset	54 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} { id-t1 }{ id-t1 }{ arrow-g } = refl
466 44bd77c80555 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 461 diff changeset	55 assoc-× {c₁} {c₂} {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	56
156e64d1bce0 on goinhg ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 448 diff changeset	57 TwoId : {c₁ c₂ : Level } (a : TwoObject {c₁} ) → (TwoHom {c₁} {c₂ } a a )
455 55a9b6177ed4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 454 diff changeset	58 TwoId {_} {_} t0 = id-t0
55a9b6177ed4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 454 diff changeset	59 TwoId {_} {_} t1 = id-t1
449 156e64d1bce0 on goinhg ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 448 diff changeset	60
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	61 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	62
455 55a9b6177ed4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 454 diff changeset	63 TwoCat : {c₁ c₂ : Level } → Category c₁ c₂ c₂
55a9b6177ed4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 454 diff changeset	64 TwoCat {c₁} {c₂} = record {
461 8436a018f88a clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 458 diff changeset	65 Obj = TwoObject ;
8436a018f88a clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 458 diff changeset	66 Hom = λ a b → TwoHom a b ;
449 156e64d1bce0 on goinhg ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 448 diff changeset	67 _o_ = λ{a} {b} {c} x y → _×_ {c₁ } { c₂} {a} {b} {c} x y ;
455 55a9b6177ed4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 454 diff changeset	68 _≈_ = λ x y → x ≡ y ;
461 8436a018f88a clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 458 diff changeset	69 Id = λ{a} → TwoId a ;
449 156e64d1bce0 on goinhg ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 448 diff changeset	70 isCategory = record {
453 3c2ce4474d92 try incomplete pattern for discrete Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 451 diff changeset	71 isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ;
449 156e64d1bce0 on goinhg ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 448 diff changeset	72 identityL = λ{a b f} → identityL {c₁} {c₂ } {a} {b} {f} ;
156e64d1bce0 on goinhg ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 448 diff changeset	73 identityR = λ{a b f} → identityR {c₁} {c₂ } {a} {b} {f} ;
156e64d1bce0 on goinhg ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 448 diff changeset	74 o-resp-≈ = λ{a b c f g h i} → o-resp-≈ {c₁} {c₂ } {a} {b} {c} {f} {g} {h} {i} ;
156e64d1bce0 on goinhg ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 448 diff changeset	75 associative = λ{a b c d f g h } → assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h}
156e64d1bce0 on goinhg ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 448 diff changeset	76 }
156e64d1bce0 on goinhg ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 448 diff changeset	77 } where
455 55a9b6177ed4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 454 diff changeset	78 identityL : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → ((TwoId B) × f) ≡ f
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 456 diff changeset	79 identityL {c₁} {c₂} {t1} {t1} { id-t1 } = refl
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 456 diff changeset	80 identityL {c₁} {c₂} {t0} {t0} { id-t0 } = refl
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 456 diff changeset	81 identityL {c₁} {c₂} {t0} {t1} { arrow-f } = refl
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 456 diff changeset	82 identityL {c₁} {c₂} {t0} {t1} { arrow-g } = refl
455 55a9b6177ed4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 454 diff changeset	83 identityR : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → ( f × TwoId A ) ≡ f
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 456 diff changeset	84 identityR {c₁} {c₂} {t1} {t1} { id-t1 } = refl
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 456 diff changeset	85 identityR {c₁} {c₂} {t0} {t0} { id-t0 } = refl
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 456 diff changeset	86 identityR {c₁} {c₂} {t0} {t1} { arrow-f } = refl
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 456 diff changeset	87 identityR {c₁} {c₂} {t0} {t1} { arrow-g } = refl
449 156e64d1bce0 on goinhg ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 448 diff changeset	88 o-resp-≈ : {c₁ c₂ : Level } {A B C : TwoObject {c₁} } {f g : ( TwoHom {c₁} {c₂ } A B)} {h i : ( TwoHom B C)} →
455 55a9b6177ed4 on going ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 454 diff changeset	89 f ≡ g → h ≡ i → ( h × f ) ≡ ( i × g )
461 8436a018f88a clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 458 diff changeset	90 o-resp-≈ {c₁} {c₂} {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	91
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	92
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	93 -- 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	94
469 65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	95 record DiscreteObj {c₁ : Level } (S : Set c₁) : Set c₁ where
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	96 field
475 4c0a955b651d add license Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 474 diff changeset	97 obj : S -- this is necessary to avoid single object
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	98
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	99 open DiscreteObj
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	100
469 65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	101 record DiscreteHom { c₁ : Level} { S : Set c₁} (a : DiscreteObj {c₁} S) (b : DiscreteObj {c₁} S)
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	102 : 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	103 field
474 2d32ded94aaf clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 472 diff changeset	104 discrete : a ≡ b -- if f : a → b then a ≡ b
472 f3d6d0275a0a discrete equality as a dom equality Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 469 diff changeset	105 dom : DiscreteObj S
f3d6d0275a0a discrete equality as a dom equality Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 469 diff changeset	106 dom = a
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	107
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	108 open DiscreteHom
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	109
469 65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	110 _*_ : ∀ {c₁} → {S : Set c₁} {a b c : DiscreteObj {c₁} S} → DiscreteHom {c₁} b c → DiscreteHom {c₁} a b → DiscreteHom {c₁} a c
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	111 _*_ {_} {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	112
469 65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	113 DiscreteId : { c₁ : Level} { S : Set c₁} ( a : DiscreteObj {c₁} S ) → DiscreteHom {c₁} a a
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	114 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	115
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	116 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	117
469 65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	118 assoc-* : {c₁ : Level } { S : Set c₁} {a b c d : DiscreteObj {c₁} S}
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	119 {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	120 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	121 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	122
469 65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	123 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	124 DiscreteCat {c₁} S = record {
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	125 Obj = DiscreteObj {c₁} S ;
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	126 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	127 _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	128 _≈_ = λ 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	129 Id = λ{a} → DiscreteId a ;
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	130 isCategory = record {
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	131 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	132 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	133 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	134 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	135 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	136 }
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	137 } where
472 f3d6d0275a0a discrete equality as a dom equality Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 469 diff changeset	138 identityL : {a b : DiscreteObj {c₁} S} {f : ( DiscreteHom {c₁} a b) } → dom ((DiscreteId b) * f) ≡ dom f
f3d6d0275a0a discrete equality as a dom equality Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 469 diff changeset	139 identityL {a} {b} {f} = refl
f3d6d0275a0a discrete equality as a dom equality Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 469 diff changeset	140 identityR : {A B : DiscreteObj S} {f : ( DiscreteHom {c₁} A B) } → dom ( f * DiscreteId A ) ≡ dom f
f3d6d0275a0a discrete equality as a dom equality Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 469 diff changeset	141 identityR {a} {b} {f} = refl
469 65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	142 o-resp-≈ : {A B C : DiscreteObj 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	143 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	144 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	145
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	146
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	147
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	148
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	149
472 f3d6d0275a0a discrete equality as a dom equality Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 469 diff changeset	150

Mercurial > hg > Members > kono > Proof > category

annotate discrete.agda @ 767:0f8e3b962c13