Mercurial > hg > Members > kono > Proof > category

annotate limit-to.agda @ 433:25478a0ba66b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
functor constraint does not work well on distribution law
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 26 Mar 2016 20:00:34 +0900
parents 688066ac172e
children 3fdf0aedc21d
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
415
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
1 open import Category -- https://github.com/konn/category-agda
350
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Level
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3
403
375edfefbf6a maybe CAT
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 402
diff changeset
4 module limit-to where
350
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import cat-utility
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import HomReasoning
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 open import Relation.Binary.Core
401
e4c10d6375f6 Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 400
diff changeset
9 open import Data.Maybe
350
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open Functor
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
401
e4c10d6375f6 Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 400
diff changeset
13
e4c10d6375f6 Maybe Category to-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 400
diff changeset
14
415
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
15 -- If we have limit then we have equalizer
350
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 --- two objects category
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 ---
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 --- f
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
19 --- -----→
350
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 --- 0 1
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
21 --- -----→
366
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
22 --- g
387
2f59c2db9d98 what is this ?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
23
350
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 354
diff changeset
25
385
ff3803fc0c8a add level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 384
diff changeset
26 data TwoObject {c₁ : Level} : Set c₁ where
415
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
27 t0 : TwoObject
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
28 t1 : TwoObject
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
29
424
4329525f5085 fix imit-to-edu for MaybeCat / TwoCat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 423
diff changeset
30 -- constrainted arrow
4329525f5085 fix imit-to-edu for MaybeCat / TwoCat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 423
diff changeset
31 -- we need inverse of f to complete cases
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
32 data Arrow {c₁ c₂ : Level } ( t00 t11 : TwoObject {c₁} ) : TwoObject {c₁} → TwoObject {c₁} → Set c₂ where
417
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
33 id-t0 : Arrow t00 t11 t00 t00
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
34 id-t1 : Arrow t00 t11 t11 t11
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
35 arrow-f : Arrow t00 t11 t00 t11
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
36 arrow-g : Arrow t00 t11 t00 t11
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
37 inv-f : Arrow t00 t11 t11 t00
415
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
38
417
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
39 record TwoHom {c₁ c₂ : Level} (a b : TwoObject {c₁} ) : Set c₂ where
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
40 field
422
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
41 hom : Maybe ( Arrow {c₁} {c₂} t0 t1 a b )
417
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
42
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
43 open TwoHom
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
44
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
45 -- arrow composition
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
46
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
47
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
48 comp : ∀ {c₁ c₂} → {a b c : TwoObject {c₁}} → Maybe ( Arrow {c₁} {c₂} t0 t1 b c ) → Maybe ( Arrow {c₁} {c₂} t0 t1 a b ) → Maybe ( Arrow {c₁} {c₂} t0 t1 a c )
422
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
49 comp {_} {_} {_} {_} {_} nothing _ = nothing
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
50 comp {_} {_} {_} {_} {_} (just _ ) nothing = nothing
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
51 comp {_} {_} {t0} {t1} {t1} (just id-t1 ) ( just arrow-f ) = just arrow-f
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
52 comp {_} {_} {t0} {t1} {t1} (just id-t1 ) ( just arrow-g ) = just arrow-g
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
53 comp {_} {_} {t1} {t1} {t1} (just id-t1 ) ( just id-t1 ) = just id-t1
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
54 comp {_} {_} {t1} {t1} {t0} (just inv-f ) ( just id-t1 ) = just inv-f
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
55 comp {_} {_} {t0} {t0} {t1} (just arrow-f ) ( just id-t0 ) = just arrow-f
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
56 comp {_} {_} {t0} {t0} {t1} (just arrow-g ) ( just id-t0 ) = just arrow-g
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
57 comp {_} {_} {t0} {t0} {t0} (just id-t0 ) ( just id-t0 ) = just id-t0
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
58 comp {_} {_} {t1} {t0} {t0} (just id-t0 ) ( just inv-f ) = just inv-f
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
59 comp {_} {_} {_} {_} {_} (just _ ) ( just _ ) = nothing
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
60
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
61
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
62 _×_ : ∀ {c₁ c₂} → {a b c : TwoObject {c₁}} → ( TwoHom {c₁} {c₂} b c ) → ( TwoHom {c₁} {c₂} a b ) → ( TwoHom {c₁} {c₂} a c )
422
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
63 _×_ {c₁} {c₂} {a} {b} {c} f g = record { hom = comp {c₁} {c₂} {a} {b} {c} (hom f) (hom g ) }
417
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
64
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
65
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
66 _==_ : ∀{ c₁ c₂ a b } → Rel (Maybe (Arrow {c₁} {c₂} t0 t1 a b )) (c₂)
417
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
67 _==_ = Eq _≡_
414
28249d32b700 Maybe does not help conflict ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 413
diff changeset
68
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
69 map2hom : ∀{ c₁ c₂ } → {a b : TwoObject {c₁}} → Maybe ( Arrow {c₁} {c₂} t0 t1 a b ) → TwoHom {c₁} {c₂ } a b
422
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
70 map2hom {_} {_} {t1} {t1} (just id-t1) = record { hom = just id-t1 }
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
71 map2hom {_} {_} {t0} {t1} (just arrow-f) = record { hom = just arrow-f }
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
72 map2hom {_} {_} {t0} {t1} (just arrow-g) = record { hom = just arrow-g }
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
73 map2hom {_} {_} {t0} {t0} (just id-t0) = record { hom = just id-t0 }
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
74 map2hom {_} {_} {_} {_} _ = record { hom = nothing }
417
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
75
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
76 record TwoHom1 {c₁ c₂ : Level} (a : TwoObject {c₁} ) (b : TwoObject {c₁} ) : Set c₂ where
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
77 field
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
78 Map : TwoHom {c₁} {c₂ } a b
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
79 iso-Map : Map ≡ map2hom ( hom Map )
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
80
422
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
81 open TwoHom1
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
82
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
83 ==refl : ∀{ c₁ c₂ a b } → ∀ {x : Maybe (Arrow {c₁} {c₂} t0 t1 a b )} → x == x
417
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
84 ==refl {_} {_} {_} {_} {just x} = just refl
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
85 ==refl {_} {_} {_} {_} {nothing} = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
86
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
87 ==sym : ∀{ c₁ c₂ a b } → ∀ {x y : Maybe (Arrow {c₁} {c₂} t0 t1 a b )} → x == y → y == x
417
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
88 ==sym (just x≈y) = just (≡-sym x≈y)
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
89 ==sym nothing = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
90
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
91 ==trans : ∀{ c₁ c₂ a b } → ∀ {x y z : Maybe (Arrow {c₁} {c₂} t0 t1 a b ) } →
417
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
92 x == y → y == z → x == z
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
93 ==trans (just x≈y) (just y≈z) = just (≡-trans x≈y y≈z)
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
94 ==trans nothing nothing = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
95
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
96 ==cong : ∀{ c₁ c₂ a b c d } → ∀ {x y : Maybe (Arrow {c₁} {c₂} t0 t1 a b )} →
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
97 (f : Maybe (Arrow {c₁} {c₂} t0 t1 a b ) → Maybe (Arrow {c₁} {c₂} t0 t1 c d ) ) → x == y → f x == f y
422
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
98 ==cong { c₁} {c₂} {a} {b } {c} {d} {nothing} {nothing} f nothing = ==refl
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
99 ==cong { c₁} {c₂} {a} {b } {c} {d} {just x} {just .x} f (just refl) = ==refl
420
3e44951b9bdb refl in free-monoid trouble
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 419
diff changeset
100
417
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
101
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
102 module ==-Reasoning {c₁ c₂ : Level} where
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
103
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
104 infixr 2 _∎
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
105 infixr 2 _==⟨_⟩_ _==⟨⟩_
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
106 infix 1 begin_
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
107
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
108
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
109 data _IsRelatedTo_ {c₁ c₂ : Level} {a b : TwoObject {c₁} } (x y : (Maybe (Arrow {c₁} {c₂} t0 t1 a b ))) :
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
110 Set c₂ where
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
111 relTo : (x≈y : x == y ) → x IsRelatedTo y
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
112
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
113 begin_ : { a b : TwoObject {c₁} } {x : Maybe (Arrow {c₁} {c₂} t0 t1 a b ) } {y : Maybe (Arrow {c₁} {c₂} t0 t1 a b )} →
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
114 x IsRelatedTo y → x == y
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
115 begin relTo x≈y = x≈y
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
116
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
117 _==⟨_⟩_ : { a b : TwoObject {c₁} } (x : Maybe (Arrow {c₁} {c₂} t0 t1 a b )) {y z : Maybe (Arrow {c₁} {c₂} t0 t1 a b ) } →
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
118 x == y → y IsRelatedTo z → x IsRelatedTo z
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
119 _ ==⟨ x≈y ⟩ relTo y≈z = relTo (==trans x≈y y≈z)
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
120
422
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
121
417
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
122 _==⟨⟩_ : { a b : TwoObject {c₁} }(x : Maybe (Arrow {c₁} {c₂} t0 t1 a b )) {y : Maybe (Arrow {c₁} {c₂} t0 t1 a b )}
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
123 → x IsRelatedTo y → x IsRelatedTo y
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
124 _ ==⟨⟩ x≈y = x≈y
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
125
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
126 _∎ : { a b : TwoObject {c₁} }(x : Maybe (Arrow {c₁} {c₂} t0 t1 a b )) → x IsRelatedTo x
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
127 _∎ _ = relTo ==refl
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
128
410
508c88223aab add reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 409
diff changeset
129
422
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
130 -- TwoHom1Eq : {c₁ c₂ : Level } {a b : TwoObject {c₁} } {f g : ( TwoHom1 {c₁} {c₂ } a b)} →
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
131 -- hom (Map f) == hom (Map g) → f == g
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
132 -- TwoHom1Eq = ?
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
133
406
2fbd92ddecb5 non recorded arrow does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 405
diff changeset
134
417
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
135 -- f g h
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
136 -- d <- c <- b <- a
420
3e44951b9bdb refl in free-monoid trouble
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 419
diff changeset
137 --
3e44951b9bdb refl in free-monoid trouble
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 419
diff changeset
138 -- It can be proved without Arrow constraints
417
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
139
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
140 assoc-× : {c₁ c₂ : Level } {a b c d : TwoObject {c₁} }
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
141 {f : (TwoHom {c₁} {c₂ } c d )} →
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
142 {g : (TwoHom {c₁} {c₂ } b c )} →
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
143 {h : (TwoHom {c₁} {c₂ } a b )} →
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
144 hom ( f × (g × h)) == hom ((f × g) × h )
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
145 assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h} with hom f | hom g | hom h
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
146 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} {f} {g} {h} | nothing | _ | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
147 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | nothing | _ | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
148 assoc-× {c₁} {c₂} {t0} {t0} {t1} {t0} {f} {g} {h} | nothing | _ | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
149 assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | nothing | _ | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
150 assoc-× {c₁} {c₂} {t0} {t1} {t0} {t0} {f} {g} {h} | nothing | _ | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
151 assoc-× {c₁} {c₂} {t0} {t1} {t0} {t1} {f} {g} {h} | nothing | _ | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
152 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t0} {f} {g} {h} | nothing | _ | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
153 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | nothing | _ | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
154 assoc-× {c₁} {c₂} {t1} {t0} {t0} {t0} {f} {g} {h} | nothing | _ | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
155 assoc-× {c₁} {c₂} {t1} {t0} {t0} {t1} {f} {g} {h} | nothing | _ | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
156 assoc-× {c₁} {c₂} {t1} {t0} {t1} {t0} {f} {g} {h} | nothing | _ | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
157 assoc-× {c₁} {c₂} {t1} {t0} {t1} {t1} {f} {g} {h} | nothing | _ | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
158 assoc-× {c₁} {c₂} {t1} {t1} {t0} {t0} {f} {g} {h} | nothing | _ | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
159 assoc-× {c₁} {c₂} {t1} {t1} {t0} {t1} {f} {g} {h} | nothing | _ | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
160 assoc-× {c₁} {c₂} {t1} {t1} {t1} {t0} {f} {g} {h} | nothing | _ | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
161 assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} {f} {g} {h} | nothing | _ | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
162 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} {f} {g} {h} | just _ | nothing | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
163 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just _ | nothing | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
164 assoc-× {c₁} {c₂} {t0} {t0} {t1} {t0} {f} {g} {h} | just _ | nothing | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
165 assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just _ | nothing | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
166 assoc-× {c₁} {c₂} {t0} {t1} {t0} {t0} {f} {g} {h} | just _ | nothing | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
167 assoc-× {c₁} {c₂} {t0} {t1} {t0} {t1} {f} {g} {h} | just _ | nothing | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
168 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t0} {f} {g} {h} | just _ | nothing | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
169 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | just _ | nothing | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
170 assoc-× {c₁} {c₂} {t1} {t0} {t0} {t0} {f} {g} {h} | just _ | nothing | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
171 assoc-× {c₁} {c₂} {t1} {t0} {t0} {t1} {f} {g} {h} | just _ | nothing | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
172 assoc-× {c₁} {c₂} {t1} {t0} {t1} {t0} {f} {g} {h} | just _ | nothing | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
173 assoc-× {c₁} {c₂} {t1} {t0} {t1} {t1} {f} {g} {h} | just _ | nothing | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
174 assoc-× {c₁} {c₂} {t1} {t1} {t0} {t0} {f} {g} {h} | just _ | nothing | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
175 assoc-× {c₁} {c₂} {t1} {t1} {t0} {t1} {f} {g} {h} | just _ | nothing | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
176 assoc-× {c₁} {c₂} {t1} {t1} {t1} {t0} {f} {g} {h} | just _ | nothing | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
177 assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} {f} {g} {h} | just _ | nothing | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
178 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} {f} {g} {h} | just id-t0 | just id-t0 | just id-t0 = ==refl
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
179 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just arrow-f | just id-t0 | just id-t0 = ==refl
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
180 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just arrow-g | just id-t0 | just id-t0 = ==refl
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
181 assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-f | just id-t0 = ==refl
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
182 assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-g | just id-t0 = ==refl
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
183 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | just id-t1 | just id-t1 | just arrow-f = ==refl
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
184 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | just id-t1 | just id-t1 | just arrow-g = ==refl
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
185 assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} {f} {g} {h} | just id-t1 | just id-t1 | just id-t1 = ==refl
424
4329525f5085 fix imit-to-edu for MaybeCat / TwoCat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 423
diff changeset
186 -- remaining all failure case (except inf-f case )
418
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
187 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} {f} {g} {h} | just id-t0 | just id-t0 | nothing = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
188 assoc-× {c₁} {c₂} {t1} {t0} {t0} {t0} {f} {g} {h} | just id-t0 | just id-t0 | nothing = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
189 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | just id-t1 | just id-t1 | nothing = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
190 assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} {f} {g} {h} | just id-t1 | just id-t1 | nothing = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
191 assoc-× {c₁} {c₂} {t0} {t1} {t0} {t0} {f} {g} {h} | just id-t0 | just inv-f | nothing = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
192 assoc-× {c₁} {c₂} {t1} {t1} {t0} {t0} {f} {g} {h} | just id-t0 | just inv-f | nothing = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
193 assoc-× {c₁} {c₂} {t1} {t0} {t0} {t1} {f} {g} {h} | just arrow-f | just id-t0 | nothing = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
194 assoc-× {c₁} {c₂} {t1} {t0} {t0} {t1} {f} {g} {h} | just arrow-g | just id-t0 | nothing = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
195 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just arrow-f | just id-t0 | nothing = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
196 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just arrow-g | just id-t0 | nothing = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
197 assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-f | nothing = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
198 assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-g | nothing = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
199 assoc-× {c₁} {c₂} {t1} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-f | nothing = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
200 assoc-× {c₁} {c₂} {t1} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-g | nothing = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
201 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t0} {f} {g} {h} | just inv-f | just id-t1 | nothing = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
202 assoc-× {c₁} {c₂} {t1} {t1} {t1} {t0} {f} {g} {h} | just inv-f | just id-t1 | nothing = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
203 assoc-× {_} {_} {t0} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just _) | nothing = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
204 assoc-× {_} {_} {t0} {t1} {t0} {t1} {_} {_} {_} | (just _) | (just _) | nothing = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
205 assoc-× {_} {_} {t1} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just _) | nothing = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
206 assoc-× {_} {_} {t1} {t1} {t0} {t1} {_} {_} {_} | (just _) | (just _) | nothing = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
207 assoc-× {_} {_} {t0} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just arrow-f) | (just id-t0) = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
208 assoc-× {_} {_} {t0} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just arrow-g) | (just id-t0) = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
209 assoc-× {_} {_} {t0} {t1} {t0} {t0} {_} {_} {_} | (just id-t0) | (just inv-f) | (just _) = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
210 assoc-× {_} {_} {t0} {t1} {t0} {t1} {_} {_} {_} | (just _) | (just _) | (just _) = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
211 assoc-× {_} {_} {t0} {t1} {t1} {t0} {_} {_} {_} | (just inv-f) | (just id-t1) | (just arrow-f) = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
212 assoc-× {_} {_} {t0} {t1} {t1} {t0} {_} {_} {_} | (just inv-f) | (just id-t1) | (just arrow-g) = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
213 assoc-× {_} {_} {t1} {t0} {t0} {t0} {_} {_} {_} | (just id-t0) | (just id-t0) | (just inv-f) = ==refl
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
214 assoc-× {_} {_} {t1} {t0} {t0} {t1} {_} {_} {_} | (just arrow-f) | (just id-t0) | (just inv-f) = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
215 assoc-× {_} {_} {t1} {t0} {t0} {t1} {_} {_} {_} | (just arrow-g) | (just id-t0) | (just inv-f) = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
216 assoc-× {_} {_} {t1} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just _) | (just _) = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
217 assoc-× {_} {_} {t1} {t0} {t1} {t1} {_} {_} {_} | (just id-t1) | (just arrow-f) | (just _) = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
218 assoc-× {_} {_} {t1} {t0} {t1} {t1} {_} {_} {_} | (just id-t1) | (just arrow-g) | (just _) = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
219 assoc-× {_} {_} {t1} {t1} {t0} {t0} {_} {_} {_} | (just id-t0) | (just inv-f) | (just id-t1) = ==refl
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
220 assoc-× {_} {_} {t1} {t1} {t0} {t1} {_} {_} {_} | (just arrow-f) | (just inv-f) | (just id-t1) = ==refl
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
221 assoc-× {_} {_} {t1} {t1} {t0} {t1} {_} {_} {_} | (just arrow-g) | (just inv-f) | (just id-t1) = ==refl
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
222 assoc-× {_} {_} {t1} {t1} {t1} {t0} {_} {_} {_} | (just inv-f) | (just id-t1) | (just id-t1) = ==refl
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
223
404
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 403
diff changeset
224
409
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 408
diff changeset
225
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
226 TwoId : {c₁ c₂ : Level } (a : TwoObject {c₁} ) → (TwoHom {c₁} {c₂ } a a )
422
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
227 TwoId {_} {_} t0 = record { hom = just id-t0 }
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
228 TwoId {_} {_} t1 = record { hom = just id-t1 }
417
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
229
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
230 open import maybeCat
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
231
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
232 -- identityL {c₁} {c₂} {_} {b} {nothing} = let open ==-Reasoning {c₁} {c₂} in
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
233 -- begin
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
234 -- (TwoId b × nothing)
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
235 -- ==⟨ {!!} ⟩
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
236 -- nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
237 -- ∎
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
238
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
239 open import Relation.Binary
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
240 TwoCat : {c₁ c₂ ℓ : Level } → Category c₁ c₂ c₂
417
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
241 TwoCat {c₁} {c₂} {ℓ} = record {
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
242 Obj = TwoObject {c₁} ;
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
243 Hom = λ a b → ( TwoHom {c₁} {c₂ } a b ) ;
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
244 _o_ = λ{a} {b} {c} x y → _×_ {c₁ } { c₂} {a} {b} {c} x y ;
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
245 _≈_ = λ x y → hom x == hom y ;
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
246 Id = λ{a} → TwoId {c₁ } { c₂} a ;
417
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
247 isCategory = record {
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
248 isEquivalence = record {refl = ==refl ; trans = ==trans ; sym = ==sym } ;
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
249 identityL = λ{a b f} → identityL {c₁} {c₂ } {a} {b} {f} ;
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
250 identityR = λ{a b f} → identityR {c₁} {c₂ } {a} {b} {f} ;
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
251 o-resp-≈ = λ{a b c f g h i} → o-resp-≈ {c₁} {c₂ } {a} {b} {c} {f} {g} {h} {i} ;
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
252 associative = λ{a b c d f g h } → assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h}
417
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
253 }
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
254 } where
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
255 identityL : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → hom ((TwoId B) × f) == hom f
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
256 identityL {c₁} {c₂} {_} {_} {f} with hom f
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
257 identityL {c₁} {c₂} {t0} {t0} {_} | nothing = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
258 identityL {c₁} {c₂} {t0} {t1} {_} | nothing = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
259 identityL {c₁} {c₂} {t1} {t0} {_} | nothing = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
260 identityL {c₁} {c₂} {t1} {t1} {_} | nothing = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
261 identityL {c₁} {c₂} {t1} {t0} {_} | just inv-f = ==refl
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
262 identityL {c₁} {c₂} {t1} {t1} {_} | just id-t1 = ==refl
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
263 identityL {c₁} {c₂} {t0} {t0} {_} | just id-t0 = ==refl
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
264 identityL {c₁} {c₂} {t0} {t1} {_} | just arrow-f = ==refl
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
265 identityL {c₁} {c₂} {t0} {t1} {_} | just arrow-g = ==refl
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
266 identityR : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → hom ( f × TwoId A ) == hom f
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
267 identityR {c₁} {c₂} {_} {_} {f} with hom f
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
268 identityR {c₁} {c₂} {t0} {t0} {_} | nothing = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
269 identityR {c₁} {c₂} {t0} {t1} {_} | nothing = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
270 identityR {c₁} {c₂} {t1} {t0} {_} | nothing = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
271 identityR {c₁} {c₂} {t1} {t1} {_} | nothing = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
272 identityR {c₁} {c₂} {t1} {t0} {_} | just inv-f = ==refl
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
273 identityR {c₁} {c₂} {t1} {t1} {_} | just id-t1 = ==refl
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
274 identityR {c₁} {c₂} {t0} {t0} {_} | just id-t0 = ==refl
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
275 identityR {c₁} {c₂} {t0} {t1} {_} | just arrow-f = ==refl
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
276 identityR {c₁} {c₂} {t0} {t1} {_} | just arrow-g = ==refl
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
277 o-resp-≈ : {c₁ c₂ : Level } {A B C : TwoObject {c₁} } {f g : ( TwoHom {c₁} {c₂ } A B)} {h i : ( TwoHom B C)} →
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
278 hom f == hom g → hom h == hom i → hom ( h × f ) == hom ( i × g )
422
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
279 o-resp-≈ {c₁} {c₂} {a} {b} {c} {f} {g} {h} {i} f==g h==i =
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
280 let open ==-Reasoning {c₁} {c₂ } in begin
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
281 hom ( h × f )
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
282 ==⟨⟩
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
283 comp (hom h) (hom f)
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
284 ==⟨ ==cong (λ x → comp ( hom h ) x ) f==g ⟩
422
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
285 comp (hom h) (hom g)
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
286 ==⟨ ==cong (λ x → comp x ( hom g ) ) h==i ⟩
422
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
287 comp (hom i) (hom g)
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
288 ==⟨⟩
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
289 hom ( i × g )
3a4a99a8edbe o-resp passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
290 ∎
420
3e44951b9bdb refl in free-monoid trouble
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 419
diff changeset
291
426
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
292 record Nil {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
293 field
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
294 nil : {a b : Obj A } → Hom A a b
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
295 nil-id : {a : Obj A } → A [ nil {a} {a} ≈ id1 A a ]
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
296 nil-idL : {a b c : Obj A } → { f : Hom A a b } → A [ A [ nil {b} {c} o f ] ≈ nil {a} {c} ]
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
297 nil-idR : {a b c : Obj A } → { f : Hom A b c } → A [ A [ f o nil {a} {b} ] ≈ nil {a} {c} ]
426
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
298
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
299 open Nil
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
300
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
301 justFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → Nil A → Functor (MaybeCat A ) A
426
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
302 justFunctor{c₁} {c₂} {ℓ} A none = record {
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
303 FObj = λ a → fobj a
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
304 ; FMap = λ {a} {b} f → fmap {a} {b} f
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
305 ; isFunctor = record {
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
306 identity = λ{x} → identity {x}
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
307 ; distr = λ {a} {b} {c} {f} {g} → distr2 {a} {b} {c} {f} {g}
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
308 ; ≈-cong = λ {a} {b} {c} {f} → ≈-cong {a} {b} {c} {f}
426
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
309 }
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
310 } where
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
311 MA = MaybeCat A
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
312 fobj : Obj MA → Obj A
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
313 fobj = λ x → x
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
314 fmap : {x y : Obj MA } → Hom MA x y → Hom A x y
426
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
315 fmap {x} {y} f with MaybeHom.hom f
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
316 fmap {x} {y} _ | nothing = nil none
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
317 fmap {x} {y} _ | (just f) = f
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
318 identity : {x : Obj MA} → A [ fmap (id1 MA x) ≈ id1 A (fobj x) ]
426
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
319 identity = let open ≈-Reasoning (A) in refl-hom
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
320 distr2 : {a : Obj MA} {b : Obj MA} {c : Obj MA} {f : Hom MA a b} {g : Hom MA b c} → A [ fmap (MA [ g o f ]) ≈ A [ fmap g o fmap f ] ]
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
321 distr2 {a} {b} {c} {f} {g} with MaybeHom.hom f | MaybeHom.hom g
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
322 distr2 | nothing | nothing = let open ≈-Reasoning (A) in sym ( nil-idR none )
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
323 distr2 | nothing | just ga = let open ≈-Reasoning (A) in sym ( nil-idR none )
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
324 distr2 | just fa | nothing = let open ≈-Reasoning (A) in sym ( nil-idL none )
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
325 distr2 | just f | just g = let open ≈-Reasoning (A) in refl-hom
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
326 ≈-cong : {a : Obj MA} {b : Obj MA} {f g : Hom MA a b} → MA [ f ≈ g ] → A [ fmap f ≈ fmap g ]
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
327 ≈-cong {a} {b} {f} {g} eq with MaybeHom.hom f | MaybeHom.hom g
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
328 ≈-cong {a} {b} {f} {g} nothing | nothing | nothing = let open ≈-Reasoning (A) in refl-hom
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
329 ≈-cong {a} {b} {f} {g} (just eq) | just _ | just _ = eq
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
330
432
688066ac172e add another method as a comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 431
diff changeset
331 -- indexFunctor' : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (none : Nil A) ( a b : Obj A) ( f g : Hom A a b )
688066ac172e add another method as a comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 431
diff changeset
332 -- → ( obj→ : Obj A -> TwoObject {c₁} )
688066ac172e add another method as a comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 431
diff changeset
333 -- → ( hom→ : { a b : Obj A } -> Hom A a b -> Arrow t0 t0 (obj→ a) (obj→ b) )
688066ac172e add another method as a comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 431
diff changeset
334 -- → ( { x y : Obj A } { h i : Hom A x y } -> A [ h ≈ i ] → hom→ h ≡ hom→ i )
688066ac172e add another method as a comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 431
diff changeset
335 -- → Functor A A
433
25478a0ba66b functor constraint does not work well on distribution law
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 432
diff changeset
336 -- this one does not work on fmap ( g o f ) ≈ ( fmap g o fmap f )
25478a0ba66b functor constraint does not work well on distribution law
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 432
diff changeset
337 -- because g o f can be arrow-f when g is arrow-g
25478a0ba66b functor constraint does not work well on distribution law
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 432
diff changeset
338 -- ideneity and ≈-cong are easy
432
688066ac172e add another method as a comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 431
diff changeset
339
388
a0ab2643eee7 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 387
diff changeset
340
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
341 indexFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (none : Nil A) ( a b : Obj A) ( f g : Hom A a b ) → Functor (TwoCat {c₁} {c₂} {c₂} ) A
427
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
342 indexFunctor {c₁} {c₂} {ℓ} A none a b f g = record {
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
343 FObj = λ a → fobj a
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
344 ; FMap = λ {a} {b} f → fmap {a} {b} f
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
345 ; isFunctor = record {
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
346 identity = λ{x} → identity {x}
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
347 ; distr = λ {a} {b} {c} {f} {g} → distr1 {a} {b} {c} {f} {g}
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
348 ; ≈-cong = λ {a} {b} {c} {f} → ≈-cong {a} {b} {c} {f}
427
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
349 }
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
350 } where
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
351 I = TwoCat {c₁} {c₂} {ℓ}
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
352 fobj : Obj I → Obj A
427
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
353 fobj t0 = a
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
354 fobj t1 = b
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
355 fmap : {x y : Obj I } → (TwoHom {c₁} {c₂} x y ) → Hom A (fobj x) (fobj y)
427
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
356 fmap {x} {y} h with hom h
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
357 fmap {t0} {t0} h | just id-t0 = id1 A a
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
358 fmap {t1} {t1} h | just id-t1 = id1 A b
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
359 fmap {t0} {t1} h | just arrow-f = f
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
360 fmap {t0} {t1} h | just arrow-g = g
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
361 fmap {_} {_} h | _ = nil none
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
362 open ≈-Reasoning A
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
363 ≈-cong : {a : Obj I} {b : Obj I} {f g : Hom I a b} → I [ f ≈ g ] → A [ fmap f ≈ fmap g ]
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
364 ≈-cong {a} {b} {f1} {g1} f≈g with hom f1 | hom g1
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
365 ≈-cong {t0} {t0} {f1} {g1} nothing | nothing | nothing = refl-hom
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
366 ≈-cong {t0} {t1} {f1} {g1} nothing | nothing | nothing = refl-hom
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
367 ≈-cong {t1} {t0} {f1} {g1} nothing | nothing | nothing = refl-hom
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
368 ≈-cong {t1} {t1} {f1} {g1} nothing | nothing | nothing = refl-hom
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
369 ≈-cong {t0} {t0} {f1} {g1} (just refl) | just id-t0 | just id-t0 = refl-hom
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
370 ≈-cong {t1} {t1} {f1} {g1} (just refl) | just id-t1 | just id-t1 = refl-hom
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
371 ≈-cong {t0} {t1} {f1} {g1} (just refl) | just arrow-f | just arrow-f = refl-hom
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
372 ≈-cong {t0} {t1} {f1} {g1} (just refl) | just arrow-g | just arrow-g = refl-hom
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
373 ≈-cong {t1} {t0} {f1} {g1} (just refl) | just inv-f | just inv-f = refl-hom
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
374 identity : {x : Obj I} → A [ fmap ( id1 I x ) ≈ id1 A (fobj x) ]
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
375 identity {t0} = refl-hom
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
376 identity {t1} = refl-hom
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
377 distr1 : {a₁ : Obj I} {b₁ : Obj I} {c : Obj I} {f₁ : Hom I a₁ b₁} {g₁ : Hom I b₁ c} →
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
378 A [ fmap (I [ g₁ o f₁ ]) ≈ A [ fmap g₁ o fmap f₁ ] ]
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
379 distr1 {a1} {b1} {c1} {f1} {g1} with hom g1 | hom f1
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
380 distr1 {t0} {t0} {t0} {f1} {g1} | nothing | nothing = sym ( nil-idR none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
381 distr1 {t0} {t0} {t1} {f1} {g1} | nothing | nothing = sym ( nil-idR none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
382 distr1 {t0} {t1} {t0} {f1} {g1} | nothing | nothing = sym ( nil-idR none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
383 distr1 {t0} {t1} {t1} {f1} {g1} | nothing | nothing = sym ( nil-idR none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
384 distr1 {t1} {t0} {t0} {f1} {g1} | nothing | nothing = sym ( nil-idR none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
385 distr1 {t1} {t0} {t1} {f1} {g1} | nothing | nothing = sym ( nil-idR none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
386 distr1 {t1} {t1} {t0} {f1} {g1} | nothing | nothing = sym ( nil-idR none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
387 distr1 {t1} {t1} {t1} {f1} {g1} | nothing | nothing = sym ( nil-idR none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
388 distr1 {t0} {t0} {t0} {f1} {g1} | nothing | just id-t0 = sym ( nil-idL none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
389 distr1 {t0} {t0} {t1} {f1} {g1} | nothing | just id-t0 = sym ( nil-idL none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
390 distr1 {t1} {t1} {t0} {f1} {g1} | nothing | just id-t1 = sym ( nil-idL none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
391 distr1 {t1} {t1} {t1} {f1} {g1} | nothing | just id-t1 = sym ( nil-idL none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
392 distr1 {t0} {t1} {t1} {f1} {g1} | nothing | just arrow-f = sym ( nil-idL none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
393 distr1 {t0} {t1} {t0} {f1} {g1} | nothing | just arrow-f = sym ( nil-idL none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
394 distr1 {t0} {t1} {t1} {f1} {g1} | nothing | just arrow-g = sym ( nil-idL none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
395 distr1 {t0} {t1} {t0} {f1} {g1} | nothing | just arrow-g = sym ( nil-idL none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
396 distr1 {t1} {t0} {t0} {f1} {g1} | nothing | just inv-f = sym ( nil-idL none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
397 distr1 {t1} {t0} {t1} {f1} {g1} | nothing | just inv-f = sym ( nil-idL none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
398 distr1 {t0} {t0} {t0} {f1} {g1} | just id-t0 | nothing = sym ( nil-idR none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
399 distr1 {t1} {t0} {t0} {f1} {g1} | just id-t0 | nothing = sym ( nil-idR none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
400 distr1 {t0} {t1} {t1} {f1} {g1} | just id-t1 | nothing = sym ( nil-idR none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
401 distr1 {t1} {t1} {t1} {f1} {g1} | just id-t1 | nothing = sym ( nil-idR none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
402 distr1 {t0} {t0} {t1} {f1} {g1} | just arrow-f | nothing = sym ( nil-idR none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
403 distr1 {t1} {t0} {t1} {f1} {g1} | just arrow-f | nothing = sym ( nil-idR none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
404 distr1 {t0} {t0} {t1} {f1} {g1} | just arrow-g | nothing = sym ( nil-idR none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
405 distr1 {t1} {t0} {t1} {f1} {g1} | just arrow-g | nothing = sym ( nil-idR none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
406 distr1 {t0} {t1} {t0} {f1} {g1} | just inv-f | nothing = sym ( nil-idR none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
407 distr1 {t1} {t1} {t0} {f1} {g1} | just inv-f | nothing = sym ( nil-idR none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
408 distr1 {t0} {t0} {t0} {f1} {g1} | just id-t0 | just id-t0 = sym idL
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
409 distr1 {t1} {t0} {t0} {f1} {g1} | just id-t0 | just inv-f = sym idL
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
410 distr1 {t0} {t0} {t1} {f1} {g1} | just arrow-f | just id-t0 = sym idR
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
411 distr1 {t0} {t0} {t1} {f1} {g1} | just arrow-g | just id-t0 = sym idR
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
412 distr1 {t1} {t1} {t1} {f1} {g1} | just id-t1 | just id-t1 = sym idL
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
413 distr1 {t0} {t1} {t1} {f1} {g1} | just id-t1 | just arrow-f = sym idL
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
414 distr1 {t0} {t1} {t1} {f1} {g1} | just id-t1 | just arrow-g = sym idL
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
415 distr1 {t1} {t1} {t0} {f1} {g1} | just inv-f | just id-t1 = sym ( nil-idL none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
416 distr1 {t0} {t1} {t0} {_} {_} | (just inv-f) | (just _) = sym ( nil-idL none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
417 distr1 {t1} {t0} {t1} {_} {_} | (just arrow-f) | (just _) = sym ( nil-idR none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
418 distr1 {t1} {t0} {t1} {_} {_} | (just arrow-g) | (just _) = sym ( nil-idR none )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
419
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
420
365
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
421
387
2f59c2db9d98 what is this ?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
422 --- Equalizer
2f59c2db9d98 what is this ?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
423 --- f
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
424 --- e -----→
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
425 --- c -----→ a b
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
426 --- ^ / -----→
387
2f59c2db9d98 what is this ?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
427 --- |k h g
415
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
428 --- | /
426
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
429 --- | / ^
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
430 --- | / |
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
431 --- |/ | Γ
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
432 --- d _ |
432
688066ac172e add another method as a comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 431
diff changeset
433 --- |\ |
688066ac172e add another method as a comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 431
diff changeset
434 --- \ K af
688066ac172e add another method as a comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 431
diff changeset
435 --- \ -----→
688066ac172e add another method as a comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 431
diff changeset
436 --- \ t0 t1
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
437 --- -----→
426
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
438 --- ag
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
439 ---
1290d6876129 Functor MA → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 425
diff changeset
440 ---
387
2f59c2db9d98 what is this ?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
441
350
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
442 open Limit
352
f589e71875ea bad approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 351
diff changeset
443
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
444 I' : {c₁ c₂ ℓ : Level} → Category c₁ c₂ c₂
425
98811e927d4a define MA and I
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 424
diff changeset
445 I' {c₁} {c₂} {ℓ} = TwoCat {c₁} {c₂} {ℓ}
424
4329525f5085 fix imit-to-edu for MaybeCat / TwoCat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 423
diff changeset
446
427
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
447 lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( none : Nil A )
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
448 (lim : ( Γ : Functor (I' {c₁} {c₂} {ℓ}) A ) → {a0 : Obj A }
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
449 {u : NTrans I' A ( K A I' a0 ) Γ } → Limit A I' Γ a0 u ) -- completeness
415
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
450 → {a b c : Obj A} (f g : Hom A a b )
365
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
451 → (e : Hom A c a ) → (fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] ) → Equalizer A e f g
427
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
452 lim-to-equ {c₁} {c₂} {ℓ } A none lim {a} {b} {c} f g e fe=ge = record {
350
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
453 fe=ge = fe=ge
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
454 ; k = λ {d} h fh=gh → k {d} h fh=gh
373
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 372
diff changeset
455 ; ek=h = λ {d} {h} {fh=gh} → ek=h d h fh=gh
417
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
456 ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k'
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
457 } where
428
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 427
diff changeset
458 open ≈-Reasoning A
429
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
459 I : Category c₁ c₂ c₂
425
98811e927d4a define MA and I
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 424
diff changeset
460 I = I' {c₁} {c₂} {ℓ}
429
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
461 Γ : Functor I A
427
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
462 Γ = indexFunctor {c₁} {c₂} {ℓ} A none a b f g
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
463 nmap : (x : Obj I ) ( d : Obj (A) ) (h : Hom A d a ) → Hom A (FObj (K A I d) x) (FObj Γ x)
427
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
464 nmap x d h with x
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
465 ... | t0 = h
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
466 ... | t1 = A [ f o h ]
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
467 commute1 : {x y : Obj I} {f' : Hom I x y} (d : Obj A) (h : Hom A d a ) → A [ A [ f o h ] ≈ A [ g o h ] ]
427
531b739a1d7c add Nil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 426
diff changeset
468 → A [ A [ FMap Γ f' o nmap x d h ] ≈ A [ nmap y d h o FMap (K A I d) f' ] ]
429
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
469 commute1 {x} {y} {f'} d h fh=gh with hom f'
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
470 commute1 {t0} {t0} {f'} d h fh=gh | nothing = begin
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
471 nil none o h
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
472 ≈⟨ car ( nil-id none ) ⟩
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
473 id1 A a o h
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
474 ≈⟨ idL ⟩
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
475 h
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
476 ≈↑⟨ idR ⟩
428
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 427
diff changeset
477 h o id1 A d
429
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
478 ∎
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
479 commute1 {t0} {t1} {f'} d h fh=gh | nothing = begin
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
480 nil none o h
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
481 ≈↑⟨ car ( nil-idL none ) ⟩
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
482 (nil none o f ) o h
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
483 ≈⟨ car ( car ( nil-id none ) ) ⟩
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
484 (id1 A b o f ) o h
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
485 ≈⟨ car idL ⟩
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
486 f o h
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
487 ≈↑⟨ idR ⟩
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
488 (f o h ) o id1 A d
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
489 ∎
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
490 commute1 {t1} {t0} {f'} d h fh=gh | nothing = begin
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
491 nil none o ( f o h )
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
492 ≈⟨ assoc ⟩
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
493 ( nil none o f ) o h
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
494 ≈⟨ car ( nil-idL none ) ⟩
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
495 nil none o h
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
496 ≈⟨ car ( nil-id none ) ⟩
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
497 id1 A a o h
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
498 ≈⟨ idL ⟩
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
499 h
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
500 ≈↑⟨ idR ⟩
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
501 h o id1 A d
428
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 427
diff changeset
502 ∎
429
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
503 commute1 {t1} {t1} {f'} d h fh=gh | nothing = begin
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
504 nil none o ( f o h )
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
505 ≈⟨ car ( nil-id none ) ⟩
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
506 id1 A b o ( f o h )
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
507 ≈⟨ idL ⟩
428
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 427
diff changeset
508 f o h
429
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
509 ≈↑⟨ idR ⟩
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
510 ( f o h ) o id1 A d
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
511 ∎
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
512 commute1 {t1} {t0} {f'} d h fh=gh | just inv-f = begin
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
513 nil none o ( f o h )
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
514 ≈⟨ assoc ⟩
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
515 ( nil none o f ) o h
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
516 ≈⟨ car ( nil-idL none ) ⟩
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
517 nil none o h
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
518 ≈⟨ car ( nil-id none ) ⟩
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
519 id1 A a o h
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
520 ≈⟨ idL ⟩
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
521 h
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
522 ≈↑⟨ idR ⟩
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
523 h o id1 A d
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
524 ∎
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
525 commute1 {t0} {t1} {f'} d h fh=gh | just arrow-f = begin
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
526 f o h
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
527 ≈↑⟨ idR ⟩
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
528 (f o h ) o id1 A d
428
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 427
diff changeset
529 ∎
429
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
530 commute1 {t0} {t1} {f'} d h fh=gh | just arrow-g = begin
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
531 g o h
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
532 ≈↑⟨ fh=gh ⟩
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
533 f o h
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
534 ≈↑⟨ idR ⟩
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
535 (f o h ) o id1 A d
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
536 ∎
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
537 commute1 {t0} {t0} {f'} d h fh=gh | just id-t0 = begin
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
538 id1 A a o h
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
539 ≈⟨ idL ⟩
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
540 h
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
541 ≈↑⟨ idR ⟩
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
542 h o id1 A d
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
543 ∎
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
544 commute1 {t1} {t1} {f'} d h fh=gh | just id-t1 = begin
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
545 id1 A b o ( f o h )
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
546 ≈⟨ idL ⟩
428
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 427
diff changeset
547 f o h
429
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
548 ≈↑⟨ idR ⟩
02eefa110eae nat commute in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 428
diff changeset
549 ( f o h ) o id1 A d
428
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 427
diff changeset
550 ∎
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 427
diff changeset
551 nat1 : (d : Obj A) → (h : Hom A d a ) → A [ A [ f o h ] ≈ A [ g o h ] ] → NTrans I A (K A I d) Γ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 427
diff changeset
552 nat1 d h fh=gh = record {
415
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
553 TMap = λ x → nmap x d h ;
350
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
554 isNTrans = record {
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
555 commute = λ {x} {y} {f'} → commute1 {x} {y} {f'} d h fh=gh
350
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
556 }
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
557 }
430
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
558 eqlim = lim Γ {c} {nat1 c e fe=ge }
350
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
559 k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c
430
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
560 k {d} h fh=gh = limit eqlim d (nat1 d h fh=gh )
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
561 ek=h : (d : Obj A ) (h : Hom A d a ) → ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) → A [ A [ e o k h fh=gh ] ≈ h ]
430
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
562 ek=h d h fh=gh = begin
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
563 e o k h fh=gh
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
564 ≈⟨ t0f=t eqlim {d} {nat1 d h fh=gh} {t0} ⟩
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
565 h
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
566 ∎
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
567 uniq-nat : {i : Obj I} → (d : Obj A ) (h : Hom A d a ) ( k' : Hom A d c ) → A [ A [ e o k' ] ≈ h ] → A [ A [ nmap i c e o k' ] ≈ nmap i d h ]
430
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
568 uniq-nat {t0} d h k' ek'=h = begin
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
569 nmap t0 c e o k'
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
570 ≈⟨⟩
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
571 e o k'
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
572 ≈⟨ ek'=h ⟩
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
573 h
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
574 ≈⟨⟩
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
575 nmap t0 d h
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
576 ∎
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
577 uniq-nat {t1} d h k' ek'=h = begin
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
578 nmap t1 c e o k'
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
579 ≈⟨⟩
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
580 (f o e ) o k'
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
581 ≈↑⟨ assoc ⟩
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
582 f o ( e o k' )
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
583 ≈⟨ cdr ek'=h ⟩
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
584 f o h
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
585 ≈⟨⟩
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
586 nmap t1 d h
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
587 ∎
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
588 uniquness : (d : Obj A ) (h : Hom A d a ) → ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) →
372
b4855a3ebd34 add more lemma in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 371
diff changeset
589 ( k' : Hom A d c )
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
590 → A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ]
430
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
591 uniquness d h fh=gh k' ek'=h = begin
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
592 k h fh=gh
431
a15f52456c78 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 430
diff changeset
593 ≈⟨ limit-uniqueness eqlim {d} {nat1 d h fh=gh } {k'} ( λ{i} → uniq-nat {i} d h k' ek'=h ) ⟩
430
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
594 k'
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
595 ∎
368
b18585089d2e add more parameter to nat in lim-to-equ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
596
372
b4855a3ebd34 add more lemma in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 371
diff changeset
597
430
46c057cb3d82 limit-to done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 429
diff changeset
598