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

    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 = {!!}

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