Mercurial > hg > Members > kono > Proof > category
diff src/CCC.agda @ 967:472bcadfd216
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 25 Feb 2021 13:08:17 +0900 |
| parents | 396bf884f5e7 |
| children | 5f76e5cf3d49 |
line wrap: on
line diff
--- a/src/CCC.agda Thu Feb 25 11:13:31 2021 +0900 +++ b/src/CCC.agda Thu Feb 25 13:08:17 2021 +0900 @@ -32,29 +32,29 @@ e4a : {a b c : Obj A} → { h : Hom A (c ∧ b) a } → A [ A [ ε o < A [ (h *) o π ] , π' > ] ≈ h ] e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } → A [ ( A [ ε o < A [ k o π ] , π' > ] ) * ≈ k ] *-cong : {a b c : Obj A} → { f f' : Hom A (a ∧ b) c } → A [ f ≈ f' ] → A [ f * ≈ f' * ] - - e'2 : A [ ○ １ ≈ id1 A １ ] - e'2 = let open ≈-Reasoning A in begin + open ≈-Reasoning A + e'2 : ○ １ ≈ id1 A １ + e'2 = begin ○ １ ≈↑⟨ e2 ⟩ id1 A １ ∎ - e''2 : {a b : Obj A} {f : Hom A a b } → A [ A [ ○ b o f ] ≈ ○ a ] - e''2 {a} {b} {f} = let open ≈-Reasoning A in begin + e''2 : {a b : Obj A} {f : Hom A a b } → ( ○ b o f ) ≈ ○ a + e''2 {a} {b} {f} = begin ○ b o f ≈⟨ e2 ⟩ ○ a ∎ - π-id : {a b : Obj A} → A [ < π , π' > ≈ id1 A (a ∧ b ) ] - π-id {a} {b} = let open ≈-Reasoning A in begin + π-id : {a b : Obj A} → < π , π' > ≈ id1 A (a ∧ b ) + π-id {a} {b} = begin < π , π' > ≈↑⟨ π-cong idR idR ⟩ < π o id1 A (a ∧ b) , π' o id1 A (a ∧ b) > ≈⟨ e3c ⟩ id1 A (a ∧ b ) ∎ - 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 ] > ] - distr-π {a} {b} {c} {d} {f} {g} {h} = let open ≈-Reasoning A in begin + 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 ) > + distr-π {a} {b} {c} {d} {f} {g} {h} = begin < f , g > o h ≈↑⟨ e3c ⟩ < π o < f , g > o h , π' o < f , g > o h > @@ -64,8 +64,28 @@ < f o h , g o h > ∎ _×_ : { a b c d : Obj A } ( f : Hom A a c ) (g : Hom A b d ) → Hom A (a ∧ b) ( c ∧ d ) - f × g = < (A [ f o π ] ) , (A [ g o π' ]) > - 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 π ] , π' > ] ) * ] + f × g = < ( f o π ) , (g o π' ) > + π-exchg : {a b c : Obj A} {f : Hom A c a }{g : Hom A c b } → < π' , π > o < f , g > ≈ < g , f > + π-exchg {a} {b} {c} {f} {g} = begin + < π' , π > o < f , g > + ≈⟨ distr-π ⟩ + < π' o < f , g > , π o < f , g > > + ≈⟨ π-cong e3b e3a ⟩ + < g , f > + ∎ + π'π : {a b : Obj A} → < π' , π > o < π' , π > ≈ id1 A (a ∧ b) + π'π = trans-hom π-exchg π-id + 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 π > + exchg-π {a} {b} {c} {d} {f} {g} = begin + < f o π , g o π' > o < π' , π > + ≈⟨ distr-π ⟩ + < (f o π) o < π' , π > , (g o π' ) o < π' , π > > + ≈↑⟨ π-cong assoc assoc ⟩ + < f o (π o < π' , π > ) , g o (π' o < π' , π >)> + ≈⟨ π-cong (cdr e3a) (cdr e3b) ⟩ + < f o π' , g o π > + ∎ + 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 π ) , π' > ) * distr-* {a} {b} {c} {d} {h} {k} = begin h * o k ≈↑⟨ e4b ⟩ @@ -86,12 +106,12 @@ h o < k o π , π' > ∎ ) ⟩ ( h o < k o π , π' > ) * - ∎ where open ≈-Reasoning A + ∎ α : {a b c : Obj A } → Hom A (( a ∧ b ) ∧ c ) ( a ∧ ( b ∧ c ) ) - α = < A [ π o π ] , < A [ π' o π ] , π' > > + α = < ( π o π ) , < ( π' o π ) , π' > > α' : {a b c : Obj A } → Hom A ( a ∧ ( b ∧ c ) ) (( a ∧ b ) ∧ c ) - α' = < < π , A [ π o π' ] > , A [ π' o π' ] > - β : {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 > > ] + α' = < < π , ( π o π' ) > , ( π' o π' ) > + β : {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 > > β {a} {b} {c} {d} {f} {g} {h} = begin α o < < f , g > , h > ≈⟨⟩ @@ -106,7 +126,7 @@ < ( π o < f , g > ) , < ( π' o < f , g > ) , h > > ≈⟨ π-cong e3a ( π-cong e3b refl-hom ) ⟩ < f , < g , h > > - ∎ where open ≈-Reasoning A + ∎ record CCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where