是否有可能在没有功能扩展性的情况下证明Agda中类别类别(带有仿函数作为态射)的存在？

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

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类型理论中是否存在此类别的证据取决于功能扩展性？

只是做A ? B一个setoid,而不是一个Set.这是在标准类别库中完成的.在我的小开发中,我做了同样的事情,但更换了

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)

差别不是很大,但看起来对我来说更好一些.这是我对setoid的变体Functor.和Cat类别.

我会详细说明一下.如果将相等的对象映射到相等的对象并将等态的态射映射到相等的态射,则函数是相等的.但后者意味着前者,因为如果两个moprhisms相等,那么它们的域和codomains也是相等的,所以我们从对等身份态度的等式中获得对象的相等性:

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是不同类型的.解决方案是在现有同构上构建异构等式

data _?_ {A B} (f : A ? B) : ? {X Y} ? (X ? Y) ? Set (? ? e) where
  ??? : {g : A ? B} ? .(f ? g) ? f ? g

我们可以更系统地处理这个问题,并从任何索引的setoid中生成异构setoid:

data _?_ {i} (x : A i) : ? {j} -> A j -> Set ? where
  hetero : {y : A i} -> x ? y -> x ? y

(一个好处是使用这种转换,我们可以通过命题平等来实现Agda的异构平等.)