два поля записывают соответствие в Agda

Я хотел бы написать лимит в категории наборов, используя Agda. Предполагая локальную малость, функтор — это пара отображения на Set OC и I, как здесь.

 sobj :  OC →  Set  c₂
 smap : { i j :  OC  }  → (f : I ) →  sobj i → sobj j

Конус для функтора — это запись с двумя полями. С помощью записи легко показать коммутативность конуса и свойства Предела, кроме единственности. Уникальность Лимита заключается в совпадении записей с двумя полями.

В следующем коде agda я хочу доказать лемму snat-cong.

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

Это очень похоже на ответ Равенство для зависимых типов записей.

Так что это должно работать что-то вроде

snat-cong s t refl refl = refl

но выдает такую ​​ошибку.

.sncommute i j f != sncommute t i j f of type
.SMap f (snmap t i) ≡ snmap t j

Есть ли помощь?


theorem-proving category-theory agda
person Shinji Kono    schedule 09.06.2017    source источник
comment
Я не уверен, что должен означать ваш третий аргумент snat-cong, можете ли вы уточнить это? Вы имеете в виду (∀ i j f → (smap0 s f (snmap s i) ≡ snmap s j) ≡ (smap0 t f (snmap t i) ≡ snmap t j))?   -  person Cactus    schedule 13.06.2017
comment
То же самое с использованием функциональной экстенсиональности: {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ Икс → ж Икс ≡ λ Икс → г Икс )   -  person Shinji Kono    schedule 19.06.2017

Ответы (1)


arrow_upward
1
arrow_downward

В snat-cong ни один из аргументов не говорит о том, что sncommute s равно sncommute t. Вместо этого вы говорите, что тип sncommute s равен типу sncommute t, но это уже следует из первого равенства.

Самый простой способ заявить о равенстве самих sncommutes — это гетерогенное равенство. Таким образом, snat-cong может выглядеть примерно так:

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

Если вы хотите быть более явным или хотите работать с --without-K, вы можете использовать зависимый тип равенства для 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
person Twan van Laarhoven    schedule 18.08.2017
comment
А, это имеет смысл. Спасибо. - person Shinji Kono; 23.10.2017
comment
Я закончил доказательство как cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/category/file/ - person Shinji Kono; 30.10.2017