Mercurial > hg > Members > kono > Proof > category

changeset 690:3d41a8edbf63

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix universal mapping done.
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 12 Nov 2017 01:29:47 +0900
parents fb9fc9652c04
children 917e51be9bbf
files cat-utility.agda code-data.agda free-monoid.agda freyd2.agda pullback.agda universal-mapping.agda
diffstat 6 files changed, 61 insertions(+), 39 deletions(-) [+]
line wrap: on
line diff
--- a/cat-utility.agda	Sun Nov 12 00:53:32 2017 +0900
+++ b/cat-utility.agda	Sun Nov 12 01:29:47 2017 +0900
@@ -27,11 +27,11 @@
 
         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
+               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 η _*
 
@@ -49,11 +49,11 @@
 
         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
+               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/code-data.agda	Sun Nov 12 00:53:32 2017 +0900
+++ b/code-data.agda	Sun Nov 12 01:29:47 2017 +0900
@@ -178,8 +178,10 @@
 eta-map a = id1 A a
 
 
-Lemma1 :  UniversalMapping A DataCategory U F eta-map
+Lemma1 :  UniversalMapping A DataCategory U 
 Lemma1 = record {
+         F = F ;
+         η = eta-map ;
          _* =  solution ;
          isUniversalMapping = record {
                     universalMapping  = \{a} {b} {f} -> universalMapping {a} {b} {f} ;
--- a/free-monoid.agda	Sun Nov 12 00:53:32 2017 +0900
+++ b/free-monoid.agda	Sun Nov 12 01:29:47 2017 +0900
@@ -234,9 +234,11 @@
 eta :  (a : Obj A) → Hom A a ( FObj U (Generator a) )
 eta  a = λ ( x : a ) →  x :: []
 
-FreeMonoidUniveralMapping : UniversalMapping A B U Generator eta
+FreeMonoidUniveralMapping : UniversalMapping A B U 
 FreeMonoidUniveralMapping = 
     record {
+       F = Generator ;
+       η = eta ;
        _* = λ {a b} → λ f → solution a b f ; 
        isUniversalMapping = record {
              universalMapping = λ {a b f} → universalMapping {a} {b} {f} ; 
@@ -343,7 +345,7 @@
 -- Eta          x :: []
 -- Epsiron      morph = Φ
 
-adj = UMAdjunction A B  U Generator eta FreeMonoidUniveralMapping 
+adj = UMAdjunction A B U FreeMonoidUniveralMapping 
 
  
 
--- a/freyd2.agda	Sun Nov 12 00:53:32 2017 +0900
+++ b/freyd2.agda	Sun Nov 12 01:29:47 2017 +0900
@@ -405,8 +405,10 @@
          comm1 : B [ B [ FMap U g o hom (i a) ] ≈ B [ B [ FMap U g o tmap-η a ] o FMap (K B A a) g ] ]
          comm1 = let open ≈-Reasoning B in sym idR
 
-   UM : UniversalMapping B A U (λ b → obj (i b)) (tmap-η)
+   UM : UniversalMapping B A U 
    UM = record {
+         F = λ b → obj (i b) ;
+         η = tmap-η ;
          _* = λ f → arrow (solution f)  ;
          isUniversalMapping = record {
             universalMapping  = λ {a} {b} {f} → univ f ;
--- a/pullback.agda	Sun Nov 12 00:53:32 2017 +0900
+++ b/pullback.agda	Sun Nov 12 01:29:47 2017 +0900
@@ -235,8 +235,10 @@
 
 limit2couniv :
      ( lim : ( Γ : Functor I A ) → Limit A I Γ )
-     →  coUniversalMapping A ( A ^ I ) (KI I) ( λ b → a0 ( lim b) ) ( λ b → t0 (lim b) )
+     →  coUniversalMapping A ( A ^ I ) (KI I) 
 limit2couniv lim  = record {  
+       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} ;
@@ -264,19 +266,21 @@
 open import Category.Cat
 
 univ2limit :
-     ( 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 ε ) →
+     ( univ :   coUniversalMapping A (A ^ I) (KI I) ) →
      ( Γ : Functor I A ) →   Limit A I Γ 
-univ2limit U ε univ Γ = record {
-     a0 = U Γ ;
-     t0 = ε Γ ;
+univ2limit univ Γ = record {
+     a0 = (coUniversalMapping.U univ ) Γ  ;
+     t0 = (coUniversalMapping.ε univ ) Γ  ;
      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
+     U : Obj (A ^ I) → Obj A  
+     U b = coUniversalMapping.U univ b
+     ε : ( b : Obj (A ^ I ) ) → NTrans I A (FObj (KI I) (U b)) b 
+     ε b = coUniversalMapping.ε univ b
      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/universal-mapping.agda	Sun Nov 12 00:53:32 2017 +0900
+++ b/universal-mapping.agda	Sun Nov 12 01:29:47 2017 +0900
@@ -17,8 +17,10 @@
 --
 
 Adj2UM : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
-      → (adj : Adjunction A B ) → UniversalMapping A B (Adjunction.U adj) (FObj (Adjunction.F adj)) (TMap (Adjunction.η adj))
+      → (adj : Adjunction A B ) → UniversalMapping A B (Adjunction.U adj) 
 Adj2UM A B adj = record {
+         F = FObj (Adjunction.F adj) ;
+         η = TMap (Adjunction.η adj) ;
          _* = solution  ;
          isUniversalMapping = record {
                     universalMapping  = universalMapping;
@@ -95,16 +97,18 @@
 --
 
 FunctorF : {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) ) } 
-       → UniversalMapping A B  U F η → Functor A B
-FunctorF A B {U} {F} {η} um = record {
+       { U : Functor B A }
+       → UniversalMapping A B  U → Functor A B
+FunctorF A B {U} um = record {
               FObj = F;
               FMap = myFMap ;
               isFunctor = myIsFunctor
        } where
-    _* : (UniversalMapping A B U F η ) →  { a : Obj A} { b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (F a ) b
+    F : Obj A → Obj B 
+    F = UniversalMapping.F um
+    η : (a : Obj A) → Hom A a ( FObj U (F a) )
+    η = UniversalMapping.η um
+    _* : (UniversalMapping A B U ) →  { 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 ])
@@ -170,16 +174,18 @@
 --
 nat-η : {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) ) } 
-                 → (um : UniversalMapping A B  U F η )  →
+                 → (um : UniversalMapping A B  U )  →
            NTrans  A A identityFunctor ( U ○ FunctorF A B um )
-nat-η A B {U} {F} { η} um = record {
+nat-η A B {U} um = record {
              TMap = η ; isNTrans = myIsNTrans
        } where
+    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 U F η ) →  { a : Obj A} { b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (F a ) b
+    _* : (UniversalMapping A B U ) →  { 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 ] ]
@@ -196,16 +202,18 @@
 
 nat-ε : {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) ) }
-       → (um : UniversalMapping A B  U F η  )  →
+       → (um : UniversalMapping A B  U )  →
            NTrans B B ( FunctorF A B um ○ U ) identityFunctor
-nat-ε A B {U} {F} { η} um = record {
+nat-ε A B {U} um = record {
              TMap = ε ; isNTrans = myIsNTrans
        } where
+    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 U F η ) →  { a : Obj A} { b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (F a ) b
+    _* : (UniversalMapping A B U ) →  { 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))
@@ -268,12 +276,10 @@
 -----
 
 UMAdjunction : {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) ) ) →
-       (um : UniversalMapping A B U F' η' )  →
+                ( U : Functor B A ) →
+       (um : UniversalMapping A B U )  →
               Adjunction A B 
-UMAdjunction A B U F' η' um = record {
+UMAdjunction A B U um = record {
            U = U  ;
            F = FunctorF A B um ;
            η = nat-η A B um ;
@@ -283,13 +289,17 @@
                adjoint2 = adjoint2
            }
        } where
+          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
           η : NTrans A A identityFunctor ( U ○  F )
           η = nat-η A B um
           ε : NTrans B B  ( F ○  U ) identityFunctor
           ε = nat-ε A B um
-          _* : UniversalMapping A B  U F' η' →  { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (FObj F a ) b
+          _* : UniversalMapping A B  U  →  { 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 } →
@@ -555,8 +565,10 @@
 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 U (FObj F) (uo-η-map A B U F uo )
+                 ( uo : UnityOfOppsite A B U F)  → UniversalMapping A B U 
 UO2UM  A B U F uo = record {
+         F = FObj F ;
+         η = uo-η-map A B U F uo ;
          _* = uo-solution A B U F uo  ;
          isUniversalMapping = record {
                     universalMapping  = universalMapping;