Mercurial > hg > Members > kono > Proof > category

comparison S.agda @ 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 7194ba55df56
children 749df4959d19
comparison
equal deleted inserted replaced
662:e1d54c0f73a7 663:855e497a9c8f
12 module S where 12 module S where
13 13
14 open import Relation.Binary.Core 14 open import Relation.Binary.Core
15 open import Function 15 open import Function
16 import Relation.Binary.PropositionalEquality 16 import Relation.Binary.PropositionalEquality
17 open import Relation.Binary.HeterogeneousEquality using (_≅_;refl)
17 18
18 record snat { c₂ } { I OC : Set c₂ } ( sobj : OC → Set c₂ ) 19 record snat { c₂ } { I OC : Set c₂ } ( sobj : OC → Set c₂ )
19 ( smap : { i j : OC } → (f : I ) → sobj i → sobj j ) : Set c₂ where 20 ( smap : { i j : OC } → (f : I ) → sobj i → sobj j ) : Set c₂ where
20 field 21 field
21 snmap : ( i : OC ) → sobj i 22 snmap : ( i : OC ) → sobj i
23 smap0 : { i j : OC } → (f : I ) → sobj i → sobj j 24 smap0 : { i j : OC } → (f : I ) → sobj i → sobj j
24 smap0 {i} {j} f x = smap f x 25 smap0 {i} {j} f x = smap f x
25 26
26 open snat 27 open snat
27 28
28 snat-cong : { c : Level } { I OC : Set c } { SObj : OC → Set c } { SMap : { i j : OC } → (f : I )→ SObj i → SObj j } 29 snat-cong' : { c : Level } { I OC : Set c } { SObj : OC → Set c } { SMap : { i j : OC } → (f : I )→ SObj i → SObj j }
29 ( s t : snat SObj SMap ) 30 ( s t : snat SObj SMap )
30 → ( ( λ i → snmap s i ) ≡ ( λ i → snmap t i ) ) 31 → ( ( λ i → snmap s i ) ≡ ( λ i → snmap t i ) )
31 → ( ( λ i j f → smap0 s f ( snmap s i ) ≡ snmap s j ) ≡ ( ( λ i j f → smap0 t f ( snmap t i ) ≡ snmap t j ) ) ) 32 → ( ( λ i j f → smap0 s f ( snmap s i ) ≡ snmap s j ) ≡ ( ( λ i j f → smap0 t f ( snmap t i ) ≡ snmap t j ) ) )
32 → s ≡ t 33 → s ≡ t
33 snat-cong s t refl refl = {!!} 34 snat-cong' s t refl refl = {!!}
35
36 snat-cong : {c : Level}
37 {I OC : Set c}
38 {sobj : OC → Set c}
39 {smap : {i j : OC} → (f : I) → sobj i → sobj j}
40 → (s t : snat sobj smap)
41 → (snmap-≡ : snmap s ≡ snmap t)
42 → (sncommute-≅ : sncommute s ≅ sncommute t)
43 → s ≡ t
44 snat-cong _ _ refl refl = refl
34 45
35 --This is quite simlar to the answer of 46 --This is quite simlar to the answer of
36 -- 47 --
37 -- Equality on dependent record types 48 -- Equality on dependent record types
38 -- https://stackoverflow.com/questions/37488098/equality-on-dependent-record-types 49 -- https://stackoverflow.com/questions/37488098/equality-on-dependent-record-types