|
608
|
1 --I'd like to write the Limit in Sets Category using Agda. Assuming local smallness, a functor is a pair of map on Set OC and I, like this.
|
|
|
2 --
|
|
|
3 -- sobj : OC → Set c₂
|
|
|
4 -- smap : { i j : OC } → (f : I ) → sobj i → sobj j
|
|
|
5 --
|
|
|
6 --A cone for the functor is a record with two fields. Using the record, commutativity of the cone and the propertiesy of the Limit
|
|
|
7 --are easity shown, except uniquness. The uniquness of the Limit turned out that congruence of the record with two fields.
|
|
|
8 --
|
|
|
9 --In the following agda code, I'd like to prove snat-cong lemma.
|
|
|
10
|
|
|
11 open import Level
|
|
|
12 module S where
|
|
|
13
|
|
|
14 open import Relation.Binary.Core
|
|
|
15 open import Function
|
|
|
16 import Relation.Binary.PropositionalEquality
|
|
|
17
|
|
|
18 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 field
|
|
|
21 snmap : ( i : OC ) → sobj i
|
|
|
22 sncommute : ( i j : OC ) → ( f : I ) → smap f ( snmap i ) ≡ snmap j
|
|
|
23 smap0 : { i j : OC } → (f : I ) → sobj i → sobj j
|
|
|
24 smap0 {i} {j} f x = smap f x
|
|
|
25
|
|
|
26 open snat
|
|
|
27
|
|
|
28 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 → ( ( λ 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 → s ≡ t
|
|
|
33 snat-cong s t refl refl = {!!}
|
|
|
34
|
|
|
35 --This is quite simlar to the answer of
|
|
|
36 --
|
|
|
37 -- Equality on dependent record types
|
|
|
38 -- https://stackoverflow.com/questions/37488098/equality-on-dependent-record-types
|
|
|
39 --
|
|
|
40 --So it should work something like
|
|
|
41 --
|
|
|
42 -- snat-cong s t refl refl = refl
|
|
|
43 --
|
|
|
44 --but it gives an error like this.
|
|
|
45 --
|
|
|
46 -- .sncommute i j f != sncommute t i j f of type
|
|
|
47 -- .SMap f (snmap t i) ≡ snmap t j
|
|
|
48 --
|
|
|
49 --Is there any help?
|
