Mercurial > hg > Members > kono > Proof > category
changeset 794:ba575c73ea48
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 22 Apr 2019 12:43:49 +0900 |
| parents | f37f11e1b871 |
| children | 030c5b87ed78 |
| files | CCC.agda CCChom.agda |
| diffstat | 2 files changed, 97 insertions(+), 11 deletions(-) [+] |
line wrap: on
line diff
--- a/CCC.agda Mon Apr 22 02:41:53 2019 +0900 +++ b/CCC.agda Mon Apr 22 12:43:49 2019 +0900 @@ -52,8 +52,8 @@ ≈⟨ 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 } → 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 < f , g > o h ≈↑⟨ e3c ⟩ < π o < f , g > o h , π' o < f , g > o h > @@ -62,8 +62,51 @@ ≈⟨ π-cong (car e3a ) (car e3b) ⟩ < f o h , g o h > ∎ - _×_ : { 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 ) - f × g = λ h → < A [ f o A [ π o h ] ] , A [ g o A [ π' 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 π ] , π' > ] ) * ] + distr-* {a} {b} {c} {d} {h} {k} = begin + h * o k + ≈↑⟨ e4b ⟩ + ( ε o < (h * o k ) o π , π' > ) * + ≈⟨ *-cong ( begin + ε o < (h * o k ) o π , π' > + ≈↑⟨ cdr ( π-cong assoc refl-hom ) ⟩ + ε o ( < h * o ( k o π ) , π' > ) + ≈↑⟨ cdr ( π-cong (cdr e3a) e3b ) ⟩ + ε o ( < h * o ( π o < k o π , π' > ) , π' o < k o π , π' > > ) + ≈⟨ cdr ( π-cong assoc refl-hom) ⟩ + ε o ( < (h * o π) o < k o π , π' > , π' o < k o π , π' > > ) + ≈↑⟨ cdr ( distr-π ) ⟩ + ε o ( < h * o π , π' > o < k o π , π' > ) + ≈⟨ assoc ⟩ + ( ε o < h * o π , π' > ) o < k o π , π' > + ≈⟨ car e4a ⟩ + 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 π ] , π' > > + α' : {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 > > ] + β {a} {b} {c} {d} {f} {g} {h} = begin + α o < < f , g > , h > + ≈⟨⟩ + ( < ( π o π ) , < ( π' o π ) , π' > > ) o < < f , g > , h > + ≈⟨ distr-π ⟩ + < ( ( π o π ) o < < f , g > , h > ) , ( < ( π' o π ) , π' > o < < f , g > , h > ) > + ≈⟨ π-cong refl-hom distr-π ⟩ + < ( ( π o π ) o < < f , g > , h > ) , ( < ( ( π' o π ) o < < f , g > , h > ) , ( π' o < < f , g > , h > ) > ) > + ≈↑⟨ π-cong assoc ( π-cong assoc refl-hom ) ⟩ + < ( π o (π o < < f , g > , h >) ) , ( < ( π' o ( π o < < f , g > , h > ) ) , ( π' o < < f , g > , h > ) > ) > + ≈⟨ π-cong (cdr e3a ) ( π-cong (cdr e3a ) e3b ) ⟩ + < ( π 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 field
--- a/CCChom.agda Mon Apr 22 02:41:53 2019 +0900 +++ b/CCChom.agda Mon Apr 22 12:43:49 2019 +0900 @@ -85,7 +85,7 @@ ; ccc-3 = record { ≅→ = c301 ; ≅← = c302 ; iso→ = c303 ; iso← = c304 ; cong← = c305 ; cong→ = c306 } ; nat-2 = nat-2 ; nat-3 = nat-3 } - } where + } module CCC→HOM where c101 : {a : Obj A} → Hom A a (CCC.１ c) → Hom OneCat OneObj OneObj c101 _ = OneObj c102 : {a : Obj A} → Hom OneCat OneObj OneObj → Hom A a (CCC.１ c) @@ -166,11 +166,54 @@ c301 k ∎ where open ≈-Reasoning A -lemma1 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( ccc : CCC A ) → {a b c : Obj A} → -- Hom A １ ( c ^ b ) ≅ Hom A b c +U_b : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → ( ccc : CCC A ) → (b : Obj A) → Functor A A +FObj (U_b A ccc b) = λ a → (CCC._<=_ ccc a b ) +FMap (U_b A ccc b) = λ f → CCC._* ccc ( A [ f o CCC.ε ccc ] ) +isFunctor (U_b A ccc b) = isF where + isF : IsFunctor A A ( λ a → (CCC._<=_ ccc a b)) ( λ f → CCC._* ccc ( A [ f o CCC.ε ccc ] ) ) + IsFunctor.≈-cong isF f≈g = IsCCC.*-cong (CCC.isCCC ccc) ( car f≈g ) where open ≈-Reasoning A + -- e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } → A [ ( A [ ε o < A [ k o π ] , π' > ] ) * ≈ k ] + IsFunctor.identity isF {a} = begin + (ccc CCC.*) (A [ id1 A a o CCC.ε ccc ]) + ≈⟨ IsCCC.*-cong (CCC.isCCC ccc) ( begin + id1 A a o CCC.ε ccc + ≈⟨ idL ⟩ + CCC.ε ccc + ≈↑⟨ idR ⟩ + CCC.ε ccc o id1 A (CCC._∧_ ccc ( CCC._<=_ ccc a b ) b ) + ≈↑⟨ cdr ( IsCCC.π-id (CCC.isCCC ccc)) ⟩ + CCC.ε ccc o ( CCC.<_,_> ccc ( CCC.π ccc ) (CCC.π' ccc) ) + ≈↑⟨ cdr ( IsCCC.π-cong (CCC.isCCC ccc) idL refl-hom) ⟩ + CCC.ε ccc o ( CCC.<_,_> ccc ( id1 A (CCC._<=_ ccc a b) o CCC.π ccc ) (CCC.π' ccc) ) + ∎ ) ⟩ + (ccc CCC.*) ( CCC.ε ccc o ( CCC.<_,_> ccc ( id1 A (CCC._<=_ ccc a b) o CCC.π ccc ) (CCC.π' ccc) )) + ≈⟨ IsCCC.e4b (CCC.isCCC ccc) ⟩ + id1 A ((ccc CCC.<= a) b) + ∎ where open ≈-Reasoning A + IsFunctor.distr isF {x} {y} {z} {f} {g} = begin + (ccc CCC.*) ( ( g o f ) o CCC.ε ccc ) + ≈⟨ {!!} ⟩ + (ccc CCC.*) (( g o CCC.ε ccc ) o CCC.<_,_> ccc ((ccc CCC.*) + ( f o ( CCC.ε ccc o CCC.<_,_> ccc (CCC.π ccc o CCC.π ccc ) (CCC.π' ccc)))) (CCC.π' ccc)) + ≈⟨ IsCCC.*-cong (CCC.isCCC ccc) ( cdr ( IsCCC.π-cong (CCC.isCCC ccc) ( begin + (ccc CCC.*) ( f o ( CCC.ε ccc o CCC.<_,_> ccc (CCC.π ccc o CCC.π ccc ) (CCC.π' ccc))) + ≈⟨ IsCCC.*-cong (CCC.isCCC ccc) assoc ⟩ + (ccc CCC.*) (( f o CCC.ε ccc ) o CCC.<_,_> ccc (CCC.π ccc o CCC.π ccc ) (CCC.π' ccc)) + ≈↑⟨ IsCCC.distr-* (CCC.isCCC ccc) ⟩ + (ccc CCC.*) ( f o CCC.ε ccc ) o CCC.π ccc + ∎ ) refl-hom )) ⟩ + (ccc CCC.*) (( g o CCC.ε ccc ) o CCC.<_,_> ccc ( (ccc CCC.*) ( f o CCC.ε ccc ) o CCC.π ccc ) (CCC.π' ccc) ) + ≈↑⟨ IsCCC.distr-* (CCC.isCCC ccc) ⟩ + (ccc CCC.*) ( g o CCC.ε ccc ) o (ccc CCC.*) ( f o CCC.ε ccc ) + ∎ where open ≈-Reasoning A + + + +c^b=b<=c : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( ccc : CCC A ) → {a b c : Obj A} → -- Hom A １ ( c ^ b ) ≅ Hom A b c IsoS A A (CCC.１ ccc ) (CCC._<=_ ccc c b) b c -lemma1 A ccc {a} {b} {c} = record { - ≅→ = λ f → A [ CCC.ε ccc o CCC.<_,_> ccc ( A [ f o CCC.○ ccc b ] ) ( id1 A b ) ] - ; ≅← = λ f → CCC._* ccc ( A [ f o CCC.π' ccc ] ) +c^b=b<=c A ccc {a} {b} {c} = record { + ≅→ = λ f → A [ CCC.ε ccc o CCC.<_,_> ccc ( A [ f o CCC.○ ccc b ] ) ( id1 A b ) ] --- g ’ (g : 1 → b ^ a) of + ; ≅← = λ f → CCC._* ccc ( A [ f o CCC.π' ccc ] ) --- ┌ f ┐ name of (f : b ^a → 1 ) ; iso→ = iso→ ; iso← = iso← ; cong→ = cong* @@ -188,7 +231,7 @@ CCC.ε ccc o ( CCC.<_,_> ccc (CCC._* ccc (f o CCC.π' ccc) o ( CCC.π ccc o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) ) ) ((CCC.π' ccc) o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) ) ) ≈⟨ cdr ( IsCCC.π-cong ( CCC.isCCC ccc ) assoc refl-hom ) ⟩ CCC.ε ccc o ( CCC.<_,_> ccc ((CCC._* ccc (f o CCC.π' ccc) o CCC.π ccc ) o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) ) ((CCC.π' ccc) o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) ) ) - ≈↑⟨ cdr ( IsCCC.distr ( CCC.isCCC ccc ) ) ⟩ + ≈↑⟨ cdr ( IsCCC.distr-π ( CCC.isCCC ccc ) ) ⟩ CCC.ε ccc o ( CCC.<_,_> ccc (CCC._* ccc (f o CCC.π' ccc) o CCC.π ccc ) (CCC.π' ccc) o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) ) ≈⟨ assoc ⟩ ( CCC.ε ccc o CCC.<_,_> ccc (CCC._* ccc (f o CCC.π' ccc) o CCC.π ccc ) (CCC.π' ccc) ) o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) @@ -222,7 +265,7 @@ CCC._* ccc (( CCC.ε ccc o ( CCC.<_,_> ccc ( f o (CCC.○ ccc b) ) (id1 A b ))) o (CCC.π' ccc)) ≈↑⟨ IsCCC.*-cong ( CCC.isCCC ccc ) assoc ⟩ CCC._* ccc ( CCC.ε ccc o (( CCC.<_,_> ccc ( f o (CCC.○ ccc b) ) (id1 A b )) o (CCC.π' ccc))) - ≈⟨ IsCCC.*-cong ( CCC.isCCC ccc ) (cdr ( IsCCC.distr ( CCC.isCCC ccc ) ) ) ⟩ + ≈⟨ IsCCC.*-cong ( CCC.isCCC ccc ) (cdr ( IsCCC.distr-π ( CCC.isCCC ccc ) ) ) ⟩ CCC._* ccc ( CCC.ε ccc o CCC.<_,_> ccc ( (f o (CCC.○ ccc b)) o CCC.π' ccc ) (id1 A b o CCC.π' ccc) ) ≈⟨ IsCCC.*-cong ( CCC.isCCC ccc ) (cdr ( IsCCC.π-cong ( CCC.isCCC ccc ) lemma idL )) ⟩ CCC._* ccc ( CCC.ε ccc o CCC.<_,_> ccc ( f o CCC.π ccc ) (CCC.π' ccc) )