Mercurial > hg > Members > kono > Proof > category

changeset 278:9fafe4a53f89

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
univ2limit
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 23 Sep 2013 02:39:57 +0900
parents 21ef5ba54458
children 8df8e74e6316
files pullback.agda
diffstat 1 files changed, 11 insertions(+), 38 deletions(-) [+]
line wrap: on
line diff
--- a/pullback.agda	Mon Sep 23 01:10:48 2013 +0900
+++ b/pullback.agda	Mon Sep 23 02:39:57 2013 +0900
@@ -275,62 +275,35 @@
 
 open import Category.Cat
 
-open Adjunction
 
-adjoint2limit : 
-     ( U : Functor (A ^ I) A ) ( η :  NTrans A A identityFunctor ( U ○  (KI I) ) )
+open coUniversalMapping
+ 
+univ2limit : 
+     ( U : Functor (A ^ I) A ) 
      ( ε :   NTrans (A ^ I) (A ^ I)  ( (KI I) ○  U ) identityFunctor )
-     ( adj : Adjunction A (A ^ I) U (KI I) η ε ) →
+     ( univ :  coUniversalMapping A (A ^ I) (KI I) (FObj U) (TMap ε) ) →
      ( Γ : Functor I A ) →   Limit I Γ (FObj U Γ) (TMap ε Γ)
-adjoint2limit U η ε adj Γ = record {
+univ2limit U ε univ Γ = 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
      limit1 :  (a : Obj A) → NTrans I A (K I a) Γ → Hom A a (FObj U Γ)
-     limit1 a t = A [ FMap U t o TMap η a ] 
+     limit1 a t = _*' univ t 
      t0f=t1 :   {a : Obj A} {t : NTrans I A (K I a) Γ} {i : Obj I} →
                 A [ A [ TMap (TMap ε Γ) i o limit1 a t ] ≈ TMap t i ]
      t0f=t1 {a} {t} {i} =  let  open ≈-Reasoning (A) in begin
             TMap (TMap ε Γ) i o limit1 a t
         ≈⟨⟩
-            TMap (TMap ε Γ) i o ( FMap U t  o TMap η a )
-        ≈⟨ assoc  ⟩
-            (TMap (TMap ε Γ) i o  FMap U t ) o TMap η a 
-        ≈⟨ car (nat ε)  ⟩
-           TMap (FMap (KI I) (TMap (TMap ε (FObj (KI I) (FObj Γ i))) i o FMap U (FMap (KI I) (TMap t i)))) i o TMap η a
-        ≈⟨ car (distr (KI I)) ⟩
-            (TMap (TMap ε (FObj (KI I) (FObj Γ i))) i o   FMap (U ○ KI I) (TMap t i)) o TMap η a 
-        ≈↑⟨ assoc  ⟩
-            TMap (TMap ε (FObj (KI I) (FObj Γ i))) i o (  FMap (U ○ KI I) (TMap t i) o TMap η a )
-        ≈⟨ cdr ( nat η ) ⟩
-            TMap (TMap ε (FObj (KI I) (FObj Γ i))) i o ((TMap (FMap (KI I) (TMap η (FObj Γ i))) i) o TMap t i )
-        ≈⟨ assoc ⟩
-            ( TMap (TMap ε (FObj (KI I) (FObj Γ i))) i o (TMap (FMap (KI I) (TMap η (FObj Γ i))) i)) o TMap t i
-        ≈⟨  car ( IsAdjunction.adjoint2 ( isAdjunction adj)) ⟩
-            id1 A  (FObj Γ i) o TMap t i
-        ≈⟨ idL ⟩
+            TMap (TMap ε Γ) i o _*' univ t
+        ≈⟨ coIsUniversalMapping.couniversalMapping ( iscoUniversalMapping univ) ⟩
             TMap t i
         ∎
      limit-uniqueness1 : { a : Obj A } →  { t : NTrans I A ( K I a ) Γ } → { f : Hom A a (FObj U Γ)} 
          → ( ∀ { i : Obj I } → A [ A [ TMap  (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
-            FMap U t  o TMap η a
-        ≈↑⟨ car ( fcong U εf=t ) ⟩
-            (FMap U ( A ^ I [ TMap ε Γ o FMap ( KI I) f ] )) o TMap η a 
-        ≈⟨ car ( distr U ) ⟩
-            (FMap U (TMap ε Γ) o   FMap U ( FMap ( KI I) f) ) o TMap η a 
-        ≈⟨⟩
-            (FMap U (TMap ε Γ) o   FMap (U ○ KI I) f ) o TMap η a 
-        ≈↑⟨ assoc ⟩
-            FMap U (TMap ε Γ) o  ( FMap (U ○ KI I) f o TMap η a ) 
-        ≈⟨ cdr ( nat η )  ⟩
-            FMap U (TMap ε Γ) o ( TMap η (FObj U Γ) o  f )
-        ≈⟨ assoc ⟩
-            (FMap U (TMap ε Γ) o TMap η (FObj U Γ)) o  f
-        ≈⟨  car ( IsAdjunction.adjoint1 ( isAdjunction adj)) ⟩
-            id1 A (FObj U Γ) o  f
-        ≈⟨ idL ⟩
+            _*' univ t
+        ≈⟨  ( coIsUniversalMapping.couniquness ( iscoUniversalMapping univ) ) εf=t  ⟩
             f
         ∎