Mercurial > hg > Members > kono > Proof > category

changeset 475:4c0a955b651d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add license
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 07 Mar 2017 12:31:35 +0900
parents 2d32ded94aaf
children 6ccda88f5561
files LICENSE.TXT discrete.agda pullback.agda
diffstat 3 files changed, 43 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/LICENSE.TXT	Tue Mar 07 12:31:35 2017 +0900
@@ -0,0 +1,39 @@
+Open Source License
+
+Copyright (c) 2013-2017 University of the Ryukyus
+All rights reserved.
+
+Developed by:
+
+    Shinji KONO
+    http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/category
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of
+this software and associated documentation files (the "Software"), to deal with
+the Software without restriction, including without limitation the rights to
+use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
+of the Software, and to permit persons to whom the Software is furnished to do
+so, subject to the following conditions:
+
+    * Redistributions of source code must retain the above copyright notice,
+      this list of conditions and the following disclaimers.
+
+    * Redistributions in binary form must reproduce the above copyright notice,
+      this list of conditions and the following disclaimers in the
+      documentation and/or other materials provided with the distribution.
+
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.  IN NO EVENT SHALL THE
+CONTRIBUTORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS WITH THE
+SOFTWARE.
+
+This program uses 
+
+        https://github.com/konn/category-agda.git
+
+as a base Library.
+
--- a/discrete.agda	Tue Mar 07 08:27:33 2017 +0900
+++ b/discrete.agda	Tue Mar 07 12:31:35 2017 +0900
@@ -94,7 +94,7 @@
 
 record DiscreteObj  {c₁  : Level } (S : Set c₁) :  Set c₁  where
    field
-      obj : S
+      obj : S              -- this is necessary to avoid single object
 
 open DiscreteObj
 
--- a/pullback.agda	Tue Mar 07 08:27:33 2017 +0900
+++ b/pullback.agda	Tue Mar 07 12:31:35 2017 +0900
@@ -217,10 +217,12 @@
 --     F = KI I : Functor A (A ^ I)
 --     U = λ b → A0 (lim b {a0 b} {t0 b}
 --     ε = λ b → T0 ( lim b {a0 b} {t0 b} )
+--
+--     a0 : Obj A and t0 : NTrans K Γ come from the limit
 
 limit2couniv :
      ( lim : ( Γ : Functor I A ) → { a0 : Obj A } { t0 : NTrans I A ( K A I a0 ) Γ } → Limit A I Γ a0 t0 )
-     → ( a0 : ( b : Functor I A ) → Obj A ) ( t0 :  ( b : Functor I A ) → NTrans I A ( K A I (a0 b) ) b )
+     → ( a0 : ( Γ : Functor I A ) → Obj A ) ( t0 :  ( Γ : Functor I A ) → NTrans I A ( K A I (a0 Γ) ) Γ )
      →  coUniversalMapping A ( A ^ I ) (KI I) (λ b → A0 (lim b {a0 b} {t0 b} ) )  ( λ b → T0 ( lim b {a0 b} {t0 b} ) )
 limit2couniv lim a0 t0 = record {  -- F             U                            ε
        _*' = λ {b} {a} k → limit (lim b {a0 b} {t0 b} ) a k ; -- η