Mercurial > hg > Members > kono > Proof > category

changeset 982:888e6613b99a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 03 Mar 2021 09:48:32 +0900
parents 0e417c508096
children 7ca3c84d4808
files src/ToposEx.agda
diffstat 1 files changed, 32 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/src/ToposEx.agda	Wed Mar 03 04:51:55 2021 +0900
+++ b/src/ToposEx.agda	Wed Mar 03 09:48:32 2021 +0900
@@ -162,34 +162,45 @@
        g :  Hom A N  a
        g0=f : A [ A [ g o nzero TNat  ]  ≈ f ]
        gs=h : A [ A [ g o nsuc  TNat  ]  ≈ A [ h o < id1 A _ , g > ] ]
+       xnat : NatD A １
 
   p33 : {a : Obj A} (z : Hom A １ a ) ( h : Hom A (N  ∧ a) a )  → prop33  z h
   p33  {a} z h = record {
         g = g
       ; g0=f = iii
       ; gs=h = v
+      ; xnat = xnat
     } where
         xnat : NatD A １
         xnat = record { Nat = N ∧ a ; nzero = < nzero TNat , z > ; nsuc = < nsuc TNat o π , h > }
         fg : Hom A N (N ∧ a )
-        fg = gNat xnat
+        fg = gNat xnat -- < f , g >
         f : Hom A N N
         f = π o fg
         g : Hom A N a
         g = π' o fg
-        ig : f ≈ id1 A N 
-        ig  = begin
-           f   ≈⟨ nat-unique TNat {!!} {!!}  ⟩
-           gNat TNat   ≈↑⟨ nat-unique TNat idL (trans-hom idL (sym idR) ) ⟩
-           id1 A _  ∎
         i : f o nzero TNat  ≈ nzero TNat
         i = begin
-            f o nzero TNat  ≈⟨ car ig  ⟩ id1 A _ o nzero TNat  ≈⟨ idL  ⟩
+            f o nzero TNat  ≈⟨⟩ 
+            (π  o fg) o  nzero TNat  ≈↑⟨ assoc ⟩ 
+            π  o (fg o  nzero TNat ) ≈⟨ cdr (IsToposNat.izero isToposN xnat ) ⟩ 
+            π o nzero xnat ≈⟨ IsCCC.e3a isCCC ⟩ 
             nzero TNat  ∎  
         ii : f o nsuc TNat  ≈ nsuc  TNat o f
         ii = begin
-            f o nsuc TNat  ≈⟨ car ig ⟩ id1 A _ o nsuc TNat  ≈⟨ idL ⟩ nsuc TNat  ≈↑⟨ idR ⟩ nsuc TNat o id1 A _  ≈↑⟨ cdr ig  ⟩
+            f o nsuc TNat  ≈⟨⟩ 
+            (π o fg ) o nsuc TNat  ≈↑⟨ assoc ⟩ 
+            π o ( fg  o nsuc TNat ) ≈⟨ cdr (IsToposNat.isuc isToposN xnat ) ⟩ 
+            π o (nsuc xnat o gNat xnat) ≈⟨ assoc ⟩ 
+            (π o  < nsuc TNat o π , h > ) o gNat xnat ≈⟨ car (IsCCC.e3a isCCC) ⟩ 
+            ( nsuc TNat o π ) o gNat xnat ≈↑⟨ assoc ⟩ 
+             nsuc TNat o ( π  o gNat xnat ) ≈⟨⟩ 
              nsuc  TNat o f  ∎  
+        ig : f ≈ id1 A N 
+        ig  = begin
+           f   ≈⟨ nat-unique TNat i ii ⟩
+           gNat TNat   ≈↑⟨ nat-unique TNat idL (trans-hom idL (sym idR) ) ⟩
+           id1 A _  ∎
         iii : g o nzero TNat ≈ z
         iii = begin
             g o nzero TNat  ≈⟨⟩ (π' o gNat xnat ) o nzero TNat  ≈↑⟨ assoc ⟩ 
@@ -222,7 +233,7 @@
               _+_ = λ {a} f g → prop33.g (p  f ( g o π ))  -- Hom A (N n ∧ a) a
            ;  κ1f+g=f = λ {a} {f} {g} → prop33.g0=f (p f (g o π ) )
            ;  κ2f+g=g = λ {a} {f} {g} → k2 {a} {f} {g}
-           ;  uniqueness = {!!}
+           ;  uniqueness = uniq
            ;  +-cong = λ f=f' g=g' → {!!} -- prop33.g-cong p f=f' (resp refl-hom g=g' )
        }
     } where
@@ -236,6 +247,18 @@
             g o ( π  o   < id1 A N  , prop33.g (p f (g o π)) >)  ≈⟨ cdr (IsCCC.e3a isCCC ) ⟩
             g o id1 A N   ≈⟨ idR ⟩
             g  ∎
+        pp :  {c : Obj A} {h : Hom A (Nat TNat) c} → prop33 ( h o nzero TNat ) ( (h o nsuc TNat)  o π)
+        pp {c} {h} = p ( h o nzero TNat ) ( (h o nsuc TNat)  o π)
+        uniq :  {c : Obj A} {h : Hom A (Nat TNat) c} → 
+            prop33.g pp ≈ h 
+        uniq {c} {h} = begin
+            prop33.g pp    ≈⟨⟩
+            π' o gNat (prop33.xnat pp) ≈↑⟨ cdr (nat-unique (prop33.xnat pp) {{!!}} {!!} {!!}) ⟩
+            π' o {!!} ≈⟨ {!!} ⟩
+            h  ∎
+        
+        -- sym ( nat-unique ? (prop33.g0=f (p ( h o nzero TNat ) ( (h o nsuc TNat)  o π) )) ? )
+