Mercurial > hg > Members > kono > Proof > category

annotate limit-to.agda @ 422:3a4a99a8edbe

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