Mercurial > hg > Members > kono > Proof > category

comparison src/CCC.agda @ 967:472bcadfd216

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 25 Feb 2021 13:08:17 +0900
parents 396bf884f5e7
children 5f76e5cf3d49
comparison
equal deleted inserted replaced
966:cb970ab7c32b 967:472bcadfd216
30 π-cong : {a b c : Obj A} → { f f' : Hom A c a }{ g g' : Hom A c b } → A [ f ≈ f' ] → A [ g ≈ g' ] → A [ < f , g > ≈ < f' , g' > ] 30 π-cong : {a b c : Obj A} → { f f' : Hom A c a }{ g g' : Hom A c b } → A [ f ≈ f' ] → A [ g ≈ g' ] → A [ < f , g > ≈ < f' , g' > ]
31 -- closed 31 -- closed
32 e4a : {a b c : Obj A} → { h : Hom A (c ∧ b) a } → A [ A [ ε o < A [ (h *) o π ] , π' > ] ≈ h ] 32 e4a : {a b c : Obj A} → { h : Hom A (c ∧ b) a } → A [ A [ ε o < A [ (h *) o π ] , π' > ] ≈ h ]
33 e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } → A [ ( A [ ε o < A [ k o π ] , π' > ] ) * ≈ k ] 33 e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } → A [ ( A [ ε o < A [ k o π ] , π' > ] ) * ≈ k ]
34 *-cong : {a b c : Obj A} → { f f' : Hom A (a ∧ b) c } → A [ f ≈ f' ] → A [ f * ≈ f' * ] 34 *-cong : {a b c : Obj A} → { f f' : Hom A (a ∧ b) c } → A [ f ≈ f' ] → A [ f * ≈ f' * ]
35 35 open ≈-Reasoning A
36 e'2 : A [ ○ １ ≈ id1 A １ ] 36 e'2 : ○ １ ≈ id1 A １
37 e'2 = let open ≈-Reasoning A in begin 37 e'2 = begin
38 ○ １ 38 ○ １
39 ≈↑⟨ e2 ⟩ 39 ≈↑⟨ e2 ⟩
40 id1 A １ 40 id1 A １
41 ∎ 41 ∎
42 e''2 : {a b : Obj A} {f : Hom A a b } → A [ A [ ○ b o f ] ≈ ○ a ] 42 e''2 : {a b : Obj A} {f : Hom A a b } → ( ○ b o f ) ≈ ○ a
43 e''2 {a} {b} {f} = let open ≈-Reasoning A in begin 43 e''2 {a} {b} {f} = begin
44 ○ b o f 44 ○ b o f
45 ≈⟨ e2 ⟩ 45 ≈⟨ e2 ⟩
46 ○ a 46 ○ a
47 ∎ 47 ∎
48 π-id : {a b : Obj A} → A [ < π , π' > ≈ id1 A (a ∧ b ) ] 48 π-id : {a b : Obj A} → < π , π' > ≈ id1 A (a ∧ b )
49 π-id {a} {b} = let open ≈-Reasoning A in begin 49 π-id {a} {b} = begin
50 < π , π' > 50 < π , π' >
51 ≈↑⟨ π-cong idR idR ⟩ 51 ≈↑⟨ π-cong idR idR ⟩
52 < π o id1 A (a ∧ b) , π' o id1 A (a ∧ b) > 52 < π o id1 A (a ∧ b) , π' o id1 A (a ∧ b) >
53 ≈⟨ e3c ⟩ 53 ≈⟨ e3c ⟩
54 id1 A (a ∧ b ) 54 id1 A (a ∧ b )
55 ∎ 55 ∎
56 distr-π : {a b c d : Obj A} {f : Hom A c a }{g : Hom A c b } {h : Hom A d c } → A [ A [ < f , g > o h ] ≈ < A [ f o h ] , A [ g o h ] > ] 56 distr-π : {a b c d : Obj A} {f : Hom A c a }{g : Hom A c b } {h : Hom A d c } → ( < f , g > o h ) ≈ < ( f o h ) , ( g o h ) >
57 distr-π {a} {b} {c} {d} {f} {g} {h} = let open ≈-Reasoning A in begin 57 distr-π {a} {b} {c} {d} {f} {g} {h} = begin
58 < f , g > o h 58 < f , g > o h
59 ≈↑⟨ e3c ⟩ 59 ≈↑⟨ e3c ⟩
60 < π o < f , g > o h , π' o < f , g > o h > 60 < π o < f , g > o h , π' o < f , g > o h >
61 ≈⟨ π-cong assoc assoc ⟩ 61 ≈⟨ π-cong assoc assoc ⟩
62 < ( π o < f , g > ) o h , (π' o < f , g > ) o h > 62 < ( π o < f , g > ) o h , (π' o < f , g > ) o h >
63 ≈⟨ π-cong (car e3a ) (car e3b) ⟩ 63 ≈⟨ π-cong (car e3a ) (car e3b) ⟩
64 < f o h , g o h > 64 < f o h , g o h >
65 ∎ 65 ∎
66 _×_ : { a b c d : Obj A } ( f : Hom A a c ) (g : Hom A b d ) → Hom A (a ∧ b) ( c ∧ d ) 66 _×_ : { a b c d : Obj A } ( f : Hom A a c ) (g : Hom A b d ) → Hom A (a ∧ b) ( c ∧ d )
67 f × g = < (A [ f o π ] ) , (A [ g o π' ]) > 67 f × g = < ( f o π ) , (g o π' ) >
68 distr-* : {a b c d : Obj A } { h : Hom A (a ∧ b) c } { k : Hom A d a } → A [ A [ h * o k ] ≈ ( A [ h o < A [ k o π ] , π' > ] ) * ] 68 π-exchg : {a b c : Obj A} {f : Hom A c a }{g : Hom A c b } → < π' , π > o < f , g > ≈ < g , f >
69 π-exchg {a} {b} {c} {f} {g} = begin
70 < π' , π > o < f , g >
71 ≈⟨ distr-π ⟩
72 < π' o < f , g > , π o < f , g > >
73 ≈⟨ π-cong e3b e3a ⟩
74 < g , f >
75 ∎
76 π'π : {a b : Obj A} → < π' , π > o < π' , π > ≈ id1 A (a ∧ b)
77 π'π = trans-hom π-exchg π-id
78 exchg-π : {a b c d : Obj A} {f : Hom A c a }{g : Hom A d b } → < f o π , g o π' > o < π' , π > ≈ < f o π' , g o π >
79 exchg-π {a} {b} {c} {d} {f} {g} = begin
80 < f o π , g o π' > o < π' , π >
81 ≈⟨ distr-π ⟩
82 < (f o π) o < π' , π > , (g o π' ) o < π' , π > >
83 ≈↑⟨ π-cong assoc assoc ⟩
84 < f o (π o < π' , π > ) , g o (π' o < π' , π >)>
85 ≈⟨ π-cong (cdr e3a) (cdr e3b) ⟩
86 < f o π' , g o π >
87 ∎
88 distr-* : {a b c d : Obj A } { h : Hom A (a ∧ b) c } { k : Hom A d a } → ( h * o k ) ≈ ( h o < ( k o π ) , π' > ) *
69 distr-* {a} {b} {c} {d} {h} {k} = begin 89 distr-* {a} {b} {c} {d} {h} {k} = begin
70 h * o k 90 h * o k
71 ≈↑⟨ e4b ⟩ 91 ≈↑⟨ e4b ⟩
72 ( ε o < (h * o k ) o π , π' > ) * 92 ( ε o < (h * o k ) o π , π' > ) *
73 ≈⟨ *-cong ( begin 93 ≈⟨ *-cong ( begin
84 ( ε o < h * o π , π' > ) o < k o π , π' > 104 ( ε o < h * o π , π' > ) o < k o π , π' >
85 ≈⟨ car e4a ⟩ 105 ≈⟨ car e4a ⟩
86 h o < k o π , π' > 106 h o < k o π , π' >
87 ∎ ) ⟩ 107 ∎ ) ⟩
88 ( h o < k o π , π' > ) * 108 ( h o < k o π , π' > ) *
89 ∎ where open ≈-Reasoning A 109 ∎
90 α : {a b c : Obj A } → Hom A (( a ∧ b ) ∧ c ) ( a ∧ ( b ∧ c ) ) 110 α : {a b c : Obj A } → Hom A (( a ∧ b ) ∧ c ) ( a ∧ ( b ∧ c ) )
91 α = < A [ π o π ] , < A [ π' o π ] , π' > > 111 α = < ( π o π ) , < ( π' o π ) , π' > >
92 α' : {a b c : Obj A } → Hom A ( a ∧ ( b ∧ c ) ) (( a ∧ b ) ∧ c ) 112 α' : {a b c : Obj A } → Hom A ( a ∧ ( b ∧ c ) ) (( a ∧ b ) ∧ c )
93 α' = < < π , A [ π o π' ] > , A [ π' o π' ] > 113 α' = < < π , ( π o π' ) > , ( π' o π' ) >
94 β : {a b c d : Obj A } { f : Hom A a b} { g : Hom A a c } { h : Hom A a d } → A [ A [ α o < < f , g > , h > ] ≈ < f , < g , h > > ] 114 β : {a b c d : Obj A } { f : Hom A a b} { g : Hom A a c } { h : Hom A a d } → ( α o < < f , g > , h > ) ≈ < f , < g , h > >
95 β {a} {b} {c} {d} {f} {g} {h} = begin 115 β {a} {b} {c} {d} {f} {g} {h} = begin
96 α o < < f , g > , h > 116 α o < < f , g > , h >
97 ≈⟨⟩ 117 ≈⟨⟩
98 ( < ( π o π ) , < ( π' o π ) , π' > > ) o < < f , g > , h > 118 ( < ( π o π ) , < ( π' o π ) , π' > > ) o < < f , g > , h >
99 ≈⟨ distr-π ⟩ 119 ≈⟨ distr-π ⟩
104 < ( π o (π o < < f , g > , h >) ) , ( < ( π' o ( π o < < f , g > , h > ) ) , ( π' o < < f , g > , h > ) > ) > 124 < ( π o (π o < < f , g > , h >) ) , ( < ( π' o ( π o < < f , g > , h > ) ) , ( π' o < < f , g > , h > ) > ) >
105 ≈⟨ π-cong (cdr e3a ) ( π-cong (cdr e3a ) e3b ) ⟩ 125 ≈⟨ π-cong (cdr e3a ) ( π-cong (cdr e3a ) e3b ) ⟩
106 < ( π o < f , g > ) , < ( π' o < f , g > ) , h > > 126 < ( π o < f , g > ) , < ( π' o < f , g > ) , h > >
107 ≈⟨ π-cong e3a ( π-cong e3b refl-hom ) ⟩ 127 ≈⟨ π-cong e3a ( π-cong e3b refl-hom ) ⟩
108 < f , < g , h > > 128 < f , < g , h > >
109 ∎ where open ≈-Reasoning A 129 ∎
110 130
111 131
112 record CCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where 132 record CCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
113 field 133 field
114 １ : Obj A 134 １ : Obj A