agda - 是否可以在没有函数外延性的情况下证明 Agda 中范畴范畴(以仿函数作为态射)的存在性？

Question

我正在像这样对类别和仿函数建模(导入来自标准库):

module Categories where

open import Level
open import Relation.Binary.PropositionalEquality

record Category a b  : Set (suc (a ⊔ b)) where
  field
    Obj : Set a
    _⇒_ : Obj → Obj → Set b
    _∘_ : {A B C : Obj} → B ⇒ C → A ⇒ B → A ⇒ C
    id : {A : Obj} → A ⇒ A

    left-id : ∀ {A B : Obj} (f : A ⇒ B) → id ∘ f ≡ f
    right-id : ∀ {A B : Obj} (f : A ⇒ B) → f ∘ id ≡ f
    assoc : ∀ {A B C D : Obj} (f : C ⇒ D) (g : B ⇒ C) (h : A ⇒ B) → (f ∘ g) ∘ h ≡ f ∘ (g ∘ h)

infix 10 _[_⇒_] _[_∘_]
_[_⇒_] : ∀ {a b} (C : Category a b) (X : Category.Obj C) (Y : Category.Obj C) → Set b
_[_⇒_] = Category._⇒_

_[_∘_] : ∀ {a b} (C : Category a b) → ∀ {X Y Z} (f : C [ Y ⇒ Z ]) (g : C [ X ⇒ Y ]) → C [ X ⇒ Z ]
_[_∘_] = Category._∘_

record Functor {a b c d} (C : Category a b) (D : Category c d) : Set (a ⊔ b ⊔ c ⊔ d) where
  private module C = Category C
  private module D = Category D

  field
    F : C.Obj → D.Obj
    fmap′ : ∀ (A B : C.Obj) → C [ A ⇒ B ] → D [ F A ⇒ F B ]

    fmap-id′ : ∀ (A : C.Obj) → fmap′ A _ C.id ≡ D.id
    fmap-∘′ : ∀ (X Y Z : C.Obj) (f : C [ Y ⇒ Z ]) (g : C [ X ⇒ Y ]) → fmap′ _ _ (C [ f ∘ g ]) ≡ D [ fmap′ _ _ f ∘ fmap′ _ _ g ]

  fmap : ∀ {A B : C.Obj} → C [ A ⇒ B ] → D [ F A ⇒ F B ]
  fmap {A}{B} = fmap′ A B

  fmap-id : ∀ {A : C.Obj} → fmap′ A A C.id ≡ D.id
  fmap-id {A} = fmap-id′ A

  fmap-∘ : ∀ {X Y Z : C.Obj} (f : C [ Y ⇒ Z ]) (g : C [ X ⇒ Y ]) → fmap′ _ _ (C [ f ∘ g ]) ≡ D [ fmap′ _ _ f ∘ fmap′ _ _ g ]
  fmap-∘ {X}{Y}{Z} = fmap-∘′ X Y Z

我试图通过像这样实例化它来证明类别类别的存在(其中级别 a 和 b 是模块的整洁参数) :

category : Category (suc (a ⊔ b)) (a ⊔ b)
category = record
  { Obj = Category a b
  ; _⇒_ = Functor
  ; _∘_ = Compose
  ; id = Identity
  ; left-id = {!!}
  ; right-id = {!!}
  ; assoc = {!!}
  }

Compose 和 Identity 的定义如您所料，重要的是，fmap-id 用于仿函数的组合 F 和 G 的证明如下:

  fmap-id : ∀ (A : C.Obj) → fmap A _ C.id ≡ E.id
  fmap-id _ =
    begin
      F.fmap (G.fmap C.id)
    ≡⟨ cong F.fmap G.fmap-id ⟩
      F.fmap D.id
    ≡⟨ F.fmap-id ⟩
      E.id
    ∎

现在，我一直在努力为这个类别证明 left-id。这是我目前所拥有的:

FunctorCongruence : ∀ {C D : Category a b} → Functor C D → Functor C D → Set ((a ⊔ b))
FunctorCongruence F G = F.F ≅ G.F → F.fmap′ ≅ G.fmap′ → F.fmap-id′ ≅ G.fmap-id′ → F.fmap-∘′ ≅ G.fmap-∘′ → F ≅ G
  where
    module F = Functor F
    module G = Functor G

functor-cong : ∀ {C D : Category a b}{F : Functor C D}{G : Functor C D} → FunctorCongruence F G
functor-cong refl refl refl refl = refl

