Mercurial > hg > Members > kono > Proof > automaton

changeset 265:c47634c830f3

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 Thu, 08 Jul 2021 08:41:05 +0900
parents d1e8e5eadc38
children e5cf49902db3
files automaton-in-agda/src/bijection.agda
diffstat 1 files changed, 13 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/bijection.agda	Wed Jul 07 19:36:59 2021 +0900
+++ b/automaton-in-agda/src/bijection.agda	Thu Jul 08 08:41:05 2021 +0900
@@ -27,11 +27,22 @@
 
 open Bijection 
 
-bij-combination : {n m l : Level} (R : Set n) (S : Set m) (T : Set l)  → Bijection R S → Bijection S T → Bijection R T
-bij-combination R S T rs st = record { fun← = λ x → fun← rs ( fun← st x ) ; fun→ = λ x → fun→ st ( fun→ rs x )
+bi-trans : {n m l : Level} (R : Set n) (S : Set m) (T : Set l)  → Bijection R S → Bijection S T → Bijection R T
+bi-trans R S T rs st = record { fun← = λ x → fun← rs ( fun← st x ) ; fun→ = λ x → fun→ st ( fun→ rs x )
     ; fiso← = λ x →  trans (cong (λ k → fun← rs k) (fiso← st (fun→ rs x))) ( fiso← rs x)
     ; fiso→ = λ x →  trans (cong (λ k → fun→ st k) (fiso→ rs (fun← st x))) ( fiso→ st x) }
 
+bid : {n : Level} (R : Set n)  → Bijection R R
+bid {n} R = record {  fun← = λ x → x ; fun→  = λ x → x ; fiso← = λ _ → refl ;  fiso→ = λ _ → refl } 
+
+bi-sym : {n m : Level} (R : Set n) (S : Set m) → Bijection R S →  Bijection S R
+bi-sym R S eq = record {  fun← =  fun→ eq ; fun→  = fun← eq  ; fiso← =  fiso→ eq ;  fiso→ =  fiso← eq } 
+
+open import Relation.Binary.Structures
+
+bijIsEquivalence : {n : Level } → IsEquivalence  (Bijection {n} {n})
+bijIsEquivalence = record { refl = λ {R} → bid R ; sym = λ {R} {S} → bi-sym R S ; trans = λ {R} {S} {T} → bi-trans R S T }
+
 --  ¬ A = A → ⊥ 
 --
 -- famous diagnostic function