Mercurial > hg > Members > kono > Proof > category

changeset 410:508c88223aab

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add reasoning
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 23 Mar 2016 11:16:16 +0900
parents cb03612d8162
children 33958fdfc77e
files limit-to.agda
diffstat 1 files changed, 77 insertions(+), 50 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Wed Mar 23 10:57:00 2016 +0900
+++ b/limit-to.agda	Wed Mar 23 11:16:16 2016 +0900
@@ -31,7 +31,7 @@
 -- arrow composition
 
 
-_×_ :  { c₁  c₂ : Level }  -> {A B C : TwoObject { c₁} } →  Maybe ( TwoObject   { c₂ }) →  Maybe ( TwoObject    { c₂ })  →  Maybe ( TwoObject  { c₂ })  
+_×_ :  ∀ { c₁  c₂ }  -> {A B C : TwoObject { c₁} } →  Maybe ( TwoObject   { c₂ }) →  Maybe ( TwoObject    { c₂ })  →  Maybe ( TwoObject  { c₂ })  
 _×_   nothing _  = nothing
 _×_   (just _) nothing  = nothing
 _×_   { c₁} { c₂} {t1} {t1} {t1} _ f   =  f
@@ -41,70 +41,97 @@
 _×_   { c₁} { c₂} {a} {b} {c} (just f)  (just g)   =  nothing
 
 
-_==_ : { c₁ c₂ : Level}   {a b : TwoObject {c₁} } ->  Rel (Maybe (TwoObject  { c₂ })) (c₂) 
+_==_ :  ∀{ c₂ }  ->  Rel (Maybe (TwoObject  { c₂ })) (c₂) 
 _==_   =  Eq   _≡_ 
 
-==refl : ∀ {x} → _==_ x x
-==refl {just x}  = just refl
-==refl {nothing} = nothing
+==refl :  ∀{ c₂ } ->  ∀ {x : Maybe (TwoObject  { c₂ })} → _==_ x x
+==refl {_} {just x}  = just refl
+==refl {_} {nothing} = nothing
 
-==sym : ∀ {x y} → _==_ x  y → _==_ y  x
+==sym :  ∀{ c₂ } -> ∀ {x y :  Maybe (TwoObject  { c₂ })} → _==_ x  y → _==_ y  x
 ==sym (just x≈y) = just (≡-sym x≈y)
 ==sym nothing    = nothing
 
-==trans : ∀ {x y z} → _==_ x  y → _==_ y  z → _==_ x  z
+==trans :  ∀{ c₂ } -> ∀ {x y z :   Maybe (TwoObject  { c₂ }) } → _==_ x  y → _==_ y  z → _==_ x  z
 ==trans (just x≈y) (just y≈z) = just (≡-trans x≈y y≈z)
 ==trans nothing    nothing    = nothing
 
+module ==-Reasoning { c₁ c₂ : Level} where
+
+        infixr  2 _∎
+        infixr 2 _==⟨_⟩_ _==⟨⟩_
+        infix  1 begin_
+
+
+        data _IsRelatedTo_   (x y : (Maybe (TwoObject  { c₂ }))) :
+                             Set  c₂ where
+            relTo : (x≈y : x  == y  ) → x IsRelatedTo y
+
+        begin_ :  {x : Maybe (TwoObject  { c₂ }) } {y : Maybe (TwoObject  { c₂ })} →
+                   x IsRelatedTo y →  x ==  y 
+        begin relTo x≈y = x≈y
+
+        _==⟨_⟩_ :  (x :  Maybe (TwoObject  { c₂ })) {y z :  Maybe (TwoObject  { c₂ }) } →
+                    x == y  → y IsRelatedTo z → x IsRelatedTo z
+        _ ==⟨ x≈y ⟩ relTo y≈z = relTo (==trans x≈y y≈z)
+
+        _==⟨⟩_ :  (x : Maybe (TwoObject  { c₂ })) {y : Maybe (TwoObject  { c₂ })} 
+                    → x IsRelatedTo y → x IsRelatedTo y
+        _ ==⟨⟩ x≈y = x≈y
+
+        _∎ :  (x :  Maybe (TwoObject  { c₂ })) → x IsRelatedTo x
+        _∎ _ = relTo ==refl
+
+
 
 --          f    g    h
 --       d <- c <- b <- a
 
 assoc-× :   { c₁  c₂ : Level } {a b c d : TwoObject  { c₁} } {f g h : Maybe (TwoObject  { c₂ })} → 
-     _==_ { c₁} { c₂} {a} {d}  (  _×_ { c₁} { c₂} {a} {b} {d} f ( _×_ { c₁} { c₂} {a} {b} {c} g h )  )
+      (  _×_ { c₁} { c₂} {a} {b} {d} f ( _×_ { c₁} { c₂} {a} {b} {c} g h )  ) ==
                 (  _×_ { c₁} { c₂} {a} {c} {d}  ( _×_ { c₁} { c₂} {b} {c} {d} f g )   h )