left-id : ∀ {C D : Category a b} (F : Functor C D) → Compose Identity F ≡ F
left-id {C} F = ≅-to-≡ (functor-cong F-≅ fmap-≅ fmap-id-≅ fmap-∘-≅)
  where
    Cmp = Compose Identity F
    module F = Functor F
    module Cmp = Functor Cmp
    module C = Category C

    open HetEq.≅-Reasoning

    F-≅ : Cmp.F ≅ F.F
    F-≅ = refl

    fmap-≅ : Cmp.fmap′ ≅ F.fmap′
    fmap-≅ = refl

    lem : (λ A → trans (cong (λ x → x) (F.fmap-id′ A)) refl) ≅ F.fmap-id′
    lem =
      begin
        (λ A → trans (cong (λ x → x) (F.fmap-id′ A)) refl)
      ≅⟨ ? ⟩
        (λ A → cong (λ x → x) (F.fmap-id′ A))
      ≅⟨ ? ⟩
        (λ A → F.fmap-id′ A)
      ≅⟨ refl ⟩
        F.fmap-id′
      ∎

    fmap-id-≅ : Cmp.fmap-id′ ≅ F.fmap-id′
    fmap-id-≅ = lem

    fmap-∘-≅ : Cmp.fmap-∘′ ≅ F.fmap-∘′
    fmap-∘-≅ = ?

但我担心证明等式 (λ A → trans (cong (λ x → x) (F.fmap-id′ A)) refl) ≅ F.fmap-id′ 似乎需要异构相等的功能扩展性，因为 LHS 隐藏在 λ A 后面。如果我对此是正确的，是否可能有一种不同的方法来定义 fmap-id 来避免这种情况？或者在 Agda 的类型理论中是否有任何证据表明该类别的存在取决于函数的可扩展性？

Answer 1

只需将 A ⇒ B 设为 setoid 而不是 Set。这就是它在 standard categories library 中的完成方式.在 my small development我做了同样的事情，但更换了

record Category α β γ : Set (suc (α ⊔ β ⊔ γ)) where
  field
    Obj    : Set α
    _⇒_    : Obj -> Obj -> Set β
    setoid : ∀ {A B} -> Setoid (A ⇒ B) γ
    ...

与

record Category α β γ : Set (suc (α ⊔ β ⊔ γ)) where
  field
    Obj    : Set α
    _⇒_    : Obj -> Obj -> Set β       
    setoid : ISetoid₂ _⇒_ γ
    ...

在哪里

record IsIEquivalence {ι α β} {I : Set ι} (A : I -> Set α) (_≈_ : ∀ {i} -> A i -> A i -> Set β)
                      : Set (ι ⊔ α ⊔ β) where
  field
    refl  : ∀ {i} {x     : A i} -> x ≈ x
    sym   : ∀ {i} {x y   : A i} -> x ≈ y -> y ≈ x
    trans : ∀ {i} {x y z : A i} -> x ≈ y -> y ≈ z -> x ≈ z

record ISetoid {ι α} {I : Set ι} (A : I -> Set α) β : Set (ι ⊔ α ⊔ suc β) where
  infix 4 _≈_

  field
    _≈_            : ∀ {i} -> A i -> A i -> Set β
    isIEquivalence : IsIEquivalence A _≈_

ISetoid₂ : ∀ {ι₁ ι₂ α} {I₁ : Set ι₁} {I₂ : I₁ -> Set ι₂} (A : ∀ i₁ -> I₂ i₁ -> Set α) β
         -> Set (ι₁ ⊔ ι₂ ⊔ α ⊔ suc β)
ISetoid₂ A = ISetoid (uncurry A)

差别不大，但对我来说看起来稍微好一点。 Here是我在 Functor 上的 setoid 变体。和 Cat类别。

---

我会详细说明一下。如果仿函数将相等的对象映射到相等的对象并将相等的态射映射到相等的态射，则仿函数是相等的。但后者意味着前者，因为如果两个态射相等，则它们的定义域和余域也相等，因此我们从恒等态射得到对象相等:

F₁ (id A) ≈ G₁ (id A)
id (F₀ A) ≈ id (G₀ A)
F₀ A      ≡ G₀ A

在标准类别库和我的仿函数中，如果它们将定义上相等的态射映射到相等的态射，则它们是相等的(我想知道为什么):

F ≈ G = ∀ f -> F₁ f ≈ G₁ f

这里的问题是，要说 f ≈ g，我们需要 f 和 g 是相同对象之间的态射。但是

f : A ⇒ B
F₁ f : F₀ A ⇒ F₀ B
G₁ f : G₀ A ⇒ G₀ B

F₁ f 和 G₁ f 是不同的类型。 The solution是在现有的同质之上构造异质平等

data _∼_ {A B} (f : A ⇒ B) : ∀ {X Y} → (X ⇒ Y) → Set (ℓ ⊔ e) where
  ≡⇒∼ : {g : A ⇒ B} → .(f ≡ g) → f ∼ g

We can deal更系统地从任何索引的 setoid 中生成异构 setoid:

data _≋_ {i} (x : A i) : ∀ {j} -> A j -> Set β where
  hetero : {y : A i} -> x ≈ y -> x ≋ y

(一件好事是使用这个转换 we can 从命题相等性中得到 Agda 的异构相等性。)