Mercurial > hg > Members > kono > Proof > category

changeset 663:855e497a9c8f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
introducd HeterogeneousEquality https://stackoverflow.com/questions/44456608/two-fields-record-congruence-in-agda
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 22 Oct 2017 22:42:56 +0900
parents e1d54c0f73a7
children 9e8276b89cd0
files S.agda SetsCompleteness.agda freyd2.agda
diffstat 3 files changed, 34 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/S.agda	Sat Aug 12 16:35:58 2017 +0900
+++ b/S.agda	Sun Oct 22 22:42:56 2017 +0900
@@ -14,6 +14,7 @@
     open import Relation.Binary.Core
     open import Function
     import Relation.Binary.PropositionalEquality
+    open import Relation.Binary.HeterogeneousEquality using (_≅_;refl)
 
     record snat   { c₂ }  { I OC :  Set  c₂ } ( sobj :  OC →  Set  c₂ )
          ( smap : { i j :  OC  }  → (f : I ) →  sobj i → sobj j ) : Set  c₂ where
@@ -25,12 +26,22 @@
 
     open snat
 
-    snat-cong :  { c : Level }  { I OC :  Set  c }  { SObj :  OC →  Set  c  } { SMap : { i j :  OC  }  → (f : I )→  SObj i → SObj j }
+    snat-cong' :  { c : Level }  { I OC :  Set  c }  { SObj :  OC →  Set  c  } { SMap : { i j :  OC  }  → (f : I )→  SObj i → SObj j }
              ( s t :  snat SObj SMap   )
          → ( ( λ i  → snmap s i )  ≡  ( λ i →  snmap t i ) )
          → ( ( λ i j f →  smap0 s f ( snmap s i )  ≡ snmap s j   ) ≡ (  ( λ  i j f → smap0 t f ( snmap t i )  ≡ snmap t j ) ) )
          → s ≡ t
-    snat-cong s t refl refl = {!!}
+    snat-cong' s t refl refl = {!!}
+
+    snat-cong : {c : Level}
+                {I OC : Set c}
+                {sobj : OC → Set c}
+                {smap : {i j : OC}  → (f : I) → sobj i → sobj j}
+              → (s t : snat sobj smap)
+              → (snmap-≡ : snmap s ≡ snmap t)
+              → (sncommute-≅ : sncommute s ≅ sncommute t)
+              → s ≡ t
+    snat-cong _ _ refl refl = refl
 
 --This is quite simlar to the answer of 
 --
--- a/SetsCompleteness.agda	Sat Aug 12 16:35:58 2017 +0900
+++ b/SetsCompleteness.agda	Sun Oct 22 22:42:56 2017 +0900
@@ -182,13 +182,17 @@
 ≡cong2 _ refl refl = refl
 
 open import Relation.Binary.HeterogeneousEquality as HE renaming ( cong to cong' ; sym to sym' ; subst₂ to subst₂' ; Extensionality to Extensionality' )
+    using (_≅_;refl)
 
-snat-cong :  { c : Level }  { I OC :  Set  c }  { SObj :  OC →  Set  c  } { SMap : { i j :  OC  }  → (f : I )→  SObj i → SObj j }
-         ( s t :  snat SObj SMap   )
-     → ( ( λ i  → snmap s i )  ≡  ( λ i →  snmap t i ) )
-     → ( ( λ i j f →  smap0 s f ( snmap s i )  ≡ snmap s j   ) ≡ (  ( λ  i j f → smap0 t f ( snmap t i )  ≡ snmap t j ) ) )
-     → s ≡ t
-snat-cong s t refl refl = {!!}
+snat-cong : {c : Level}
+                {I OC : Set c}
+                {sobj : OC → Set c}
+                {smap : {i j : OC}  → (f : I) → sobj i → sobj j}
+              → (s t : snat sobj smap)
+              → (snmap-≡ : snmap s ≡ snmap t)
+              → (sncommute-≅ : sncommute s ≅ sncommute t)
+              → s ≡ t
+snat-cong _ _ refl refl = refl
 
 open import HomReasoning
 open NTrans
@@ -246,15 +250,21 @@
                   limit1 a t x
              ≡⟨⟩
                   record { snmap = λ i →  ( TMap t i ) x ; sncommute = λ i j f → comm2 t f }
-             ≡⟨ snat-cong (limit1 a t x) (f x ) ( extensionality Sets  ( λ  i  →  eq1 x i )) {!!}  ⟩
+             ≡⟨ snat-cong (limit1 a t x) (f x ) ( extensionality Sets  ( λ  i  →  eq1 x i )) (eq2 x ) ⟩
                   record { snmap = λ i →  snmap  (f x ) i  ; sncommute = λ i j f' → sncommute (f x ) i j f'  }
              ≡⟨⟩
                   f x
              ∎  ) where
                   open  import  Relation.Binary.PropositionalEquality
+                  postulate ≅extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → HE.Extensionality c₂ c₂
                   open ≡-Reasoning
                   eq1 : (x : a ) (i : Obj C) → TMap t i x ≡ snmap (f x) i
                   eq1 x i = sym ( ≡cong ( λ f → f x ) cif=t  )
-                  eq2 : ( x : a) → (λ i j f₁ → smap0 (limit1 a t x) f₁ (snmap (limit1 a t x) i) ≡ snmap (limit1 a t x) j)
-                        ≡ (λ i j  f₁ → smap0 (f x) f₁ (snmap (f x) i) ≡ snmap (f x) j)
+                  eq2' : ( x : a) → (λ i j f₁ → smap0 (limit1 a t x) f₁ (snmap (limit1 a t x) i) ≡ snmap (limit1 a t x) j)
+                        ≅ (λ i j  f₁ → smap0 (f x) f₁ (snmap (f x) i) ≡ snmap (f x) j)
+                  eq2' x = {!!}
+                  irr≅ : { c₂ : Level}  {d : Set c₂ }  { x y : d } ( eq eq' :  x  ≡ y ) → eq ≅ eq'
+                  irr≅ refl refl = refl
+                  -- eq2 :  ( x : a) → sncommute (limit1 a t x) ≅ sncommute (f x)
+                  eq2 :  ( x : a) →  ( λ i j f → ≡cong ( λ f → f x ) ( IsNTrans.commute ( isNTrans t )))  ≅ sncommute (f x)
                   eq2 x = {!!}
--- a/freyd2.agda	Sat Aug 12 16:35:58 2017 +0900
+++ b/freyd2.agda	Sun Oct 22 22:42:56 2017 +0900
@@ -368,9 +368,9 @@
 
 module Adjoint-Functor {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete A I )
      (U : Functor A B )
-     ( i :  (b : Obj B) → Obj ( K B A b ↓ U) )
+     (i :  (b : Obj B) → Obj ( K B A b ↓ U) )
      (In :  (b : Obj B) → HasInitialObject ( K B A b ↓ U) (i b) ) 
-     (LP :  LimitPreserve A I B U  ) where
+        where
 
    tmap-η : (y : Obj B)  → Hom B y (FObj U (obj (i y)))
    tmap-η  y = hom (i y)