Mercurial > hg > Members > kono > Proof > category

changeset 355:8fd085379380

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add DataCategory Universal mapping
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 11 May 2015 11:16:24 +0900
parents 2a83718f50a0
children 500c813af3c9
files code-data.agda limit-to.agda
diffstat 2 files changed, 240 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/code-data.agda	Mon May 11 11:16:24 2015 +0900
@@ -0,0 +1,228 @@
+open import Category -- https://github.com/konn/category-agda
+open import Level
+--open import Category.HomReasoning
+open import HomReasoning
+open import cat-utility
+open import Category.Cat
+
+module code-data { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where
+
+record DataObj : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
+   field
+      dom : Obj A
+      codom : Obj A
+      code : Hom A dom codom
+      rev-code : Hom A codom dom
+      id-left  :  A [ A [ code  o rev-code ]  ≈  id1 A codom ]
+
+open DataObj
+
+record isDataHom (a : DataObj ) (b : DataObj ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where
+   field
+      history : Hom A (codom a) (dom b)
+   data-dom = a
+   data-codom = b
+
+open isDataHom
+
+DataHom : (a : DataObj ) (b : DataObj ) → Set (c₁ ⊔ c₂ ⊔ ℓ)
+DataHom = λ a b →  isDataHom a b
+
+DataId : { a : DataObj } → DataHom a a
+DataId {a} = record {
+      history = rev-code a
+   }
+
+_∙_ :  {a b c : DataObj } → DataHom b c → DataHom a b → DataHom a c
+_∙_ {a} {b} {c} g f = record { history = A [ history g o A [ code b o history f ] ] }
+
+_≗_ : {a : DataObj } {b : DataObj } (f g : DataHom a b ) → Set ℓ 
+_≗_ {a} {b} f g = A [  A [ code b o history f ]  ≈  A [ code b o history g ]  ]
+
+open import Relation.Binary.Core
+
+iDataCategory : IsCategory DataObj DataHom _≗_ _∙_  DataId 
+iDataCategory  = record  { isEquivalence =  isEquivalence 
+                    ; identityL =   \{a} {b} {f} -> identityL a b f
+                    ; identityR =   \{a} {b} {f} -> identityR a b f
+                    ; o-resp-≈ =    \{a} {b} {c} {f} {g} {h} {i} -> o-resp {a} {b} {c} {f} {g} {h} {i}
+                    ; associative = \{a} {b} {c} {d} {f} {g} {h} -> associative a b c d f g h
+                    }
+     where
+         open ≈-Reasoning (A) 
+         o-resp :  {A B C : DataObj} {f g : DataHom A B} {h i : DataHom B C} → f ≗ g → h ≗ i → (h ∙ f) ≗ (i ∙ g)
+         o-resp {a} {b} {c} {f} {g} {h} {i} f≗g h≗i =  begin
+                code c o history (h ∙ f) 
+           ≈⟨⟩
+                code c o history h o code b o history f
+           ≈⟨ cdr ( cdr ( f≗g ) ) ⟩
+                code c o history h o code b o history g
+           ≈⟨ assoc ⟩
+                (code c o history h ) o code b o history g
+           ≈⟨ car h≗i ⟩
+                (code c o history i ) o code b o history g
+           ≈⟨ sym assoc ⟩
+                code c o history i o code b o history g
+           ≈⟨⟩
+                code c o history (i ∙ g)
+           ∎ 
+         associative : (a b c d : DataObj)  (f : DataHom c d) (g : DataHom b c) (h : DataHom a b) → (f ∙ (g ∙ h)) ≗ ((f ∙ g) ∙ h)
+         associative a b c d f g h  = begin
+               code d o history (f ∙ (g ∙ h))
+           ≈⟨⟩
+               code d o history f o code c o  history g  o code b o history h  
+           ≈⟨ cdr (cdr assoc ) ⟩
+               code d o history f o (code c o  history g)  o code b o history h  
+           ≈⟨ cdr assoc ⟩
+               code d o (history f o code c o history g) o code b o history h
+           ≈⟨⟩
+               code d o history ((f ∙ g) ∙ h) 
+           ∎
+         identityL : (a : DataObj) (b : DataObj) (f : DataHom a b) → (DataId ∙ f) ≗ f
+         identityL a b f  = begin
+              code b o history (DataId ∙ f) 
+           ≈⟨⟩
+               code b o ( rev-code b o  (code b o history f ))
+           ≈⟨ assoc ⟩
+               (code b o  rev-code b ) o  ( code b o history f )
+           ≈⟨ car (id-left b )  ⟩
+               id1 A (codom b) o  ( code b o history f )
+           ≈⟨ idL ⟩
+              code b o history f 
+           ∎
+         identityR : (a : DataObj) (b : DataObj) (f : DataHom a b) → (f ∙ DataId  ) ≗ f
+         identityR a b f  = begin
+               code b o history (f ∙ DataId) 
+           ≈⟨⟩
+               code b o ( history f  o ( code a   o rev-code a ) )
+           ≈⟨ cdr (cdr (id-left a)) ⟩
+               code b o ( history f  o id1 A (codom a) )
+           ≈⟨ cdr idR ⟩
+               code b o history f
+           ∎
+         isEquivalence : {a : DataObj } {b : DataObj } →
+               IsEquivalence {_} {_} {DataHom a b } _≗_
+         isEquivalence {C} {D} =      -- this is the same function as A's equivalence but has different types
+           record { refl  = refl-hom
+             ; sym   = sym
+             ; trans = trans-hom
+             } 
+DataCategory : Category (c₁ ⊔ c₂ ⊔ ℓ) (c₁ ⊔ c₂ ⊔ ℓ) ℓ
+DataCategory =
+  record { Obj = DataObj
+         ; Hom = DataHom
+         ; _o_ = _∙_ 
+         ; _≈_ = _≗_
+         ; Id  =  DataId 
+         ; isCategory = iDataCategory
+          }
+
+
+
+open Functor
+open NTrans
+
+F : Obj A -> Obj DataCategory  
+F d  = record {
+      dom  = d
+      ; codom = d
+      ; code  = id1 A d
+      ; rev-code  = id1 A d
+      ; id-left = idL
+   }  where open ≈-Reasoning (A)  
+
+U : Functor  DataCategory A
+U = record {
+      FObj = \d -> codom  d
+    ; FMap = \f -> A [ code ( data-codom f ) o history f ] 
+    ; isFunctor = record {
+             ≈-cong   =  \{a} {b} {f} {g} -> ≈-cong-1 {a} {b} {f} {g}
+             ; identity = \{a} -> identity-1 {a}
+             ; distr    = \{a b c f g} -> distr-1 {a} {b} {c} {f} {g}
+      }
+ } where
+    open ≈-Reasoning (A) 
+    ≈-cong-1 :  {a : Obj DataCategory} {b : Obj DataCategory} {f g : Hom DataCategory a b} → DataCategory [ f ≈ g ] → 
+         A [ A [ code (data-codom f) o history f ] ≈ A [ code (data-codom g) o history g ] ]
+    ≈-cong-1 {a} {b} {f} {g}  f≈g =  begin
+              code (data-codom f) o history f 
+           ≈⟨⟩
+              code b o history f 
+           ≈⟨ f≈g ⟩
+              code b o history g 
+           ≈⟨⟩
+              code (data-codom g) o history g 
+           ∎
+    identity-1 :  {a : Obj DataCategory} → A [ A [ code (data-codom (DataId {a})) o history (DataId {a}) ] ≈ id1 A (codom a) ]
+    identity-1 {a} =   begin
+              code (data-codom (DataId {a} )) o history (DataId  {a} )
+           ≈⟨⟩
+               code a o  rev-code a
+           ≈⟨ id-left a ⟩
+              id1 A (codom a)
+           ∎
+    distr-1 :  {a b c : Obj DataCategory} {f : Hom DataCategory a b} {g : Hom DataCategory b c} → 
+             A [ A [ code (data-codom ( g ∙ f )) o history ( g ∙ f ) ] ≈
+                A [ A [ code (data-codom g) o history g ] o A [ code (data-codom f) o history f ] ] ]
+    distr-1 {a} {b} {c} {f} {g} =  begin
+               code (data-codom (g ∙ f )) o history ( g ∙ f ) 
+           ≈⟨⟩
+                code c o history g o  code b o history f
+           ≈⟨ assoc ⟩
+                (code c o history g ) o  code b o history f
+           ≈⟨⟩
+               ( code (data-codom g) o history g ) o ( code (data-codom f) o history f )
+           ∎
+
+eta-map :   (a : Obj A) → Hom A a ( FObj U (F a) )
+eta-map a = id1 A a
+
+
+Lemma1 :  UniversalMapping A DataCategory U F eta-map
+Lemma1 = record {
+         _* =  solution ;
+         isUniversalMapping = record {
+                    universalMapping  = \{a} {b} {f} -> universalMapping {a} {b} {f} ;
+                    uniquness = \{a} {b} {f} {g} -> uniqueness {a} {b} {f} {g}
+              }
+  } where
+    open ≈-Reasoning (A) 
+    solution :  {a : Obj A} {b : Obj DataCategory} → Hom A a (FObj U b) → Hom DataCategory (F a) b
+    solution {a} {b} f = record { history = A [ rev-code b o f ]  }
+    universalMapping :  {a : Obj A} {b : Obj DataCategory} {f : Hom A a (FObj U b)} → A [ A [ FMap U (solution {a} {b} f) o eta-map a ] ≈ f ]
+    universalMapping {a} {b} {f} = begin
+                FMap U (solution {a} {b} f) o eta-map a 
+           ≈⟨⟩
+               (code b o ( rev-code b  o f))  o id1 A a
+           ≈⟨ idR  ⟩
+               code b o ( rev-code b  o f)
+           ≈⟨ assoc  ⟩
+               (code b o  rev-code b  ) o f
+           ≈⟨ car (id-left b) ⟩
+               id1 A (codom b) o f
+           ≈⟨ idL ⟩
+                f
+           ∎
+    uniqueness :  {a : Obj A} {b : Obj DataCategory} {f : Hom A a (FObj U b)}
+        {g : Hom DataCategory (F a) b} →
+        A [ A [ FMap U g o eta-map a ] ≈ f ] →
+        DataCategory [ solution f ≈ g ]
+    uniqueness {a} {b} {f} {g} Uη≈f  =  begin
+               code b o history (solution {a} {b} f)
+           ≈⟨⟩
+               code b o ( rev-code b o f)
+           ≈⟨ sym ( cdr ( cdr  Uη≈f   )) ⟩
+               code b o  rev-code b o ( code b o history g ) o id1 A (codom (F a))
+           ≈⟨ assoc ⟩
+               (code b o  rev-code b ) o ( code b o history g ) o id1 A (codom (F a))
+           ≈⟨ car ( id-left b) ⟩
+               id1 A (codom b ) o ( code b o history g ) o id1 A (codom (F a))
+           ≈⟨ idL ⟩
+               ( code b o history g ) o id1 A (codom (F a))
+           ≈⟨ idR ⟩
+               code b o history g
+           ∎
+
+
+
+
--- a/limit-to.agda	Thu Apr 02 22:49:13 2015 +0900
+++ b/limit-to.agda	Mon May 11 11:16:24 2015 +0900
@@ -20,14 +20,25 @@
 ---       ------>
 ---          g
 
+postulate φ id-0 id-1 f g : Set  c₂
+
 
 infixr 40 _::_
 data  List {a} (A : Set a)  : Set a where
    [] : List A
    _::_ : A -> List A -> List A
 
+data  Maybe  {a} (A : Set a)  : Set a where
+   nothing : Maybe A
+   just : A -> Maybe A
 
-postulate id-0 id-1 f g : Set  c₂
+memberp1 : {a : Level } -> {A : Set a} → A → List A → {!!} -> Maybe A
+memberp1 = {!!}
+
+memberp : {a : Level } -> {A : Set a} → A → List A → Maybe A
+memberp _ []  = nothing
+memberp x ( H :: T ) = memberp1 x T ( x ≡ H )
+
 
 
 data Two {c₁}  : Set c₁ where