### view S.agda @ 790:1e7319868d77

Sets is CCC
author Shinji KONO Fri, 19 Apr 2019 23:42:19 +0900 749df4959d19
line wrap: on
line source
```
--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.
--
--     sobj :  OC →  Set  c₂
--     smap : { i j :  OC  }  → (f : I ) →  sobj i → sobj j
--
--A cone for the functor is a record with two fields. Using the record, commutativity of the cone and the propertiesy of the Limit
--are easity shown, except uniquness. The uniquness of the Limit turned out that congruence of the record with two fields.
--
--In the following agda code, I'd like to prove snat-cong lemma.

open import Level
module S where

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
field
snmap : ( i : OC ) → sobj i
sncommute : ( i j : OC ) → ( f :  I ) →  smap f ( snmap i )  ≡ snmap j
smap0 :  { i j :  OC  }  → (f : I ) →  sobj i → sobj j
smap0 {i} {j} f x =  smap f x

open snat

-- 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

--This is quite simlar to the answer of
--
--    Equality on dependent record types
--    https://stackoverflow.com/questions/37488098/equality-on-dependent-record-types
--
--So it should work something like
--
--    snat-cong s t refl refl = refl
--
--but it gives an error like this.
--
--    .sncommute i j f != sncommute t i j f of type
--    .SMap f (snmap t i) ≡ snmap t j
--
--Is there any help?
```