Mercurial > hg > Members > kono > Proof > category

annotate limit-to.agda @ 419:8919c162b894

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
cong is a bit strange...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 24 Mar 2016 02:53:25 +0900
parents 7091104a8cb4
children 3e44951b9bdb
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
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 --- ------>
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 --- 0 1
366
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
21 --- ------>
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
417
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
30 data Arrow {c₁ c₂ : Level } ( t00 t11 : TwoObject {c₁} ) : TwoObject {c₁} -> TwoObject {c₁} -> Set c₂ where
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
31 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
32 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
33 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
34 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
35 inv-f : Arrow t00 t11 t11 t00
415
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
36
417
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
37 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
38 field
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
39 RawHom : 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
40
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
41 open TwoHom
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 hom : ∀{ c₁ c₂ } { a b : TwoObject {c₁} } ->
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
44 ∀ (f : TwoHom {c₁} {c₂ } a b ) → 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
45 hom {_} {_} {a} {b} f with RawHom f
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
46 hom {_} {_} {t0} {t0} _ | just id-t0 = just id-t0
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
47 hom {_} {_} {t1} {t1} _ | just id-t1 = just id-t1
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
48 hom {_} {_} {t0} {t1} _ | just arrow-f = just arrow-f
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
49 hom {_} {_} {t0} {t1} _ | just arrow-g = just arrow-g
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
50 hom {_} {_} {t1} {t0} _ | just inv-f = just inv-f
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
51 hom {_} {_} {_ } {_ } _ | _ = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
52
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
53
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
54 open TwoHom
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
55
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
56 -- arrow composition
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
57
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
58
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
59 _×_ : ∀ {c₁ c₂} -> {a b c : TwoObject {c₁}} → ( TwoHom {c₁} {c₂} b c ) → ( TwoHom {c₁} {c₂} a b ) → ( TwoHom {c₁} {c₂} a c )
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
60 _×_ {c₁} {c₂} {a} {b} {c} f g with hom f | hom g
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
61 _×_ {_} {_} {_} {_} {_} f g | nothing | _ = record { RawHom = nothing }
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
62 _×_ {_} {_} {_} {_} {_} f g | just _ | nothing = record { RawHom = nothing }
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
63 _×_ {_} {_} {t0} {t1} {t1} f g | just id-t1 | just arrow-f = record { RawHom = just arrow-f }
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
64 _×_ {_} {_} {t0} {t1} {t1} f g | just id-t1 | just arrow-g = record { RawHom = just arrow-g }
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
65 _×_ {_} {_} {t1} {t1} {t1} f g | just id-t1 | just id-t1 = record { RawHom = just id-t1 }
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
66 _×_ {_} {_} {t1} {t1} {t0} f g | just inv-f | just id-t1 = record { RawHom = just inv-f }
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
67 _×_ {_} {_} {t0} {t0} {t1} f g | just arrow-f | just id-t0 = record { RawHom = just arrow-f }
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
68 _×_ {_} {_} {t0} {t0} {t1} f g | just arrow-g | just id-t0 = record { RawHom = just arrow-g }
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
69 _×_ {_} {_} {t0} {t0} {t0} f g | just id-t0 | just id-t0 = record { RawHom = just id-t0 }
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
70 _×_ {_} {_} {t1} {t0} {t0} f g | just id-t0 | just inv-f = record { RawHom = just inv-f }
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
71 _×_ {_} {_} {_} {_} {_} f g | just _ | just _ = record { RawHom = nothing }
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
72
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
73
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
74 _==_ : ∀{ c₁ c₂ a b } -> Rel (Maybe (Arrow {c₁} {c₂} t0 t1 a b )) (c₂)
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
75 _==_ = Eq _≡_
414
28249d32b700 Maybe does not help conflict ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 413
diff changeset
76
417
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
77 map2hom : ∀{ c₁ c₂ } -> {a b : TwoObject {c₁}} → Maybe ( Arrow {c₁} {c₂} t0 t1 a b ) -> TwoHom {c₁} {c₂ } a b
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
78 map2hom {_} {_} {t1} {t1} (just id-t1) = record { RawHom = just id-t1 }
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
79 map2hom {_} {_} {t0} {t1} (just arrow-f) = record { RawHom = just arrow-f }
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
80 map2hom {_} {_} {t0} {t1} (just arrow-g) = record { RawHom = just arrow-g }
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
81 map2hom {_} {_} {t0} {t0} (just id-t0) = record { RawHom = just id-t0 }
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
82 map2hom {_} {_} {_} {_} _ = record { RawHom = nothing }
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
83
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
84 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
85 field
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
86 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
87 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
88
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
89 ==refl : ∀{ c₁ c₂ a b } -> ∀ {x : Maybe (Arrow {c₁} {c₂} t0 t1 a b )} → x == x
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
90 ==refl {_} {_} {_} {_} {just x} = just refl
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
91 ==refl {_} {_} {_} {_} {nothing} = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
92
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
93 ==sym : ∀{ c₁ c₂ a b } -> ∀ {x y : Maybe (Arrow {c₁} {c₂} t0 t1 a b )} → _==_ x y → _==_ y x
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
94 ==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
95 ==sym nothing = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
96
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
97 ==trans : ∀{ c₁ c₂ a b } -> ∀ {x 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
98 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
99 ==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
100 ==trans nothing nothing = nothing
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
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
103 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
104
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 infixr 2 _==⟨_⟩_ _==⟨⟩_
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
107 infix 1 begin_
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
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
110 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
111 Set c₂ where
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
112 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
113
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
114 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
115 x IsRelatedTo y → x == y
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
116 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
117
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
118 _==⟨_⟩_ : { 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
119 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
120 _ ==⟨ 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
121
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
406
2fbd92ddecb5 non recorded arrow does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 405
diff changeset
130
417
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
131 -- f g h
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
132 -- d <- c <- b <- a
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
133
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
134 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
135 {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
136 {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
137 {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
138 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
139 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
140 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
141 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
142 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
143 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
144 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
145 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
146 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
147 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
148 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
149 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
150 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
151 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
152 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
153 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
154 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
155 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
156 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
157 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
158 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
159 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
160 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
161 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
162 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
163 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
164 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
165 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
166 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
167 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
168 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
169 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
170 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
171 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
172 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
173 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
174 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
175 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
176 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
177 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
178 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
179 assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} {f} {g} {h} | just id-t1 | just id-t1 | just id-t1 = ==refl
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
180 -- remaining all failure case
418
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
181 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
182 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
183 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
184 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
185 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
186 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
187 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
188 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
189 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
190 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
191 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
192 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
193 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
194 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
195 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
196 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
197 assoc-× {_} {_} {t0} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just _) | nothing = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
198 assoc-× {_} {_} {t0} {t1} {t0} {t1} {_} {_} {_} | (just _) | (just _) | nothing = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
199 assoc-× {_} {_} {t1} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just _) | nothing = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
200 assoc-× {_} {_} {t1} {t1} {t0} {t1} {_} {_} {_} | (just _) | (just _) | nothing = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
201 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
202 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
203 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
204 assoc-× {_} {_} {t0} {t1} {t0} {t1} {_} {_} {_} | (just _) | (just _) | (just _) = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
205 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
206 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
207 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
208 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
209 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
210 assoc-× {_} {_} {t1} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just _) | (just _) = nothing
7091104a8cb4 assoc passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
211 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
212 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
213 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
214 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
215 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
216 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
217
404
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 403
diff changeset
218
409
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 408
diff changeset
219
417
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
220 TwoId : {c₁ c₂ : Level } (a : TwoObject {c₁} ) -> (TwoHom {c₁} {c₂ } a a )
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
221 TwoId {_} {_} t0 = record { RawHom = just id-t0 }
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
222 TwoId {_} {_} t1 = record { RawHom = just id-t1 }
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
223
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
224 open import maybeCat
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
225
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
226 -- 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
227 -- begin
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
228 -- (TwoId b × nothing)
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 -- nothing
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
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
233 open import Relation.Binary
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
234 TwoCat : {c₁ c₂ ℓ : Level } -> Category c₁ c₂ c₂
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
235 TwoCat {c₁} {c₂} {ℓ} = record {
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
236 Obj = TwoObject {c₁} ;
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
237 Hom = λ a b → ( TwoHom {c₁} {c₂ } a b ) ;
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
238 _o_ = \{a} {b} {c} x y -> _×_ {c₁ } { c₂} {a} {b} {c} x y ;
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
239 _≈_ = \x y -> hom x == hom y ;
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
240 Id = \{a} -> TwoId {c₁ } { c₂} a ;
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
241 isCategory = record {
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
242 isEquivalence = record {refl = ==refl ; trans = ==trans ; sym = ==sym } ;
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
243 identityL = \{a b f} -> identityL {c₁} {c₂ } {a} {b} {f} ;
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
244 identityR = \{a b f} -> identityR {c₁} {c₂ } {a} {b} {f} ;
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
245 o-resp-≈ = \{a b c f g h i} -> o-resp-≈ {c₁} {c₂ } {a} {b} {c} {f} {g} {h} {i} ;
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
246 associative = \{a b c d f g h } -> assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h}
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
247 }
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
248 } where
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
249 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
250 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
251 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
252 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
253 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
254 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
255 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
256 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
257 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
258 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
259 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
260 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
261 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
262 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
263 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
264 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
265 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
266 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
267 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
268 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
269 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
270 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
271 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
272 hom f == hom g → hom h == hom i → hom ( h × f ) == hom ( i × g )
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
273 o-resp-≈ {_} {_} {a} {b} {c} {f} {g} {h} {i} f≡g h≡i = {!!}
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
274
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
275
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
276 indexFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj (MaybeCat A )) ( f g : Hom A a b ) -> Functor (TwoCat {c₁} {c₂} {c₂} ) (MaybeCat A )
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
277 indexFunctor {c₁} {c₂} {ℓ} A a b f g = record {
385
ff3803fc0c8a add level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 384
diff changeset
278 FObj = λ a → fobj a
405
4c34c0e3c4bb no Maybe TwoCat in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 404
diff changeset
279 ; FMap = λ {a} {b} f → fmap {a} {b} f
366
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
280 ; isFunctor = record {
374
5641b923201e limit-to: indexFunctor distribution law cannot be proved
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 373
diff changeset
281 identity = \{x} -> identity {x}
415
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
282 ; distr = \ {a} {b} {c} {f} {g} -> distr1 {a} {b} {c} {f} {g}
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
283 ; ≈-cong = \ {a} {b} {c} {f} -> ≈-cong {a} {b} {c} {f}
366
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
284 }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
285 } where
417
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
286 I = TwoCat {c₁} {c₂} {ℓ}
402
9123f79c0642 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 401
diff changeset
287 MA = MaybeCat A
404
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 403
diff changeset
288 open ≈-Reasoning (MA)
417
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
289 fobj : Obj I -> Obj A
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
290 fobj t0 = a
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
291 fobj t1 = b
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
292 fmap : {x y : Obj I } -> (TwoHom {c₁} {c₂} x y ) -> Hom MA (fobj x) (fobj y)
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
293 fmap {x} {y} h with hom h
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
294 fmap {t0} {t0} h | just id-t0 = id1 MA a
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
295 fmap {t1} {t1} h | just id-t1 = id1 MA b
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
296 fmap {t0} {t1} h | just arrow-f = record { hom = just f }
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
297 fmap {t0} {t1} h | just arrow-g = record { hom = just g }
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
298 fmap {_} {_} h | _ = record { hom = nothing }
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
299 identity : {x : Obj I} → MA [ fmap ( id1 I x ) ≈ id1 MA (fobj x) ]
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
300 identity {t0} = refl-hom
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
301 identity {t1} = refl-hom
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
302 distr1 : {a₁ : Obj I} {b₁ : Obj I} {c : Obj I} {f₁ : Hom I a₁ b₁} {g₁ : Hom I b₁ c} →
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
303 MA [ fmap (I [ g₁ o f₁ ]) ≈ MA [ fmap g₁ o fmap f₁ ] ]
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
304 distr1 {a1} {b1} {c1} {f1} {g1} with hom g1 | hom f1
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
305 distr1 {t0} {t0} {t0} {f1} {g1} | nothing | nothing = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
306 distr1 {t0} {t0} {t1} {f1} {g1} | nothing | nothing = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
307 distr1 {t0} {t1} {t0} {f1} {g1} | nothing | nothing = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
308 distr1 {t0} {t1} {t1} {f1} {g1} | nothing | nothing = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
309 distr1 {t1} {t0} {t0} {f1} {g1} | nothing | nothing = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
310 distr1 {t1} {t0} {t1} {f1} {g1} | nothing | nothing = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
311 distr1 {t1} {t1} {t0} {f1} {g1} | nothing | nothing = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
312 distr1 {t1} {t1} {t1} {f1} {g1} | nothing | nothing = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
313 distr1 {t0} {t0} {t0} {f1} {g1} | nothing | just id-t0 = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
314 distr1 {t0} {t0} {t1} {f1} {g1} | nothing | just id-t0 = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
315 distr1 {t1} {t1} {t0} {f1} {g1} | nothing | just id-t1 = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
316 distr1 {t1} {t1} {t1} {f1} {g1} | nothing | just id-t1 = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
317 distr1 {t0} {t1} {t1} {f1} {g1} | nothing | just arrow-f = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
318 distr1 {t0} {t1} {t0} {f1} {g1} | nothing | just arrow-f = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
319 distr1 {t0} {t1} {t1} {f1} {g1} | nothing | just arrow-g = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
320 distr1 {t0} {t1} {t0} {f1} {g1} | nothing | just arrow-g = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
321 distr1 {t1} {t0} {t0} {f1} {g1} | nothing | just inv-f = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
322 distr1 {t1} {t0} {t1} {f1} {g1} | nothing | just inv-f = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
323 distr1 {t0} {t0} {t0} {f1} {g1} | just id-t0 | nothing = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
324 distr1 {t1} {t0} {t0} {f1} {g1} | just id-t0 | nothing = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
325 distr1 {t0} {t1} {t1} {f1} {g1} | just id-t1 | nothing = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
326 distr1 {t1} {t1} {t1} {f1} {g1} | just id-t1 | nothing = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
327 distr1 {t0} {t0} {t1} {f1} {g1} | just arrow-f | nothing = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
328 distr1 {t1} {t0} {t1} {f1} {g1} | just arrow-f | nothing = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
329 distr1 {t0} {t0} {t1} {f1} {g1} | just arrow-g | nothing = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
330 distr1 {t1} {t0} {t1} {f1} {g1} | just arrow-g | nothing = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
331 distr1 {t0} {t1} {t0} {f1} {g1} | just inv-f | nothing = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
332 distr1 {t1} {t1} {t0} {f1} {g1} | just inv-f | nothing = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
333 distr1 {t0} {t0} {t0} {f1} {g1} | just id-t0 | just id-t0 = sym idL
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
334 distr1 {t1} {t0} {t0} {f1} {g1} | just id-t0 | just inv-f = sym idL
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
335 distr1 {t0} {t0} {t1} {f1} {g1} | just arrow-f | just id-t0 = sym idR
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
336 distr1 {t0} {t0} {t1} {f1} {g1} | just arrow-g | just id-t0 = sym idR
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
337 distr1 {t1} {t1} {t1} {f1} {g1} | just id-t1 | just id-t1 = sym idL
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
338 distr1 {t0} {t1} {t1} {f1} {g1} | just id-t1 | just arrow-f = sym idL
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
339 distr1 {t0} {t1} {t1} {f1} {g1} | just id-t1 | just arrow-g = sym idL
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
340 distr1 {t1} {t1} {t0} {f1} {g1} | just inv-f | just id-t1 = sym idL
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
341 distr1 {t0} {t1} {t0} {_} {_} | (just inv-f) | (just _) = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
342 distr1 {t1} {t0} {t1} {_} {_} | (just arrow-f) | (just _) = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
343 distr1 {t1} {t0} {t1} {_} {_} | (just arrow-g) | (just _) = nothing
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
344
419
8919c162b894 cong is a bit strange...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 418
diff changeset
345 ≈-cong : {a : Obj I} {b : Obj I} {f g : Hom I a b} → I [ f ≈ g ] → MA [ fmap f ≈ fmap g ]
8919c162b894 cong is a bit strange...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 418
diff changeset
346 ≈-cong {_} {_} {f1} {g1} f≈g with hom f1 | hom g1
8919c162b894 cong is a bit strange...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 418
diff changeset
347 ≈-cong {t0} {t0} {f1} {g1} f≈g | nothing | nothing = nothing
8919c162b894 cong is a bit strange...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 418
diff changeset
348 ≈-cong {t0} {t1} {f1} {g1} f≈g | nothing | nothing = nothing
8919c162b894 cong is a bit strange...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 418
diff changeset
349 ≈-cong {t1} {t0} {f1} {g1} f≈g | nothing | nothing = nothing
8919c162b894 cong is a bit strange...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 418
diff changeset
350 ≈-cong {t1} {t1} {f1} {g1} f≈g | nothing | nothing = nothing
8919c162b894 cong is a bit strange...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 418
diff changeset
351 ≈-cong {t0} {t0} {f1} {g1} f≈g | nothing | just id-t0 = {!!}
8919c162b894 cong is a bit strange...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 418
diff changeset
352 ≈-cong {t0} {t1} {f1} {g1} f≈g | nothing | just arrow-f = {!!}
8919c162b894 cong is a bit strange...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 418
diff changeset
353 ≈-cong {t0} {t1} {f1} {g1} f≈g | nothing | just arrow-g = {!!}
8919c162b894 cong is a bit strange...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 418
diff changeset
354 ≈-cong {t1} {t0} {f1} {g1} f≈g | nothing | just inv-f = nothing
8919c162b894 cong is a bit strange...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 418
diff changeset
355 ≈-cong {t1} {t1} {f1} {g1} f≈g | nothing | just id-t1 = {!!}
8919c162b894 cong is a bit strange...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 418
diff changeset
356 ≈-cong {t0} {t0} {f1} {g1} f≈g | just id-t0 | nothing = {!!}
8919c162b894 cong is a bit strange...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 418
diff changeset
357 ≈-cong {t1} {t1} {f1} {g1} f≈g | just id-t1 | nothing = {!!}
8919c162b894 cong is a bit strange...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 418
diff changeset
358 ≈-cong {t0} {t1} {f1} {g1} f≈g | just arrow-f | nothing = {!!}
8919c162b894 cong is a bit strange...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 418
diff changeset
359 ≈-cong {t0} {t1} {f1} {g1} f≈g | just arrow-g | nothing = {!!}
8919c162b894 cong is a bit strange...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 418
diff changeset
360 ≈-cong {t1} {t0} {f1} {g1} f≈g | just inv-f | nothing = nothing
8919c162b894 cong is a bit strange...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 418
diff changeset
361 ≈-cong {t0} {t0} {f1} {g1} f≈g | just id-t0 | just id-t0 = refl-hom
8919c162b894 cong is a bit strange...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 418
diff changeset
362 ≈-cong {t1} {t1} {f1} {g1} f≈g | just id-t1 | just id-t1 = refl-hom
8919c162b894 cong is a bit strange...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 418
diff changeset
363 ≈-cong {t0} {t1} {f1} {g1} f≈g | just arrow-f | just arrow-f = refl-hom
8919c162b894 cong is a bit strange...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 418
diff changeset
364 ≈-cong {t0} {t1} {f1} {g1} f≈g | just arrow-g | just arrow-g = refl-hom
8919c162b894 cong is a bit strange...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 418
diff changeset
365 ≈-cong {t0} {t1} {f1} {g1} f≈g | just arrow-g | just arrow-f = {!!}
8919c162b894 cong is a bit strange...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 418
diff changeset
366 ≈-cong {t1} {t0} {f1} {g1} f≈g | just inv-f | just inv-f = refl-hom
8919c162b894 cong is a bit strange...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 418
diff changeset
367 ≈-cong {t0} {t1} {f1} {g1} f≈g | just arrow-f | just arrow-g = begin
8919c162b894 cong is a bit strange...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 418
diff changeset
368 {!!}
8919c162b894 cong is a bit strange...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 418
diff changeset
369 ≈⟨ {!!} ⟩
8919c162b894 cong is a bit strange...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 418
diff changeset
370 {!!}
8919c162b894 cong is a bit strange...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 418
diff changeset
371 ∎
388
a0ab2643eee7 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 387
diff changeset
372
365
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
373
387
2f59c2db9d98 what is this ?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
374 --- Equalizer
2f59c2db9d98 what is this ?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
375 --- f
2f59c2db9d98 what is this ?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
376 --- e ------>
2f59c2db9d98 what is this ?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
377 --- c ------> a b
2f59c2db9d98 what is this ?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
378 --- ^ / ------>
2f59c2db9d98 what is this ?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
379 --- |k h g
415
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
380 --- | /
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
381 --- | /
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
382 --- | /
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
383 --- |/
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
384 --- d
387
2f59c2db9d98 what is this ?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
385
350
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
386 open Limit
352
f589e71875ea bad approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 351
diff changeset
387
403
375edfefbf6a maybe CAT
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 402
diff changeset
388 lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ->
412
f04b2fb91432 recover TwoHom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 410
diff changeset
389 (lim : (I : Category c₁ c₂ ℓ) ( Γ : Functor I A ) → {a0 : Obj A } {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
390 → {a b c : Obj A} (f g : Hom A a b )
365
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
391 → (e : Hom A c a ) → (fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] ) → Equalizer A e f g
403
375edfefbf6a maybe CAT
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 402
diff changeset
392 lim-to-equ {c₁} {c₂} {ℓ } A 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
393 fe=ge = fe=ge
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
394 ; k = λ {d} h fh=gh → k {d} h fh=gh
373
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 372
diff changeset
395 ; 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
396 ; 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
397 } where
1e76e611d454 with inv-f, distribution law passed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 416
diff changeset
398 I = TwoCat {c₁} {c₂} {ℓ }
402
9123f79c0642 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 401
diff changeset
399 Γ = {!!}
375
5a6db4bc4d9b still trying ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 374
diff changeset
400 nmap : (x : Obj I) ( d : Obj A ) (h : Hom A d a ) -> Hom A (FObj (K A I d) x) (FObj Γ x)
385
ff3803fc0c8a add level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 384
diff changeset
401 nmap x d h = {!!}
415
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
402 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 ] ]
375
5a6db4bc4d9b still trying ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 374
diff changeset
403 → A [ A [ FMap Γ f' o nmap x d h ] ≈ A [ nmap y d h o FMap (K A I d) f' ] ]
385
ff3803fc0c8a add level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 384
diff changeset
404 commute1 {x} {y} {f'} d h fh=gh = {!!}
375
5a6db4bc4d9b still trying ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 374
diff changeset
405 nat : (d : Obj A) → (h : Hom A d a ) → A [ A [ f o h ] ≈ A [ g o h ] ] → NTrans I A (K A I d) Γ
368
b18585089d2e add more parameter to nat in lim-to-equ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
406 nat d h fh=gh = record {
415
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
407 TMap = λ x → nmap x d h ;
350
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
408 isNTrans = record {
415
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
409 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
410 }
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
411 }
c483374f542b try equalizer from limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
412 k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c
385
ff3803fc0c8a add level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 384
diff changeset
413 k {d} h fh=gh = {!!} -- limit (lim I Γ {c} {nat c e fe=ge }) d (nat d h fh=gh )
372
b4855a3ebd34 add more lemma in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 371
diff changeset
414 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 ]
374
5641b923201e limit-to: indexFunctor distribution law cannot be proved
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 373
diff changeset
415 ek=h d h fh=gh = {!!}
372
b4855a3ebd34 add more lemma in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 371
diff changeset
416 uniquness : (d : Obj A ) (h : Hom A d a ) -> ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) ->
b4855a3ebd34 add more lemma in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 371
diff changeset
417 ( k' : Hom A d c )
b4855a3ebd34 add more lemma in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 371
diff changeset
418 -> A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ]
415
dd086f5fb29f same conflict again ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 414
diff changeset
419 uniquness d h fh=gh = {!!}
368
b18585089d2e add more parameter to nat in lim-to-equ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
420
372
b4855a3ebd34 add more lemma in limit-to
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 371
diff changeset
421