Mercurial > hg > Members > kono > Proof > category
comparison CCC.agda @ 794:ba575c73ea48
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 22 Apr 2019 12:43:49 +0900 (2019-04-22) |
parents | f37f11e1b871 |
children |
comparison
equal
deleted
inserted
replaced
793:f37f11e1b871 | 794:ba575c73ea48 |
---|---|
50 ≈↑⟨ π-cong idR idR ⟩ | 50 ≈↑⟨ π-cong idR idR ⟩ |
51 < π o id1 A (a ∧ b) , π' o id1 A (a ∧ b) > | 51 < π o id1 A (a ∧ b) , π' o id1 A (a ∧ b) > |
52 ≈⟨ e3c ⟩ | 52 ≈⟨ e3c ⟩ |
53 id1 A (a ∧ b ) | 53 id1 A (a ∧ b ) |
54 ∎ | 54 ∎ |
55 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 ] > ] | 55 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} {f} {g} {h} = let open ≈-Reasoning A in begin | 56 distr-π {a} {b} {c} {d} {f} {g} {h} = let open ≈-Reasoning A in begin |
57 < f , g > o h | 57 < f , g > o h |
58 ≈↑⟨ e3c ⟩ | 58 ≈↑⟨ e3c ⟩ |
59 < π o < f , g > o h , π' o < f , g > o h > | 59 < π o < f , g > o h , π' o < f , g > o h > |
60 ≈⟨ π-cong assoc assoc ⟩ | 60 ≈⟨ π-cong assoc assoc ⟩ |
61 < ( π o < f , g > ) o h , (π' o < f , g > ) o h > | 61 < ( π o < f , g > ) o h , (π' o < f , g > ) o h > |
62 ≈⟨ π-cong (car e3a ) (car e3b) ⟩ | 62 ≈⟨ π-cong (car e3a ) (car e3b) ⟩ |
63 < f o h , g o h > | 63 < f o h , g o h > |
64 ∎ | 64 ∎ |
65 _×_ : { a b c d e : Obj A } ( f : Hom A a d ) (g : Hom A b e ) ( h : Hom A c (a ∧ b) ) → Hom A c ( d ∧ e ) | 65 _×_ : { a b c d : Obj A } ( f : Hom A a c ) (g : Hom A b d ) → Hom A (a ∧ b) ( c ∧ d ) |
66 f × g = λ h → < A [ f o A [ π o h ] ] , A [ g o A [ π' o h ] ] > | 66 f × g = < (A [ f o π ] ) , (A [ g o π' ]) > |
67 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 distr-* {a} {b} {c} {d} {h} {k} = begin | |
69 h * o k | |
70 ≈↑⟨ e4b ⟩ | |
71 ( ε o < (h * o k ) o π , π' > ) * | |
72 ≈⟨ *-cong ( begin | |
73 ε o < (h * o k ) o π , π' > | |
74 ≈↑⟨ cdr ( π-cong assoc refl-hom ) ⟩ | |
75 ε o ( < h * o ( k o π ) , π' > ) | |
76 ≈↑⟨ cdr ( π-cong (cdr e3a) e3b ) ⟩ | |
77 ε o ( < h * o ( π o < k o π , π' > ) , π' o < k o π , π' > > ) | |
78 ≈⟨ cdr ( π-cong assoc refl-hom) ⟩ | |
79 ε o ( < (h * o π) o < k o π , π' > , π' o < k o π , π' > > ) | |
80 ≈↑⟨ cdr ( distr-π ) ⟩ | |
81 ε o ( < h * o π , π' > o < k o π , π' > ) | |
82 ≈⟨ assoc ⟩ | |
83 ( ε o < h * o π , π' > ) o < k o π , π' > | |
84 ≈⟨ car e4a ⟩ | |
85 h o < k o π , π' > | |
86 ∎ ) ⟩ | |
87 ( h o < k o π , π' > ) * | |
88 ∎ where open ≈-Reasoning A | |
89 α : {a b c : Obj A } → Hom A (( a ∧ b ) ∧ c ) ( a ∧ ( b ∧ c ) ) | |
90 α = < A [ π o π ] , < A [ π' o π ] , π' > > | |
91 α' : {a b c : Obj A } → Hom A ( a ∧ ( b ∧ c ) ) (( a ∧ b ) ∧ c ) | |
92 α' = < < π , A [ π o π' ] > , A [ π' o π' ] > | |
93 β : {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 > > ] | |
94 β {a} {b} {c} {d} {f} {g} {h} = begin | |
95 α o < < f , g > , h > | |
96 ≈⟨⟩ | |
97 ( < ( π o π ) , < ( π' o π ) , π' > > ) o < < f , g > , h > | |
98 ≈⟨ distr-π ⟩ | |
99 < ( ( π o π ) o < < f , g > , h > ) , ( < ( π' o π ) , π' > o < < f , g > , h > ) > | |
100 ≈⟨ π-cong refl-hom distr-π ⟩ | |
101 < ( ( π o π ) o < < f , g > , h > ) , ( < ( ( π' o π ) o < < f , g > , h > ) , ( π' o < < f , g > , h > ) > ) > | |
102 ≈↑⟨ π-cong assoc ( π-cong assoc refl-hom ) ⟩ | |
103 < ( π o (π o < < f , g > , h >) ) , ( < ( π' o ( π o < < f , g > , h > ) ) , ( π' o < < f , g > , h > ) > ) > | |
104 ≈⟨ π-cong (cdr e3a ) ( π-cong (cdr e3a ) e3b ) ⟩ | |
105 < ( π o < f , g > ) , < ( π' o < f , g > ) , h > > | |
106 ≈⟨ π-cong e3a ( π-cong e3b refl-hom ) ⟩ | |
107 < f , < g , h > > | |
108 ∎ where open ≈-Reasoning A | |
109 | |
67 | 110 |
68 record CCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where | 111 record CCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where |
69 field | 112 field |
70 1 : Obj A | 113 1 : Obj A |
71 ○ : (a : Obj A ) → Hom A a 1 | 114 ○ : (a : Obj A ) → Hom A a 1 |