Mercurial > hg > Members > kono > Proof > category

annotate discrete.agda @ 451:3ee32e4df4c7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add negation example
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 28 Feb 2017 12:38:23 +0900
parents e9ece23ab94e
children 3c2ce4474d92
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
448
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Category -- https://github.com/konn/category-agda
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Level
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 module discrete where
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import cat-utility
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import HomReasoning
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 open import Relation.Binary.Core
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import Relation.Nullary
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import Data.Empty
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open import Data.Maybe
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 open Functor
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 data TwoObject {c₁ : Level} : Set c₁ where
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 t0 : TwoObject
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 t1 : TwoObject
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 -- If we have limit then we have equalizer
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 --- two objects category
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 ---
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 --- f
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 --- -----→
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 --- 0 1
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 --- -----→
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 --- g
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 data Arrow {c₁ c₂ : Level } : TwoObject {c₁} → TwoObject {c₁} → Set c₂ where
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 id-t0 : Arrow t0 t0
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 id-t1 : Arrow t1 t1
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 arrow-f : Arrow t0 t1
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 arrow-g : Arrow t0 t1
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 record TwoHom {c₁ c₂ : Level} (a b : TwoObject {c₁} ) : Set ( c₂) where
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 field
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 hom : Maybe ( Arrow {c₁} {c₂} a b )
451
3ee32e4df4c7 add negation example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 450
diff changeset
37 constraint1 : {c₁ c₂ : Level } → TwoObject {c₁} → TwoObject {c₁} → Maybe ( ⊥ )
448
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 constraint1 t0 t0 = nothing
451
3ee32e4df4c7 add negation example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 450
diff changeset
39 constraint1 {c₁} {c₂} t1 t0 = just ( {!!} )
3ee32e4df4c7 add negation example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 450
diff changeset
40 constraint1 t0 t1 = nothing
448
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 constraint1 t1 t1 = nothing
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 comp : ∀ {c₁ c₂} → {a b c : TwoObject {c₁}} → Maybe ( Arrow {c₁} {c₂} b c ) → Maybe ( Arrow {c₁} {c₂} a b ) → Maybe ( Arrow {c₁} {c₂} a c )
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 comp {_} {_} {_} {_} {_} nothing _ = nothing
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 comp {_} {_} {_} {_} {_} (just _ ) nothing = nothing
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 comp {_} {_} {t0} {t1} {t1} (just id-t1 ) ( just arrow-f ) = just arrow-f
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 comp {_} {_} {t0} {t1} {t1} (just id-t1 ) ( just arrow-g ) = just arrow-g
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 comp {_} {_} {t1} {t1} {t1} (just id-t1 ) ( just id-t1 ) = just id-t1
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 comp {_} {_} {t0} {t0} {t1} (just arrow-f ) ( just id-t0 ) = just arrow-f
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 comp {_} {_} {t0} {t0} {t1} (just arrow-g ) ( just id-t0 ) = just arrow-g
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 comp {_} {_} {t0} {t0} {t0} (just id-t0 ) ( just id-t0 ) = just id-t0
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 comp {_} {_} {_} {_} {_} (just _ ) ( just _ ) = nothing
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 open TwoHom
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 _×_ : ∀ {c₁ c₂} → {a b c : TwoObject {c₁}} → ( TwoHom {c₁} {c₂} b c ) → ( TwoHom {c₁} {c₂} a b ) → ( TwoHom {c₁} {c₂} a c )
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 _×_ {c₁} {c₂} {a} {b} {c} f g = record { hom = comp {c₁} {c₂} {a} {b} {c} (hom f) (hom g ) }
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 _==_ : ∀{ c₁ c₂ a b } → Rel (Maybe (Arrow {c₁} {c₂} a b )) (c₂)
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 _==_ = Eq _≡_
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 ==refl : ∀{ c₁ c₂ a b } → ∀ {x : Maybe (Arrow {c₁} {c₂} a b )} → x == x
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 ==refl {_} {_} {_} {_} {just x} = just refl
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 ==refl {_} {_} {_} {_} {nothing} = nothing
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 ==sym : ∀{ c₁ c₂ a b } → ∀ {x y : Maybe (Arrow {c₁} {c₂} a b )} → x == y → y == x
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 ==sym (just x≈y) = just (≡-sym x≈y)
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 ==sym nothing = nothing
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 ==trans : ∀{ c₁ c₂ a b } → ∀ {x y z : Maybe (Arrow {c₁} {c₂} a b ) } →
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 x == y → y == z → x == z
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 ==trans (just x≈y) (just y≈z) = just (≡-trans x≈y y≈z)
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 ==trans nothing nothing = nothing
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 ==cong : ∀{ c₁ c₂ a b c d } → ∀ {x y : Maybe (Arrow {c₁} {c₂} a b )} →
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76 (f : Maybe (Arrow {c₁} {c₂} a b ) → Maybe (Arrow {c₁} {c₂} c d ) ) → x == y → f x == f y
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 ==cong { c₁} {c₂} {a} {b } {c} {d} {nothing} {nothing} f nothing = ==refl
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 ==cong { c₁} {c₂} {a} {b } {c} {d} {just x} {just .x} f (just refl) = ==refl
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 module ==-Reasoning {c₁ c₂ : Level} where
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 infixr 2 _∎
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84 infixr 2 _==⟨_⟩_ _==⟨⟩_
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85 infix 1 begin_
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 data _IsRelatedTo_ {c₁ c₂ : Level} {a b : TwoObject {c₁} } (x y : (Maybe (Arrow {c₁} {c₂} a b ))) :
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89 Set c₂ where
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 relTo : (x≈y : x == y ) → x IsRelatedTo y
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92 begin_ : { a b : TwoObject {c₁} } {x : Maybe (Arrow {c₁} {c₂} a b ) } {y : Maybe (Arrow {c₁} {c₂} a b )} →
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 x IsRelatedTo y → x == y
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94 begin relTo x≈y = x≈y
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 _==⟨_⟩_ : { a b : TwoObject {c₁} } (x : Maybe (Arrow {c₁} {c₂} a b )) {y z : Maybe (Arrow {c₁} {c₂} a b ) } →
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97 x == y → y IsRelatedTo z → x IsRelatedTo z
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98 _ ==⟨ x≈y ⟩ relTo y≈z = relTo (==trans x≈y y≈z)
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101 _==⟨⟩_ : { a b : TwoObject {c₁} }(x : Maybe (Arrow {c₁} {c₂} a b )) {y : Maybe (Arrow {c₁} {c₂} a b )}
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102 → x IsRelatedTo y → x IsRelatedTo y
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103 _ ==⟨⟩ x≈y = x≈y
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105 _∎ : { a b : TwoObject {c₁} }(x : Maybe (Arrow {c₁} {c₂} a b )) → x IsRelatedTo x
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 _∎ _ = relTo ==refl
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
108
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
109 -- TwoHom1Eq : {c₁ c₂ : Level } {a b : TwoObject {c₁} } {f g : ( TwoHom1 {c₁} {c₂ } a b)} →
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
110 -- hom (Map f) == hom (Map g) → f == g
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111 -- TwoHom1Eq = ?
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
112
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
113
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
114 -- f g h
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
115 -- d <- c <- b <- a
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
116 --
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
117 -- It can be proved without Arrow constraints
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
118
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
119 assoc-× : {c₁ c₂ : Level } {a b c d : TwoObject {c₁} }
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
120 {f : (TwoHom {c₁} {c₂ } c d )} →
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
121 {g : (TwoHom {c₁} {c₂ } b c )} →
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
122 {h : (TwoHom {c₁} {c₂ } a b )} →
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
123 hom ( f × (g × h)) == hom ((f × g) × h )
449
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
124 assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h} with hom f | hom g | hom h
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
125 assoc-× {c₁} {c₂} {_} {_} {_} {_} {f} {g} {h} | nothing | _ | _ = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
126 assoc-× {c₁} {c₂} {_} {_} {_} {_} {f} {g} {h} | just _ | nothing | _ = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
127 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} {f} {g} {h} | just id-t0 | just id-t0 | just id-t0 = ==refl
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
128 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just arrow-f | just id-t0 | just id-t0 = ==refl
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
129 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just arrow-g | just id-t0 | just id-t0 = ==refl
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
130 assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-f | just id-t0 = ==refl
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
131 assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-g | just id-t0 = ==refl
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
132 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | just id-t1 | just id-t1 | just arrow-f = ==refl
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
133 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | just id-t1 | just id-t1 | just arrow-g = ==refl
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
134 assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} {f} {g} {h} | just id-t1 | just id-t1 | just id-t1 = ==refl
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
135 -- remaining all failure case
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
136 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} {f} {g} {h} | just id-t0 | just id-t0 | nothing = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
137 assoc-× {c₁} {c₂} {t1} {t0} {t0} {t0} {f} {g} {h} | just id-t0 | just id-t0 | nothing = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
138 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | just id-t1 | just id-t1 | nothing = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
139 assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} {f} {g} {h} | just id-t1 | just id-t1 | nothing = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
140 assoc-× {c₁} {c₂} {t1} {t0} {t0} {t1} {f} {g} {h} | just arrow-f | just id-t0 | nothing = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
141 assoc-× {c₁} {c₂} {t1} {t0} {t0} {t1} {f} {g} {h} | just arrow-g | just id-t0 | nothing = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
142 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just arrow-f | just id-t0 | nothing = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
143 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just arrow-g | just id-t0 | nothing = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
144 assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-f | nothing = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
145 assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-g | nothing = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
146 assoc-× {c₁} {c₂} {t1} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-f | nothing = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
147 assoc-× {c₁} {c₂} {t1} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-g | nothing = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
148 assoc-× {_} {_} {t0} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just _) | nothing = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
149 assoc-× {_} {_} {t0} {t1} {t0} {t1} {_} {_} {_} | (just _) | (just _) | nothing = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
150 assoc-× {_} {_} {t1} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just _) | nothing = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
151 assoc-× {_} {_} {t1} {t1} {t0} {t1} {_} {_} {_} | (just _) | (just _) | nothing = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
152 assoc-× {_} {_} {t0} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just arrow-f) | (just id-t0) = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
153 assoc-× {_} {_} {t0} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just arrow-g) | (just id-t0) = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
154 assoc-× {_} {_} {t0} {t1} {t0} {t1} {_} {_} {_} | (just _) | (just _) | (just _) = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
155 assoc-× {_} {_} {t1} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just _) | (just _) = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
156 assoc-× {_} {_} {t1} {t0} {t1} {t1} {_} {_} {_} | (just id-t1) | (just arrow-f) | (just _) = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
157 assoc-× {_} {_} {t1} {t0} {t1} {t1} {_} {_} {_} | (just id-t1) | (just arrow-g) | (just _) = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
158 assoc-× {_} {_} {t0} {t1} {t0} {t0} {_} {_} {_} | (just _) | (just _) | (just _) = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
159 assoc-× {_} {_} {t0} {t1} {t0} {t0} {_} {_} {_} | (just _) | (just _) | nothing = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
160 assoc-× {_} {_} {t1} {t0} {t0} {t0} {_} {_} {_} | (just id-t0) | (just id-t0) | (just _) = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
161 assoc-× {_} {_} {t1} {t0} {t0} {t1} {_} {_} {_} | (just arrow-f) | (just id-t0) | (just _) = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
162 assoc-× {_} {_} {t1} {t0} {t0} {t1} {_} {_} {_} | (just arrow-g) | (just id-t0) | (just _) = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
163 assoc-× {_} {_} {t1} {t1} {t0} {_} {_} {_} {_} | (just _) | (just _) | (just _) = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
164 assoc-× {_} {_} {t1} {t1} {t0} {t0} {_} {_} {_} | (just _) | (just _) | nothing = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
165
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
166 TwoId : {c₁ c₂ : Level } (a : TwoObject {c₁} ) → (TwoHom {c₁} {c₂ } a a )
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
167 TwoId {_} {_} t0 = record { hom = just id-t0 }
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
168 TwoId {_} {_} t1 = record { hom = just id-t1 }
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
169
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
170 open import Relation.Binary
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
171 TwoCat : {c₁ c₂ ℓ : Level } → Category c₁ c₂ c₂
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
172 TwoCat {c₁} {c₂} {ℓ} = record {
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
173 Obj = TwoObject {c₁} ;
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
174 Hom = λ a b → ( TwoHom {c₁} {c₂ } a b ) ;
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
175 _o_ = λ{a} {b} {c} x y → _×_ {c₁ } { c₂} {a} {b} {c} x y ;
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
176 _≈_ = λ x y → hom x == hom y ;
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
177 Id = λ{a} → TwoId {c₁ } { c₂} a ;
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
178 isCategory = record {
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
179 isEquivalence = record {refl = ==refl ; trans = ==trans ; sym = ==sym } ;
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
180 identityL = λ{a b f} → identityL {c₁} {c₂ } {a} {b} {f} ;
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
181 identityR = λ{a b f} → identityR {c₁} {c₂ } {a} {b} {f} ;
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
182 o-resp-≈ = λ{a b c f g h i} → o-resp-≈ {c₁} {c₂ } {a} {b} {c} {f} {g} {h} {i} ;
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
183 associative = λ{a b c d f g h } → assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h}
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
184 }
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
185 } where
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
186 identityL : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → hom ((TwoId B) × f) == hom f
450
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 449
diff changeset
187 identityL {c₁} {c₂} {a} {b} {f} with hom f | constraint1 f a b
451
3ee32e4df4c7 add negation example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 450
diff changeset
188 identityL {c₁} {c₂} {t1} {t0} {f} | _ | just C = ⊥-elim C
3ee32e4df4c7 add negation example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 450
diff changeset
189 identityL {c₁} {c₂} {t1} {t0} {_} | just _ | nothing = {!!}
450
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 449
diff changeset
190 identityL {c₁} {c₂} {t0} {t0} {_} | nothing | _ = nothing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 449
diff changeset
191 identityL {c₁} {c₂} {t0} {t1} {_} | nothing | _ = nothing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 449
diff changeset
192 identityL {c₁} {c₂} {t1} {t0} {_} | nothing | _ = nothing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 449
diff changeset
193 identityL {c₁} {c₂} {t1} {t1} {_} | nothing | _ = nothing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 449
diff changeset
194 identityL {c₁} {c₂} {t1} {t1} {_} | just id-t1 | _ = ==refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 449
diff changeset
195 identityL {c₁} {c₂} {t0} {t0} {_} | just id-t0 | _ = ==refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 449
diff changeset
196 identityL {c₁} {c₂} {t0} {t1} {_} | just arrow-f | _ = ==refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 449
diff changeset
197 identityL {c₁} {c₂} {t0} {t1} {_} | just arrow-g | _ = ==refl
449
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
198 identityR : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → hom ( f × TwoId A ) == hom f
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
199 identityR {c₁} {c₂} {_} {_} {f} with hom f
450
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 449
diff changeset
200 identityR {c₁} {c₂} {t0} {t0} {_} | nothing = nothing
449
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
201 identityR {c₁} {c₂} {t0} {t1} {_} | nothing = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
202 identityR {c₁} {c₂} {t1} {t0} {_} | nothing = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
203 identityR {c₁} {c₂} {t1} {t1} {_} | nothing = nothing
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
204 identityR {c₁} {c₂} {t1} {t1} {_} | just id-t1 = ==refl
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
205 identityR {c₁} {c₂} {t0} {t0} {_} | just id-t0 = ==refl
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
206 identityR {c₁} {c₂} {t0} {t1} {_} | just arrow-f = ==refl
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
207 identityR {c₁} {c₂} {t0} {t1} {_} | just arrow-g = ==refl
450
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 449
diff changeset
208 identityR {c₁} {c₂} {t1} {t0} {_} | just _ = {!!}
449
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
209 o-resp-≈ : {c₁ c₂ : Level } {A B C : TwoObject {c₁} } {f g : ( TwoHom {c₁} {c₂ } A B)} {h i : ( TwoHom B C)} →
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
210 hom f == hom g → hom h == hom i → hom ( h × f ) == hom ( i × g )
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
211 o-resp-≈ {c₁} {c₂} {a} {b} {c} {f} {g} {h} {i} f==g h==i =
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
212 let open ==-Reasoning {c₁} {c₂ } in begin
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
213 hom ( h × f )
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
214 ==⟨⟩
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
215 comp (hom h) (hom f)
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
216 ==⟨ ==cong (λ x → comp ( hom h ) x ) f==g ⟩
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
217 comp (hom h) (hom g)
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
218 ==⟨ ==cong (λ x → comp x ( hom g ) ) h==i ⟩
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
219 comp (hom i) (hom g)
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
220 ==⟨⟩
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
221 hom ( i × g )
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
222 ∎
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
223
156e64d1bce0 on goinhg ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 448
diff changeset
224
448
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
225
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
226
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
227 record Nil {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
228 field
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
229 nil : {a b : Obj A } → Hom A a b
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
230 nil-id : {a : Obj A } → A [ nil {a} {a} ≈ id1 A a ] -- too strong but we need this
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
231 nil-idL : {a b c : Obj A } → { f : Hom A a b } → A [ A [ nil {b} {c} o f ] ≈ nil {a} {c} ]
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
232 nil-idR : {a b c : Obj A } → { f : Hom A b c } → A [ A [ f o nil {a} {b} ] ≈ nil {a} {c} ]
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
233
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
234 open Nil
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
235
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
236 indexFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (none : Nil A) ( a b : Obj A) ( f g : Hom A a b ) →
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
237 (obj : Obj A -> TwoObject {c₁}) (hom→ : {a b : Obj A} -> Hom A a b -> TwoObject {c₁}) → Functor A A
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
238 indexFunctor {c₁} {c₂} {ℓ} A none a b f g obj→ hom→ = record {
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
239 FObj = λ a → fobj a
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
240 ; FMap = λ {a} {b} f → fmap {a} {b} f
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
241 ; isFunctor = record {
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
242 identity = λ{x} → identity {x}
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
243 ; distr = λ {a} {b} {c} {f} {g} → distr1 {a} {b} {c} {f} {g}
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
244 ; ≈-cong = λ {a} {b} {c} {f} → ≈-cong {a} {b} {c} {f}
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
245 }
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
246 } where
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
247 fobj : Obj A → Obj A
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
248 fobj x with obj→ x
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
249 fobj x | t0 = a
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
250 fobj x | t1 = b
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
251 fmap : {x y : Obj A } → (Hom A x y ) → Hom A (fobj x) (fobj y)
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
252 fmap {x} {y} h with obj→ x | obj→ y | hom→ h
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
253 fmap h | t0 | t0 | _ = id1 A a
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
254 fmap h | t1 | t1 | _ = id1 A b
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
255 fmap h | t0 | t1 | t0 = f
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
256 fmap h | t0 | t1 | t1 = g
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
257 fmap h | _ | _ | _ = nil none
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
258 open ≈-Reasoning A
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
259 ≈-cong : {a : Obj A} {b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → A [ fmap f ≈ fmap g ]
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
260 ≈-cong = {!!}
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
261 identity : {x : Obj A} → A [ fmap ( id1 A x ) ≈ id1 A (fobj x) ]
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
262 identity {x} with obj→ x
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
263 identity | t0 = refl-hom
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
264 identity | t1 = refl-hom
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
265 distr1 : {a₁ : Obj A} {b₁ : Obj A} {c : Obj A} {f₁ : Hom A a₁ b₁} {g₁ : Hom A b₁ c} →
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
266 A [ fmap (A [ g₁ o f₁ ]) ≈ A [ fmap g₁ o fmap f₁ ] ]
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
267 distr1 {a1} {b1} {c1} {f1} {g1} with obj→ a1 | obj→ b1 | obj→ c1 | hom→ f1 | hom→ g1
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
268 distr1 {a1} {b1} {c1} {f1} {g1} | t0 | t0 | t0 | _ | _ = begin
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
269 id1 A a
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
270 ≈↑⟨ idL ⟩
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
271 id1 A a o id1 A a
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
272 ∎
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
273 distr1 {a1} {b1} {c1} {f1} {g1} | t1 | t1 | t1 | _ | _ = begin
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
274 id1 A b
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
275 ≈↑⟨ idL ⟩
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
276 id1 A b o id1 A b
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
277 ∎
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
278 distr1 {a1} {b1} {c1} {f1} {g1} | t1 | t0 | t0 | _ | _ = begin
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
279 nil none
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
280 ≈↑⟨ nil-idR none ⟩
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
281 id1 A a o nil none
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
282 ∎
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
283 distr1 {a1} {b1} {c1} {f1} {g1} | t1 | t1 | t0 | _ | _ = begin
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
284 nil none
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
285 ≈↑⟨ nil-idL none ⟩
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
286 nil none o id1 A b
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
287 ∎
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
288 distr1 {a1} {b1} {c1} {f1} {g1} | t0 | t1 | t0 | _ | _ = begin
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
289 id1 A a
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
290 ≈↑⟨ nil-id none ⟩
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
291 nil none
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
292 ≈↑⟨ nil-idL none ⟩
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
293 nil none o _
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
294 ∎
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
295 distr1 {a1} {b1} {c1} {f1} {g1} | t1 | t0 | t1 | _ | _ = begin
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
296 id1 A b
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
297 ≈↑⟨ nil-id none ⟩
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
298 nil none
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
299 ≈↑⟨ nil-idR none ⟩
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
300 _ o nil none
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
301 ∎
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
302 distr1 {a1} {b1} {c1} {f1} {g1} | t0 | t0 | t1 | _ | _ = begin
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
303 {!!}
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
304 ≈⟨ {!!} ⟩
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
305 {!!} o id1 A a
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
306 ∎
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
307 distr1 {a1} {b1} {c1} {f1} {g1} | t0 | t1 | t1 | _ | _ = {!!}
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
308
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
309
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
310
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
311
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
312
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
313
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
314 --- Equalizer
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
315 --- f
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
316 --- e -----→
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
317 --- c -----→ a b
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
318 --- ^ / -----→
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
319 --- |k h g
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
320 --- | /
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
321 --- | / ^
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
322 --- | / |
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
323 --- |/ | Γ
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
324 --- d _ |
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
325 --- |\ |
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
326 --- \ K af
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
327 --- \ -----→
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
328 --- \ t0 t1
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
329 --- -----→
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
330 --- ag
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
331 ---
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
332 ---
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
333
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
334 open Complete
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
335 open Limit
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
336 open NTrans
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
337
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
338 equlimit : {c₁ c₂ ℓ : Level} (A I : Category c₁ c₂ ℓ) {a b : Obj A} -> (f g : Hom A a b) (comp : Complete A I) ->
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
339 Hom A ( limit-c comp ({!!} )) a
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
340 equlimit A I f g comp = {!!}
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
341
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
342 lim-to-equ : {c₁ c₂ ℓ : Level} (A I : Category c₁ c₂ ℓ)
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
343 (comp : Complete A I)
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
344 → {a b : Obj A} (f g : Hom A a b )
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
345 → IsEqualizer A (equlimit A I f g comp ) f g
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
346 lim-to-equ {c₁} {c₂} {ℓ} A I comp {a} {b} f g = record {
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
347 fe=ge = {!!}
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
348 ; k = λ {d} h fh=gh → k {d} h fh=gh
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
349 ; ek=h = λ {d} {h} {fh=gh} → ek=h d h fh=gh
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
350 ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k'
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
351 } where
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
352 open ≈-Reasoning A
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
353 Γ : Functor I A
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
354 Γ = {!!}
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
355 eqlim = isLimit comp Γ
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
356 c = {!!}
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
357 e = {!!}
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
358 k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
359 k {d} h fh=gh = {!!}
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
360 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 ]
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
361 ek=h d h fh=gh = begin
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
362 e o k h fh=gh
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
363 ≈⟨ {!!} ⟩
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
364 h
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
365 ∎
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
366 uniq-nat : {i : Obj I} → (d : Obj A ) (h : Hom A d a ) ( k' : Hom A d c ) → A [ A [ e o k' ] ≈ h ] → A [ A [ {!!} o k' ] ≈ {!!} ]
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
367 uniq-nat d h k' ek'=h = begin
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
368 {!!} o k'
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
369 ≈⟨⟩
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
370 e o k'
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
371 ≈⟨ ek'=h ⟩
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
372 h
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
373 ≈⟨⟩
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
374 {!!}
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
375 ∎
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
376 uniquness : (d : Obj A ) (h : Hom A d a ) → ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) →
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
377 ( k' : Hom A d c )
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
378 → A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ]
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
379 uniquness d h fh=gh k' ek'=h = begin
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
380 k h fh=gh
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
381 ≈⟨ {!!} ⟩
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
382 k'
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
383 ∎
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
384
c2616de4d208 discrete again with negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
385