# HG changeset patch # User Shinji KONO # Date 1555923603 -32400 # Node ID 030c5b87ed78375d666f25a6f25588f17157c94c # Parent ba575c73ea48d9525ba270754e3577bc6c858e3e ccc to adjunction done diff -r ba575c73ea48 -r 030c5b87ed78 CCChom.agda --- a/CCChom.agda Mon Apr 22 12:43:49 2019 +0900 +++ b/CCChom.agda Mon Apr 22 18:00:03 2019 +0900 @@ -4,7 +4,7 @@ open import HomReasoning open import cat-utility -open import Data.Product renaming (_×_ to _∧_) +open import Data.Product renaming (_×_ to _/\_ ) hiding ( <_,_> ) open import Category.Constructions.Product open import Relation.Binary.PropositionalEquality hiding ( [_] ) @@ -170,43 +170,115 @@ 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 ] ) ) + _<=_ = CCC._<=_ ccc + _∧_ = CCC._∧_ ccc + <_,_> = CCC.<_,_> ccc + _* = CCC._* ccc + ε = CCC.ε ccc + π = CCC.π ccc + π' = CCC.π' ccc + isc = CCC.isCCC ccc + *-cong = IsCCC.*-cong (CCC.isCCC ccc) + π-cong = IsCCC.π-cong (CCC.isCCC ccc) + + isF : IsFunctor A A ( λ a → (a <= b)) ( λ f → CCC._* ccc ( A [ f o ε ] ) ) 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 ]) + (id1 A a o ε ) * ≈⟨ 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) )) + ε o id1 A ( ( a <= b ) ∧ b ) + ≈↑⟨ cdr ( IsCCC.π-id isc) ⟩ + ε o ( < π , π' > ) + ≈↑⟨ cdr ( π-cong idL refl-hom) ⟩ + ε o ( < id1 A (a <= b) o π , π' > ) + ∎ ) ⟩ + ( ε o ( < id1 A ( a <= b) o π , π' > ) ) * ≈⟨ IsCCC.e4b (CCC.isCCC ccc) ⟩ - id1 A ((ccc CCC.<= a) b) + id1 A (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 ) + ( ( g o f ) o ε ) * + ≈↑⟨ *-cong assoc ⟩ + ( g o (f o ε ) ) * + ≈↑⟨ *-cong ( cdr (IsCCC.e4a isc) ) ⟩ + ( g o ( ε o ( < ( ( f o ε ) * ) o π , π' > ) )) * + ≈⟨ *-cong assoc ⟩ + ( ( g o ε ) o ( < ( ( f o ε ) * ) o π , π' > ) ) * + ≈↑⟨ IsCCC.distr-* isc ⟩ + ( g o ε ) * o ( f o ε ) * + ∎ where open ≈-Reasoning A + +F_b : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → ( ccc : CCC A ) → (b : Obj A) → Functor A A +FObj (F_b A ccc b) = λ a → ( CCC._∧_ ccc a b ) +FMap (F_b A ccc b) = λ f → ( CCC.<_,_> ccc (A [ f o CCC.π ccc ] ) ( CCC.π' ccc) ) +isFunctor (F_b A ccc b) = isF where + _∧_ = CCC._∧_ ccc + <_,_> = CCC.<_,_> ccc + π = CCC.π ccc + π' = CCC.π' ccc + isc = CCC.isCCC ccc + π-cong = IsCCC.π-cong (CCC.isCCC ccc) + + isF : IsFunctor A A ( λ a → (a ∧ b)) ( λ f → < ( A [ f o π ] ) , π' > ) + IsFunctor.≈-cong isF f≈g = π-cong ( car f≈g ) refl-hom where open ≈-Reasoning A + IsFunctor.identity isF {a} = trans-hom (π-cong idL refl-hom ) (IsCCC.π-id isc) where open ≈-Reasoning A + IsFunctor.distr isF {x} {y} {z} {f} {g} = begin + < ( g o f ) o π , π' > + ≈↑⟨ π-cong assoc refl-hom ⟩ + < g o ( f o π ) , π' > + ≈↑⟨ π-cong (cdr (IsCCC.e3a isc )) refl-hom ⟩ + < g o ( π o < ( f o π ) , π' > ) , π' > + ≈⟨ π-cong assoc ( sym-hom (IsCCC.e3b isc )) ⟩ + < ( g o π ) o < ( f o π ) , π' > , π' o < ( f o π ) , π' > > + ≈↑⟨ IsCCC.distr-π isc ⟩ + < ( g o π ) , π' > o < ( f o π ) , π' > ∎ where open ≈-Reasoning A +CCCtoAdj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( ccc : CCC A ) → (b : Obj A ) → coUniversalMapping A A (F_b A ccc b) +CCCtoAdj A ccc b = record { + U = λ a → a <= b + ; ε = ε' + ; _*' = solution + ; iscoUniversalMapping = record { + couniversalMapping = couniversalMapping + ; couniquness = couniquness + } + } where + _<=_ = CCC._<=_ ccc + <_,_> = CCC.<_,_> ccc + _* = CCC._* ccc + ε = CCC.ε ccc + π = CCC.π ccc + π' = CCC.π' ccc + isc = CCC.isCCC ccc + *-cong = IsCCC.*-cong (CCC.isCCC ccc) + ε' : (a : Obj A) → Hom A (FObj (F_b A ccc b) (a <= b)) a + ε' a = ε + solution : { b' : Obj A} {a : Obj A} → Hom A (FObj (F_b A ccc b) a) b' → Hom A a (b' <= b) + solution f = f * + couniversalMapping : {b = b₁ : Obj A} {a : Obj A} + {f : Hom A (FObj (F_b A ccc b) a) b₁} → + A [ A [ ε' b₁ o FMap (F_b A ccc b) (solution f) ] ≈ f ] + couniversalMapping {c} {a} {f} = IsCCC.e4a isc + couniquness : {b = b₁ : Obj A} {a : Obj A} + {f : Hom A (FObj (F_b A ccc b) a) b₁} {g : Hom A a (b₁ <= b)} → + A [ A [ ε' b₁ o FMap (F_b A ccc b) g ] ≈ f ] → A [ solution f ≈ g ] + couniquness {c} {a} {f} {g} eq = begin + f * + ≈↑⟨ *-cong eq ⟩ + ( ε o FMap (F_b A ccc b) g ) * + ≈⟨⟩ + ( ε o < ( g o π ) , π' > ) * + ≈⟨ IsCCC.e4b isc ⟩ + g + ∎ 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 @@ -299,7 +371,7 @@ hom→CCC A h = record { １ = １ ; ○ = ○ - ; _∧_ = _/\_ + ; _∧_ = _∧_ ; <_,_> = <,> ; π = π ; π' = π' @@ -312,21 +384,21 @@ １ = one h ○ : (a : Obj A ) → Hom A a １ ○ a = ≅← ( ccc-1 (isCCChom h ) {_} {OneObj} {OneObj} ) OneObj - _/\_ : Obj A → Obj A → Obj A - _/\_ a b = _*_ h a b - <,> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c ( a /\ b) + _∧_ : Obj A → Obj A → Obj A + _∧_ a b = _*_ h a b + <,> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c ( a ∧ b) <,> f g = ≅← ( ccc-2 (isCCChom h ) ) ( f , g ) - π : {a b : Obj A } → Hom A (a /\ b) a + π : {a b : Obj A } → Hom A (a ∧ b) a π {a} {b} = proj₁ ( ≅→ ( ccc-2 (isCCChom h ) ) (id1 A (_*_ h a b) )) - π' : {a b : Obj A } → Hom A (a /\ b) b + π' : {a b : Obj A } → Hom A (a ∧ b) b π' {a} {b} = proj₂ ( ≅→ ( ccc-2 (isCCChom h ) ) (id1 A (_*_ h a b) )) _<=_ : (a b : Obj A ) → Obj A _<=_ = _^_ h - _* : {a b c : Obj A } → Hom A (a /\ b) c → Hom A a (c <= b) + _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b) _* = ≅← ( ccc-3 (isCCChom h ) ) - ε : {a b : Obj A } → Hom A ((a <= b ) /\ b) a + ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a ε {a} {b} = ≅→ ( ccc-3 (isCCChom h ) {_^_ h a b} {b} ) (id1 A ( _^_ h a b )) - isCCC : CCC.IsCCC A １ ○ _/\_ <,> π π' _<=_ _* ε + isCCC : CCC.IsCCC A １ ○ _∧_ <,> π π' _<=_ _* ε isCCC = record { e2 = e2 ; e3a = e3a @@ -389,7 +461,7 @@ ≈⟨⟩ g ∎ where open ≈-Reasoning A - e3c : {a b c : Obj A} → { h : Hom A c (a /\ b) } → A [ <,> ( A [ π o h ] ) ( A [ π' o h ] ) ≈ h ] + e3c : {a b c : Obj A} → { h : Hom A c (a ∧ b) } → A [ <,> ( A [ π o h ] ) ( A [ π' o h ] ) ≈ h ] e3c {a} {b} {c} {f} = begin <,> ( π o f ) ( π' o f ) ≈⟨⟩ @@ -414,7 +486,7 @@ ≈⟨⟩ <,> f' g' ∎ where open ≈-Reasoning A - e4a : {a b c : Obj A} → { k : Hom A (c /\ b) a } → A [ A [ ε o ( <,> ( A [ (k *) o π ] ) π') ] ≈ k ] + e4a : {a b c : Obj A} → { k : Hom A (c ∧ b) a } → A [ A [ ε o ( <,> ( A [ (k *) o π ] ) π') ] ≈ k ] e4a {a} {b} {c} {k} = begin ε o ( <,> ((k *) o π ) π' ) ≈⟨⟩ @@ -434,7 +506,7 @@ ≈⟨ iso← (ccc-3 (isCCChom h)) ⟩ k ∎ where open ≈-Reasoning A - *-cong : {a b c : Obj A} {f f' : Hom A (a /\ b) c} → A [ f ≈ f' ] → A [ f * ≈ f' * ] + *-cong : {a b c : Obj A} {f f' : Hom A (a ∧ b) c} → A [ f ≈ f' ] → A [ f * ≈ f' * ] *-cong eq = cong← ( ccc-3 (isCCChom h )) eq open import Category.Sets @@ -448,7 +520,7 @@ sets {l} = record { １ = One' ; ○ = λ _ → λ _ → OneObj' - ; _∧_ = _/\_ + ; _∧_ = _∧_ ; <_,_> = <,> ; π = π ; π' = π' @@ -461,21 +533,21 @@ １ = One' ○ : (a : Obj Sets ) → Hom Sets a １ ○ a = λ _ → OneObj' - _/\_ : Obj Sets → Obj Sets → Obj Sets - _/\_ a b = a ∧ b - <,> : {a b c : Obj Sets } → Hom Sets c a → Hom Sets c b → Hom Sets c ( a /\ b) + _∧_ : Obj Sets → Obj Sets → Obj Sets + _∧_ a b = a /\ b + <,> : {a b c : Obj Sets } → Hom Sets c a → Hom Sets c b → Hom Sets c ( a ∧ b) <,> f g = λ x → ( f x , g x ) - π : {a b : Obj Sets } → Hom Sets (a /\ b) a + π : {a b : Obj Sets } → Hom Sets (a ∧ b) a π {a} {b} = proj₁ - π' : {a b : Obj Sets } → Hom Sets (a /\ b) b + π' : {a b : Obj Sets } → Hom Sets (a ∧ b) b π' {a} {b} = proj₂ _<=_ : (a b : Obj Sets ) → Obj Sets a <= b = b → a - _* : {a b c : Obj Sets } → Hom Sets (a /\ b) c → Hom Sets a (c <= b) + _* : {a b c : Obj Sets } → Hom Sets (a ∧ b) c → Hom Sets a (c <= b) f * = λ x → λ y → f ( x , y ) - ε : {a b : Obj Sets } → Hom Sets ((a <= b ) /\ b) a + ε : {a b : Obj Sets } → Hom Sets ((a <= b ) ∧ b) a ε {a} {b} = λ x → ( proj₁ x ) ( proj₂ x ) - isCCC : CCC.IsCCC Sets １ ○ _/\_ <,> π π' _<=_ _* ε + isCCC : CCC.IsCCC Sets １ ○ _∧_ <,> π π' _<=_ _* ε isCCC = record { e2 = e2 ; e3a = λ {a} {b} {c} {f} {g} → e3a {a} {b} {c} {f} {g} @@ -498,19 +570,19 @@ e3b : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} → Sets [ Sets [ π' o ( <,> f g ) ] ≈ g ] e3b = refl - e3c : {a b c : Obj Sets} {h : Hom Sets c (a /\ b)} → + e3c : {a b c : Obj Sets} {h : Hom Sets c (a ∧ b)} → Sets [ <,> (Sets [ π o h ]) (Sets [ π' o h ]) ≈ h ] e3c = refl π-cong : {a b c : Obj Sets} {f f' : Hom Sets c a} {g g' : Hom Sets c b} → Sets [ f ≈ f' ] → Sets [ g ≈ g' ] → Sets [ <,> f g ≈ <,> f' g' ] π-cong refl refl = refl - e4a : {a b c : Obj Sets} {h : Hom Sets (c /\ b) a} → + e4a : {a b c : Obj Sets} {h : Hom Sets (c ∧ b) a} → Sets [ Sets [ ε o <,> (Sets [ h * o π ]) π' ] ≈ h ] e4a = refl e4b : {a b c : Obj Sets} {k : Hom Sets c (a <= b)} → Sets [ (Sets [ ε o <,> (Sets [ k o π ]) π' ]) * ≈ k ] e4b = refl - *-cong : {a b c : Obj Sets} {f f' : Hom Sets (a /\ b) c} → + *-cong : {a b c : Obj Sets} {f f' : Hom Sets (a ∧ b) c} → Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ] *-cong refl = refl