Mercurial > hg > Members > kono > Proof > category

changeset 689:fb9fc9652c04

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix again
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 12 Nov 2017 00:53:32 +0900
parents a5f2ca67e7c5
children 3d41a8edbf63
files cat-utility.agda free-monoid.agda freyd2.agda pullback.agda universal-mapping.agda
diffstat 5 files changed, 56 insertions(+), 96 deletions(-) [+]
line wrap: on
line diff
--- a/cat-utility.agda	Sat Nov 11 21:34:58 2017 +0900
+++ b/cat-utility.agda	Sun Nov 12 00:53:32 2017 +0900
@@ -26,12 +26,12 @@
                              A [ A [ FMap U g o  η a ]  ≈ f ] → B [ f * ≈ g ]
 
         record UniversalMapping  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
+                         ( U : Functor B A )
+                         ( F : Obj A → Obj B )
+                         ( η : (a : Obj A) → Hom A a ( FObj U (F a) ) )
                          : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
             infixr 11 _*
             field
-               U : Functor B A 
-               F : Obj A → Obj B 
-               η : (a : Obj A) → Hom A a ( FObj U (F a) ) 
                _* :  { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (F a ) b
                isUniversalMapping : IsUniversalMapping A B U F η _*
 
@@ -48,12 +48,12 @@
                              B [ B [ ε b o FMap F g ]  ≈ f ] → A [ f *' ≈ g ]
 
         record coUniversalMapping  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
+                         ( F : Functor A B )
+                         ( U : Obj B → Obj A )
+                         ( ε : (b : Obj B) → Hom B ( FObj F (U b) ) b )
                          : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
             infixr 11 _*'
             field
-               F : Functor A B 
-               U : Obj B → Obj A 
-               ε : (b : Obj B) → Hom B ( FObj F (U b) ) b 
                _*' :  { b : Obj B}{ a : Obj A} → ( Hom B (FObj F a) b ) →  Hom A a (U b )
                iscoUniversalMapping : coIsUniversalMapping A B F U ε _*'
 
--- a/free-monoid.agda	Sat Nov 11 21:34:58 2017 +0900
+++ b/free-monoid.agda	Sun Nov 12 00:53:32 2017 +0900
@@ -234,12 +234,9 @@
 eta :  (a : Obj A) → Hom A a ( FObj U (Generator a) )
 eta  a = λ ( x : a ) →  x :: []
 
-FreeMonoidUniveralMapping : UniversalMapping A B 
+FreeMonoidUniveralMapping : UniversalMapping A B U Generator eta
 FreeMonoidUniveralMapping = 
     record {
-       U = U ;
-       F = Generator ;
-       η =  eta ;
        _* = λ {a b} → λ f → solution a b f ; 
        isUniversalMapping = record {
              universalMapping = λ {a b f} → universalMapping {a} {b} {f} ; 
@@ -346,7 +343,7 @@
 -- Eta          x :: []
 -- Epsiron      morph = Φ
 
-adj = UMAdjunction A B FreeMonoidUniveralMapping 
+adj = UMAdjunction A B  U Generator eta FreeMonoidUniveralMapping 
 
  
 
--- a/freyd2.agda	Sat Nov 11 21:34:58 2017 +0900
+++ b/freyd2.agda	Sun Nov 12 00:53:32 2017 +0900
@@ -88,7 +88,7 @@
          where open import Comma1 F G
 
 open Complete
-open HasInitialObject
+open IsInitialObject
 open import Comma1
 open CommaObj
 open LimitPreserve
@@ -181,7 +181,7 @@
 
 KUhasInitialObj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
       (a : Obj A )
-      → HasInitialObject  ( K (Sets) A * ↓ (Yoneda A a) ) ( record  { obj = a ; hom = λ x → id1 A a } )
+      → IsInitialObject  ( K (Sets) A * ↓ (Yoneda A a) ) ( record  { obj = a ; hom = λ x → id1 A a } )
 KUhasInitialObj {c₁} {c₂} {ℓ} A a = record {
            initial =  λ b → initial0 b
          ; uniqueness =  λ f → unique f
@@ -277,7 +277,7 @@
 UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
      (U : Functor A (Sets {c₂}) )
      ( i : Obj ( K (Sets) A * ↓ U) )
-     (In : HasInitialObject ( K (Sets) A * ↓ U) i ) 
+     (In : IsInitialObject ( K (Sets) A * ↓ U) i ) 
        → Representable A U (obj i)
 UisRepresentable A U i In = record {
         repr→ = record { TMap = tmap1 ; isNTrans = record { commute = comm1 } }
@@ -369,7 +369,7 @@
 module Adjoint-Functor {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete A I )
      (U : Functor A B )
      (i :  (b : Obj B) → Obj ( K B A b ↓ U) )
-     (In :  (b : Obj B) → HasInitialObject ( K B A b ↓ U) (i b) ) 
+     (In :  (b : Obj B) → IsInitialObject ( K B A b ↓ U) (i b) ) 
         where
 
    tmap-η : (y : Obj B)  → Hom B y (FObj U (obj (i y)))
--- a/pullback.agda	Sat Nov 11 21:34:58 2017 +0900
+++ b/pullback.agda	Sun Nov 12 00:53:32 2017 +0900
@@ -235,11 +235,8 @@
 
 limit2couniv :
      ( lim : ( Γ : Functor I A ) → Limit A I Γ )
-     →  coUniversalMapping A ( A ^ I ) 
+     →  coUniversalMapping A ( A ^ I ) (KI I) ( λ b → a0 ( lim b) ) ( λ b → t0 (lim b) )
 limit2couniv lim  = record {  
-       F =  KI I ;
-       U =  λ b → a0 ( lim b) ;
-       ε = λ b → t0 (lim b) ;
        _*' = λ {b} {a} k → limit (isLimit (lim b )) a k ; 
        iscoUniversalMapping = record {
            couniversalMapping = λ{ b a f} → couniversalMapping1 {b} {a} {f} ;
@@ -267,53 +264,35 @@
 open import Category.Cat
 
 univ2limit :
-     ( univ :  coUniversalMapping A (A ^ I) ) →
+     ( U : Obj (A ^ I) → Obj A  )
+     ( ε : ( b : Obj (A ^ I ) ) → NTrans I A (FObj (KI I) (U b)) b )
+     ( univ :  coUniversalMapping A (A ^ I) (KI I) U ε ) →
      ( Γ : Functor I A ) →   Limit A I Γ 
-univ2limit univ Γ = record {
+univ2limit U ε univ Γ = record {
      a0 = U Γ ;
-     t0 = ε ;
+     t0 = ε Γ ;
      isLimit = record {
              limit = λ a t → limit1 a t ;
              t0f=t = λ {a t i } → t0f=t1 {a} {t} {i}  ;
              limit-uniqueness =  λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f
      }
  } where
-     F : Functor A  (A ^ I)
-     F = coUniversalMapping.F univ
-     U : Obj (A ^ I ) → Obj A 
-     U = coUniversalMapping.U univ
-     η : (i : Obj I) → Hom A (U Γ) (FObj (FObj F (U Γ)) i)
-     η i = {!!}
-     ε :  NTrans I A (K A I (U Γ)) Γ 
-     ε  = record {
-         TMap = λ (i : Obj I) → A [ TMap ( coUniversalMapping.ε univ Γ ) i o η i ] ;
-         isNTrans = record { commute = {!!} }
-       }
-     ε' : ( b : Obj (A ^ I ) ) → NTrans I A (FObj F (U b)) b
-     ε' b = coUniversalMapping.ε univ b
-     limit1' :  (a : Obj A) → NTrans I A (FObj F a) Γ → Hom A a (U Γ)
-     limit1' a t = coUniversalMapping._*' univ {_} {a} t
-     limit1 :  (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a (U Γ)
-     limit1 a t = coUniversalMapping._*' univ {_} {a} (record {
-          TMap = λ (i : Obj I) → A [ TMap t i o {!!} ] ;
-          isNTrans = record { commute = {!!}
-        } } )
+     limit1 :  (a : Obj A) → NTrans I A (FObj (KI I) a) Γ → Hom A a (U Γ)
+     limit1 a t = coUniversalMapping._*' univ {_} {a} t
      t0f=t1 :   {a : Obj A} {t : NTrans I A (K A I a) Γ}  {i : Obj I} →
-                A [ A [ TMap ε i o limit1 a t ] ≈ TMap t i ]
+                A [ A [ TMap (ε Γ) i o limit1 a t ] ≈ TMap t i ]
      t0f=t1 {a} {t} {i} =  let  open ≈-Reasoning (A) in begin
-            TMap ε i o limit1 a t
+            TMap (ε Γ) i o limit1 a t
         ≈⟨⟩
-            TMap ε i o coUniversalMapping._*' univ {Γ} {a} {!!}
-        -- ≈⟨ coIsUniversalMapping.couniversalMapping ( coUniversalMapping.iscoUniversalMapping univ) {Γ} {?} {?} ⟩
-        ≈⟨ {!!} ⟩
+            TMap (ε Γ) i o coUniversalMapping._*' univ t
+        ≈⟨ coIsUniversalMapping.couniversalMapping ( coUniversalMapping.iscoUniversalMapping univ) {Γ} {a} {t} ⟩
             TMap t i
         ∎
      limit-uniqueness1 : { a : Obj A } →  { t : NTrans I A ( K A I a ) Γ } → { f : Hom A a (U Γ)}
-         → ( ∀ { i : Obj I } → A [ A [ TMap  ε i o  f ]  ≈ TMap t i ] ) → A [ limit1 a t ≈ f ]
+         → ( ∀ { i : Obj I } → A [ A [ TMap  (ε Γ) i o  f ]  ≈ TMap t i ] ) → A [ limit1 a t ≈ f ]
      limit-uniqueness1 {a} {t} {f} εf=t = let  open ≈-Reasoning (A) in begin
-            coUniversalMapping._*' univ {!!}
-        ≈⟨ {!!} ⟩
-        -- ≈⟨  ( coIsUniversalMapping.couniquness ( coUniversalMapping.iscoUniversalMapping univ) ) εf=t  ⟩
+            coUniversalMapping._*' univ t
+        ≈⟨  ( coIsUniversalMapping.couniquness ( coUniversalMapping.iscoUniversalMapping univ) ) εf=t  ⟩
             f
         ∎
 
--- a/universal-mapping.agda	Sat Nov 11 21:34:58 2017 +0900
+++ b/universal-mapping.agda	Sun Nov 12 00:53:32 2017 +0900
@@ -17,11 +17,8 @@
 --
 
 Adj2UM : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
-      → Adjunction A B → UniversalMapping A B 
+      → (adj : Adjunction A B ) → UniversalMapping A B (Adjunction.U adj) (FObj (Adjunction.F adj)) (TMap (Adjunction.η adj))
 Adj2UM A B adj = record {
-         U = U ;
-         F = FObj F ;
-         η = TMap η ;
          _* = solution  ;
          isUniversalMapping = record {
                     universalMapping  = universalMapping;
@@ -98,19 +95,16 @@
 --
 
 FunctorF : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
-       → UniversalMapping A B → Functor A B
-FunctorF A B um = record {
+                { U : Functor B A }
+                { F : Obj A → Obj B }
+                { η : (a : Obj A) → Hom A a ( FObj U (F a) ) } 
+       → UniversalMapping A B  U F η → Functor A B
+FunctorF A B {U} {F} {η} um = record {
               FObj = F;
               FMap = myFMap ;
               isFunctor = myIsFunctor
        } where
-    U : Functor B A 
-    U = UniversalMapping.U um
-    F : Obj A → Obj B 
-    F = UniversalMapping.F um
-    η : (a : Obj A) → Hom A a ( FObj U (F a) ) 
-    η = UniversalMapping.η um
-    _* : (UniversalMapping A B) →  { a : Obj A} { b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (F a ) b
+    _* : (UniversalMapping A B U F η ) →  { a : Obj A} { b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (F a ) b
     _* _ = UniversalMapping._* um 
     myFMap : {a b : Obj A} → Hom A a b → Hom B (F a) (F b)
     myFMap f = (_* um)  (A [  η (Category.cod A f )   o f ])
@@ -175,20 +169,17 @@
 -- naturality of η
 --
 nat-η : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
-                 → (um : UniversalMapping A B )  →
-           NTrans  A A identityFunctor ( UniversalMapping.U um ○ FunctorF A B um )
-nat-η A B um = record {
+                 { U : Functor B A }
+                 { F : Obj A → Obj B }
+                 { η : (a : Obj A) → Hom A a ( FObj U (F a) ) } 
+                 → (um : UniversalMapping A B  U F η )  →
+           NTrans  A A identityFunctor ( U ○ FunctorF A B um )
+nat-η A B {U} {F} { η} um = record {
              TMap = η ; isNTrans = myIsNTrans
        } where
-    U : Functor B A 
-    U = UniversalMapping.U um
-    F : Obj A → Obj B 
-    F = UniversalMapping.F um
-    η : (a : Obj A) → Hom A a ( FObj U (F a) ) 
-    η = UniversalMapping.η um
     F' : Functor A B
     F' = FunctorF A B um
-    _* : (UniversalMapping A B) →  { a : Obj A} { b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (F a ) b
+    _* : (UniversalMapping A B U F η ) →  { a : Obj A} { b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (F a ) b
     _* _ = UniversalMapping._* um 
     commute :  {a b : Obj A} {f : Hom A a b}
       → A [ A [ (FMap U (FMap F' f))  o  ( η a ) ]  ≈ A [ (η b ) o f ] ]
@@ -204,20 +195,17 @@
     myIsNTrans = record { commute = commute }
 
 nat-ε : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
-       → (um : UniversalMapping A B  )  →
-           NTrans B B ( FunctorF A B um ○ UniversalMapping.U um ) identityFunctor
-nat-ε A B um = record {
+                 { U : Functor B A }
+                 { F : Obj A → Obj B }
+                 { η : (a : Obj A) → Hom A a ( FObj U (F a) ) }
+       → (um : UniversalMapping A B  U F η  )  →
+           NTrans B B ( FunctorF A B um ○ U ) identityFunctor
+nat-ε A B {U} {F} { η} um = record {
              TMap = ε ; isNTrans = myIsNTrans
        } where
-    U : Functor B A 
-    U = UniversalMapping.U um
-    F : Obj A → Obj B 
-    F = UniversalMapping.F um
-    η : (a : Obj A) → Hom A a ( FObj U (F a) ) 
-    η = UniversalMapping.η um
     F' : Functor A B
     F' = FunctorF A B um
-    _* : (UniversalMapping A B) →  { a : Obj A} { b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (F a ) b
+    _* : (UniversalMapping A B U F η ) →  { a : Obj A} { b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (F a ) b
     _* _ = UniversalMapping._* um 
     ε : ( b : Obj B ) → Hom B ( FObj F' ( FObj U b) ) b
     ε b = (_* um) ( id1 A (FObj U b))
@@ -280,10 +268,13 @@
 -----
 
 UMAdjunction : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') →
-       (um : UniversalMapping A B )  →
+                ( U : Functor B A )
+                ( F' : Obj A → Obj B )
+                ( η' : (a : Obj A) → Hom A a ( FObj U (F' a) ) ) →
+       (um : UniversalMapping A B U F' η' )  →
               Adjunction A B 
-UMAdjunction A B um = record {
-           U = UniversalMapping.U um ;
+UMAdjunction A B U F' η' um = record {
+           U = U  ;
            F = FunctorF A B um ;
            η = nat-η A B um ;
            ε = nat-ε A B um ;
@@ -292,17 +283,13 @@
                adjoint2 = adjoint2
            }
        } where
-          U : Functor B A 
-          U = UniversalMapping.U um
           F : Functor A B
           F = FunctorF A B um
           η : NTrans A A identityFunctor ( U ○  F )
           η = nat-η A B um
-          η' : (a : Obj A) → Hom A a ( FObj U (FObj F a) )
-          η' = TMap (nat-η A B um)
           ε : NTrans B B  ( F ○  U ) identityFunctor
           ε = nat-ε A B um
-          _* : UniversalMapping A B →  { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (FObj F a ) b
+          _* : UniversalMapping A B  U F' η' →  { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (FObj F a ) b
           _* _ = UniversalMapping._* um
           isUniversalMapping = UniversalMapping.isUniversalMapping
           adjoint1 :   { b : Obj B } →
@@ -568,12 +555,9 @@
 UO2UM  : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
                  ( U : Functor B A )
                  ( F : Functor A B ) →
-                 ( uo : UnityOfOppsite A B U F)  → UniversalMapping A B 
+                 ( uo : UnityOfOppsite A B U F)  → UniversalMapping A B U (FObj F) (uo-η-map A B U F uo )
 UO2UM  A B U F uo = record {
          _* = uo-solution A B U F uo  ;
-         U = U ;
-         F = FObj F ;
-         η = uo-η-map A B U F uo  ; 
          isUniversalMapping = record {
                     universalMapping  = universalMapping;
                     uniquness = uniqueness