CODEWITHSUNDEEP
agdacategory-theorytheorem-proving
Shinji Kono
Shinji Kono

Reputation: 31

two fields record congruence in Agda

I'd like to write the Limit in Sets Category using Agda. Assuming local smallness, a functor is a pair of a 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 properties of the Limit are easily shown, except the uniqueness. The uniqueness of the Limit is turned out that a congruence of the records 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 .

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?

Upvotes: 2

Views: 220

Answers (1)

Twan van Laarhoven
Twan van Laarhoven

Reputation: 2602

In snat-cong none of the arguments are saying assuming anything about sncommute s being equal to sncommute t. Instead what you are saying is that the type of sncommute s is equal to the type of sncommute t, but that already follows from the first equality.

The easiest way to state equality of the sncommutes itself is with heterogeneous equality. So snat-cong could look something like this:

open import Relation.Binary.HeterogeneousEquality using (_≅_;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

If you want to be more explicit, or want to work with --without-K, then you could use a dependent equality type for sncommute-≅:

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-≡ : subst (\snmap → ∀ i j f → smap f (snmap i) ≡ snmap j) snmap-≡ (sncommute s) ≡ sncommute t)
           → s ≡ t
snat-cong' _ _ refl refl = refl

Upvotes: 1

Related Questions