---    [ f × (g × h) == (f × g) × h ]
+--    ( f × (g × h)) == ((f × g) × h )
 assoc-× {_} {_} {_} {_} {_} {_} {nothing} {_} {_} = nothing
 assoc-× {_} {_} {_} {_} {_} {_} {just _} {nothing} {_} = nothing
-assoc-,AW(B {_} {_} {t0} {t0} {t0} {t0} {just _} {just _} {just _} = just refl
-assoc-,AW(B {_} {_} {t0} {t0} {t0} {t0} {just _} {just _} {nothing} = nothing
-assoc-,AW(B {_} {_} {t0} {t0} {t0} {t1} {just _} {just _} {just _} = just refl
-assoc-,AW(B {_} {_} {t0} {t0} {t0} {t1} {just _} {just _} {nothing} = nothing
-assoc-,AW(B {_} {_} {t0} {t0} {t1} {t0} {just _} {just _} {just _} =  {!!}
-assoc-,AW(B {_} {_} {t0} {t0} {t1} {t0} {just _} {just _} {nothing} = nothing
-assoc-,AW(B {_} {_} {t0} {t0} {t1} {t1} {just _} {just _} {nothing} = nothing
-assoc-,AW(B {_} {_} {t0} {t0} {t1} {t1} {just t0} {just t0} {just t0} = just refl
-assoc-,AW(B {_} {_} {t0} {t0} {t1} {t1} {just t0} {just t0} {just t1} = {!!}
-assoc-,AW(B {_} {_} {t0} {t0} {t1} {t1} {just t0} {just t1} {just t0} = just refl
-assoc-,AW(B {_} {_} {t0} {t0} {t1} {t1} {just t0} {just t1} {just t1} = {!!}
-assoc-,AW(B {_} {_} {t0} {t0} {t1} {t1} {just t1} {just t0} {just t0} = {!!}
-assoc-,AW(B {_} {_} {t0} {t0} {t1} {t1} {just t1} {just t0} {just t1} = just refl
-assoc-,AW(B {_} {_} {t0} {t0} {t1} {t1} {just t1} {just t1} {just t0} = {!!}
-assoc-,AW(B {_} {_} {t0} {t0} {t1} {t1} {just t1} {just t1} {just t1} = just refl
-assoc-,AW(B {_} {_} {t0} {t1} {t0} {t0} {just _} {just _} {just _} = nothing
-assoc-,AW(B {_} {_} {t0} {t1} {t0} {t0} {just _} {just _} {nothing} = nothing
-assoc-,AW(B {_} {_} {t0} {t1} {t0} {t1} {just _} {just _} {just _} = nothing
-assoc-,AW(B {_} {_} {t0} {t1} {t0} {t1} {just _} {just _} {nothing} = nothing
-assoc-,AW(B {_} {_} {t0} {t1} {t1} {t0} {just _} {just _} {just _} = nothing
-assoc-,AW(B {_} {_} {t0} {t1} {t1} {t0} {just _} {just _} {nothing} = nothing
-assoc-,AW(B {_} {_} {t0} {t1} {t1} {t1} {just _} {just _} {just _} = just refl
-assoc-,AW(B {_} {_} {t0} {t1} {t1} {t1} {just _} {just _} {nothing} = nothing
-assoc-,AW(B {_} {_} {t1} {t0} {t0} {t0} {just _} {just _} {just _} = nothing
-assoc-,AW(B {_} {_} {t1} {t0} {t0} {t0} {just _} {just _} {nothing} = nothing
-assoc-,AW(B {_} {_} {t1} {t0} {t0} {t1} {just _} {just _} {just _} = nothing
-assoc-,AW(B {_} {_} {t1} {t0} {t0} {t1} {just _} {just _} {nothing} = nothing
-assoc-,AW(B {_} {_} {t1} {t0} {t1} {t0} {just _} {just _} {just _} = nothing
-assoc-,AW(B {_} {_} {t1} {t0} {t1} {t0} {just _} {just _} {nothing} = nothing
-assoc-,AW(B {_} {_} {t1} {t0} {t1} {t1} {just _} {just _} {just _} = {!!}
-assoc-,AW(B {_} {_} {t1} {t0} {t1} {t1} {just _} {just _} {nothing} = nothing
-assoc-,AW(B {_} {_} {t1} {t1} {t0} {t0} {just _} {just _} {just _} = nothing
-assoc-,AW(B {_} {_} {t1} {t1} {t0} {t0} {just _} {just _} {nothing} = nothing
-assoc-,AW(B {_} {_} {t1} {t1} {t0} {t1} {just _} {just _} {just _} = nothing
-assoc-,AW(B {_} {_} {t1} {t1} {t0} {t1} {just _} {just _} {nothing} = nothing
-assoc-,AW(B {_} {_} {t1} {t1} {t1} {t0} {just _} {just _} {just _} = nothing
-assoc-,AW(B {_} {_} {t1} {t1} {t1} {t0} {just _} {just _} {nothing} = nothing
-assoc-,AW(B {_} {_} {t1} {t1} {t1} {t1} {just _} {just _} {just _} = just refl
-assoc-,AW(B {_} {_} {t1} {t1} {t1} {t1} {just _} {just _} {nothing} = nothing
+assoc-× {_} {_} {t0} {t0} {t0} {t0} {just _} {just _} {nothing} = nothing
+assoc-× {_} {_} {t0} {t0} {t0} {t1} {just _} {just _} {nothing} = nothing
+assoc-× {_} {_} {t0} {t0} {t1} {t0} {just _} {just _} {nothing} = nothing
+assoc-× {_} {_} {t0} {t0} {t1} {t1} {just _} {just _} {nothing} = nothing
+assoc-× {_} {_} {t0} {t1} {t0} {t0} {just _} {just _} {nothing} = nothing
+assoc-× {_} {_} {t0} {t1} {t0} {t1} {just _} {just _} {nothing} = nothing
+assoc-× {_} {_} {t0} {t1} {t1} {t0} {just _} {just _} {nothing} = nothing
+assoc-× {_} {_} {t0} {t1} {t1} {t1} {just _} {just _} {nothing} = nothing
+assoc-× {_} {_} {t1} {t0} {t0} {t0} {just _} {just _} {nothing} = nothing
+assoc-× {_} {_} {t1} {t0} {t0} {t1} {just _} {just _} {nothing} = nothing
+assoc-× {_} {_} {t1} {t0} {t1} {t0} {just _} {just _} {nothing} = nothing
+assoc-× {_} {_} {t1} {t0} {t1} {t1} {just _} {just _} {nothing} = nothing
+assoc-× {_} {_} {t1} {t1} {t0} {t0} {just _} {just _} {nothing} = nothing
+assoc-× {_} {_} {t1} {t1} {t0} {t1} {just _} {just _} {nothing} = nothing
+assoc-× {_} {_} {t1} {t1} {t1} {t0} {just _} {just _} {nothing} = nothing
+assoc-× {_} {_} {t1} {t1} {t1} {t1} {just _} {just _} {nothing} = nothing
+assoc-× {_} {_} {t0} {t0} {t0} {t0} {just _} {just _} {just _} = just refl
+assoc-× {_} {_} {t0} {t0} {t0} {t1} {just _} {just _} {just _} = just refl
+assoc-× {_} {_} {t0} {t1} {t1} {t1} {just _} {just _} {just _} = just refl
+assoc-× {_} {_} {t1} {t1} {t1} {t1} {just _} {just _} {just _} = just refl
+assoc-× {_} {_} {t0} {t0} {t1} {t0} {just _} {just _} {just _} =  {!!}
+assoc-× {_} {_} {t0} {t0} {t1} {t1} {just t0} {just t0} {just t0} = just refl
+assoc-× {_} {_} {t0} {t0} {t1} {t1} {just t0} {just t1} {just t0} = just refl
+assoc-× {_} {_} {t0} {t0} {t1} {t1} {just t1} {just t0} {just t1} = just refl
+assoc-× {_} {_} {t0} {t0} {t1} {t1} {just t1} {just t1} {just t1} = just refl
+assoc-× {_} {_} {t0} {t0} {t1} {t1} {just t1} {just t1} {just t0} = {!!}
+assoc-× {_} {_} {t0} {t0} {t1} {t1} {just t1} {just t0} {just t0} = {!!}
+assoc-× {_} {_} {t0} {t0} {t1} {t1} {just t0} {just t1} {just t1} = {!!}
+assoc-× {_} {_} {t0} {t0} {t1} {t1} {just t0} {just t0} {just t1} = {!!}
+assoc-× {_} {_} {t0} {t1} {t0} {t0} {just _} {just _} {just _} = nothing
+assoc-× {_} {_} {t0} {t1} {t0} {t1} {just _} {just _} {just _} = nothing
+assoc-× {_} {_} {t0} {t1} {t1} {t0} {just _} {just _} {just _} = nothing
+assoc-× {_} {_} {t1} {t0} {t0} {t0} {just _} {just _} {just _} = nothing
+assoc-× {_} {_} {t1} {t0} {t0} {t1} {just _} {just _} {just _} = nothing
+assoc-× {_} {_} {t1} {t0} {t1} {t0} {just _} {just _} {just _} = nothing
+assoc-× {_} {_} {t1} {t0} {t1} {t1} {just _} {just _} {just _} = {!!}
+assoc-× {_} {_} {t1} {t1} {t0} {t0} {just _} {just _} {just _} = nothing
+assoc-× {_} {_} {t1} {t1} {t0} {t1} {just _} {just _} {just _} = nothing
+assoc-× {_} {_} {t1} {t1} {t1} {t0} {just _} {just _} {just _} = nothing
 
 
 
@@ -125,11 +152,11 @@
     _≈_ =    Eq  _≡_   ;
     Id  =  \{a} -> TwoId { c₁ } {  c₂} {a} ;
     isCategory  = record {
-            isEquivalence =  record {refl = {!!}  ; trans = {!!}  ; sym = {!!}  } ;
+            isEquivalence =  record {refl = ==refl ; trans = ==trans ; sym = ==sym } ;
             identityL  = {!!} ;
             identityR  = {!!} ;
             o-resp-≈  =  {!!} ;
-            associative  = {!!}
+            associative  = assoc-×
        } 
    }