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

annotate discrete.agda @ 790:1e7319868d77

Sets is CCC

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Fri, 19 Apr 2019 23:42:19 +0900
parents	340708e8d54f
children	82a8c1ab4ef5

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

Mercurial > hg > Members > kono > Proof > category

annotate discrete.agda @ 790:1e7319868d77