Mercurial > hg > Members > kono > Proof > category

changeset 822:4c0580d9dda4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
from cart to graph, hom equality to set equality
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 01 May 2019 21:16:58 +0900
parents fbbc9c03bfed
children f57c9603d989
files CCCGraph.agda negnat.agda
diffstat 2 files changed, 56 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Wed May 01 15:16:54 2019 +0900
+++ b/CCCGraph.agda	Wed May 01 21:16:58 2019 +0900
@@ -335,14 +335,46 @@
 fmap : {c₁ c₂ ℓ : Level} → {a b : Obj (Cart {c₁} {c₂} {ℓ} ) } → Hom (Cart {c₁} {c₂} {ℓ} ) a b → Hom (Grp {c₁} {c₂}) ( fobj a ) ( fobj b )
 fmap f =  record { vmap = FObj (cmap f) ; emap = FMap (cmap f) }
 
+≃-cong : {c₁ c₂ ℓ : Level}  (B : Category c₁ c₂ ℓ ) → {a b a' b' : Obj B }
+      → { f f'   : Hom B a b }
+      → { g g' : Hom B a' b' }
+      → [_]_~_ B f g → B [ f ≈ f' ] → B [ g ≈ g' ] → [_]_~_ B f' g'
+≃-cong B {a} {b} {a'} {b'} {f} {f'} {g} {g'}  (refl {g2} eqv) f=f' g=g' = let open ≈-Reasoning B in refl {_} {_} {_} {B} {a'} {b'} {f'} {g'} ( begin
+             f'
+          ≈↑⟨ f=f' ⟩
+             f
+          ≈⟨ eqv  ⟩
+             g
+          ≈⟨ g=g' ⟩
+             g'
+          ∎  )
+  
+
 UX : {c₁ c₂ ℓ : Level} → Functor (Cart {c₁} {c₂} {ℓ} ) (Grp {c₁} {c₂})
 FObj (UX {c₁} {c₂} {ℓ}) a = fobj a
 FMap UX f =  fmap f
 isFunctor (UX {c₁} {c₂} {ℓ}) = isf where
+  open import HomReasoning
+  lemma0 : {A B : Category c₁ c₂ ℓ } { f g : Functor A B } → {a b : Obj B} → [_]_~_ B  (id1 B a) (id1 B b) → a ≡ b 
+  lemma0 {A} {B} {f} {g} (refl eqv) = refl
+  lemma03 : {A B : Category c₁ c₂ ℓ } { f g : Functor A B } → {a : Obj A} → [_]_~_ B  (FMap f ( id1 A a)) (FMap g ( id1 A a)) → FObj f a ≡ FObj g a 
+  lemma03 {A} {B} {f} {g} eq = lemma0 {A} {B} {f} {g} ( ≃-cong B eq (IsFunctor.identity (Functor.isFunctor (f)))(IsFunctor.identity (Functor.isFunctor (g)))  )
+  lemma01 : {A B : Category c₁ c₂ ℓ } { f g : Functor A B } → {a : Obj A} → f ≃ g  →  FObj f a ≡ FObj g a 
+  lemma01 {A} {B} {f} {g} {a}  eq = lemma03 {A} {B} {f} {g} (eq (id1 A a))
+  lemma1 : {A B : Obj (Cart {c₁} {c₂} {ℓ}) } { f g : Hom (Cart {c₁} {c₂} {ℓ}) A B }
+       → (Cart {c₁} {c₂} {ℓ}) [ f ≈ g ] → vmap (fmap f) ≡ vmap (fmap g)
+  lemma1 {a} {b} {f} {g} eq = extensionality Sets ( λ z → lemma01 {cat a} {cat b} {cmap f} {cmap g} eq  )
+  lemma20 : {A B : Category c₁ c₂ ℓ }  {a b : Obj A} → ( e : Hom A a b ) → ( g : Functor A B )  → ( f : Hom A a b → Hom B (FObj g a) (FObj g b) ) 
+       → B [ f e ≈ FMap g e ] → f e ≅ FMap g e
+  lemma20 e g f eq = {!!}
+  lemma2 : {A B : Obj (Cart {c₁} {c₂} {ℓ}) } { f g : Hom (Cart {c₁} {c₂} {ℓ}) A B} →
+      (Cart {c₁} {c₂} {ℓ}) [ f ≈ g ]  → vmap (fmap f) ≡ vmap (fmap g)  → {a b : vertex (fobj A)} {e : edge (fobj A) a b} → emap (fmap f) e ≅ emap (fmap g) e
+  lemma2 {A} {B} {f} {g} eq refl {a} {b} {e} with ( eq e )
+  ... | refl {h} eqv =  lemma20 e (cmap g) (FMap (cmap f)) eqv
   isf : IsFunctor (Cart {c₁} {c₂} {ℓ} ) (Grp {c₁} {c₂}) fobj fmap
   IsFunctor.identity isf = mrefl refl refl
   IsFunctor.distr isf = mrefl refl refl
-  IsFunctor.≈-cong isf eq = mrefl {!!} {!!}
+  IsFunctor.≈-cong isf {a} {b} {f} {g} eq = mrefl (lemma1 {a} {b} {f} {g} eq ) (lemma2 {a} {b} {f} {g} eq (lemma1 {a} {b} {f} {g} eq ))
 
 ---   
 ---   open ccc-from-graph
--- a/negnat.agda	Wed May 01 15:16:54 2019 +0900
+++ b/negnat.agda	Wed May 01 21:16:58 2019 +0900
@@ -165,6 +165,29 @@
         lemma2 : { n :  ℕ } -> isEven (suc (suc n ))  ≡  isEven n
         lemma2 = refl
 
+data One : Set where
+   * : One
+
+lemma1 :  ( x y : One  ) → x ≡ y
+lemma1 * * = refl
+
+lemma2 :  {A : Set} ( x : A) → x ≡ x
+lemma2 x  = refl
 
 
+open import Data.Empty
+open import Relation.Nullary
+open import Level
 
+lemma4 : Set (Level.suc Level.zero)
+lemma4 =  {A : Set} ( x y : A) → ¬ ( ¬ x ≡ y )
+
+data  A   : Set  where
+   x y z : A
+
+data _==_ : ( a b : A ) → Set where
+   x=y : x == y
+
+lemma3 : ( a b : A ) → a == b → ¬ a ≡ b
+lemma3 _ _ x=y = λ ()
+