It would be nice for (1 -> C ᵒᵖ) to be the same as (1 -> C) ᵒᵖ

[JasonGross]

We've actually gone out of our way in agda-categories to make as many of these things hold judgementally. For 1 -> C vs C, that is hopeless, as they are fundamentally different even if equivalent (though there might be odd things when C is not inhabited). Certainly (1 -> C ᵒᵖ) should be the same as (1 -> C) ᵒᵖ, and it something that can be fixed if it's not. For Kan extension, it's possible we've erred, and we'd be glad to see a concrete bug report.

Originally posted by @JacquesCarette in https://github.com/agda/agda/issues/5255#issuecomment-790045655

{-# OPTIONS --without-K --safe #-}
module Categories.test where
open import Level
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; refl)
open import Categories.Functor
open import Categories.Category.Core
open import Categories.Category.Instance.One
open import Categories.Category.Construction.Functors

private
  variable
    o ℓ e o′ ℓ′ e′ : Level

test : ∀ {C : Category o ℓ e} → Category.op (Functors (One {o′} {ℓ′} {e′}) C) ≡ Functors (One {o′} {ℓ′} {e′}) (Category.op C)
test = {refl }0
{- x != x₁ of type Category.Obj C
when checking that the expression refl has type
Category.op (Functors One C) ≡ Functors One (Category.op C) -}

I believe if you make Functor a nested sigma type rather than a record, this equality will go through judgmentally. I'm not 100% sure, though.

[JacquesCarette]

Oh, you're asking for something much stronger than I expected. But it's still an interesting question. I'm investigating now.

[JasonGross]

Great! I'm curious to know the results of your investigation. Btw, the ~equivalent PR for the Coq HoTT/HoTT library is https://github.com/HoTT/HoTT/pull/849 (abandoned because it resulted in a moderate slowdown for a couple files, and also did not buy us anything without judgmental eta for the unit type)

[JacquesCarette]

Are you sure you're asking the right question? The objects aren't the same:

  module _ {C : Category o ℓ e} {o′ ℓ′ e′ : Level} where
    open Category
    open Functor

    X Y : Category _ _ _
    X = Category.op (Functors (One {o′} {ℓ′} {e′}) C)
    Y = Functors (One {o′} {ℓ′} {e′}) (Category.op C)

    -- these are not the same.
    eq₁ : Obj X ≡ Obj Y  -- Functor One C ≡ Functor One (Category.op C)
    eq₁ = {!!}

[JacquesCarette]

There is Functor.op, which would line up better.

[JasonGross]

The objects aren't the same:

That's exactly my point. The objects aren't the same, but they would be if Functor were defined as a nested sigma type:

module Categories.test where
open import Level
open import Data.Product
open import Data.Unit
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; refl)
open import Categories.Functor
open import Categories.Category.Core
open import Categories.Category.Instance.One
open import Categories.Category.Construction.Functors
open import Categories.Category

private
  variable
    o ℓ e o′ ℓ′ e′ : Level

FunctorΣ : (C : Category o ℓ e) → (D : Category o′ ℓ′ e′) → Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′)
FunctorΣ C D = Σ[ F₀ ∈ (C.Obj → D.Obj) ]
               Σ[ F₁ ∈ (∀ {A B} (f : C [ A , B ]) → D [ F₀ A , F₀ B ]) ]

               Σ[ identity     ∈ (∀ {A} → D [ F₁ (C.id {A}) ≈ D.id ]) ]
               Σ[ homomorphism ∈ (∀ {X Y Z} {f : C [ X , Y ]} {g : C [ Y , Z ]} →
                                    D [ F₁ (C [ g ∘ f ]) ≈ D [ F₁ g ∘ F₁ f ] ]) ]
               Σ[ F-resp-≈     ∈ (∀ {A B} {f g : C [ A , B ]} → C [ f ≈ g ] → D [ F₁ f ≈ F₁ g ]) ]
               ⊤ where
  private module C = Category C
  private module D = Category D

module _ {C : Category o ℓ e} {o′ ℓ′ e′ : Level} where
  open Category
  open Functor

  X Y : Category _ _ _
  X = Category.op (Functors (One {o′} {ℓ′} {e′}) C)
  Y = Functors (One {o′} {ℓ′} {e′}) (Category.op C)

  -- these are not the same.
  eq₁ : Obj X ≡ Obj Y  -- Functor One C ≡ Functor One (Category.op C)
  eq₁ = { }0

  -- but these are.
  eq₂ : FunctorΣ (One {o′} {ℓ′} {e′}) C ≡ FunctorΣ (One {o′} {ℓ′} {e′}) (Category.op C)
  eq₂ = refl

The intuition is that a functor from the terminal category to C is just an object in C, so it shouldn't matter which direction the arrows go. With enough judgmental rules, this property can hold judgmentally.

[JasonGross]

I think, btw, that NaturalTransformation will also have to be a sigma type / structural record in order for the functor categories to be judgmentally equal.

[JacquesCarette]

Thanks, that helps a lot. I'll fiddle some more.

[sstucki]

Sorry, but I feel like I must be missing something really basic here. Why does it matter whether Functor is defined as a record or as a sigma type? The later is defined as a record too, so what is the essential difference? Is it that records somehow keep tight control over their parameters?

I'm asking because we really don't wanna start encoding everything as sigmas, do we?

[JacquesCarette]

Most definitely not! Things are staying as records in this library.

The question is indeed, what makes some records different than others. There are definitely "options" that one can set or not (like eta-equality) that makes them different. I'm hoping that sigma types aren't baked in so deeply that that is what makes a difference. Thus the need for more experimentation.

[sstucki]

OK, I had to do a few experiments to understand what's going on.

As I suspected, the issue is record parameters. Apparently record signatures are injective w.r.t. to parameters in the sense that the type SomeRecord a differs from SomeRecord b irrespective of whether a and b are actually relevant to the record definition.

That wasn't obvious to me, though maybe it should have been (we use this trick in the library to avoid unification errors, e.g. in the definition of equality on isomorphisms).

Those who, like me, don't find this obvious, may find the following example helpful.

open import Relation.Binary.PropositionalEquality

data Bool : Set where false true : Bool
record ⊤ : Set where

record Silly₁ (b : Bool) : Set where

Silly₂ : (b : Bool) → Set
Silly₂ b = ⊤

_ : Silly₁ true ≡ Silly₁ false
_ = {!refl!}  -- nope, remembering the different values of `b'

_ : Silly₂ true ≡ Silly₂ false
_ = refl      -- yep, no problem, the Booleans are computed away

Clearly the two definitions of Silly are isomorphic. In either case, the type parameter is totally irrelevant. But the parameter of Silly₂ is reduced away, while that of Silly₁ isn't. And that means we can't prove the first equation.

Translated to @JasonGross's Functor example this means that the Functor record in the library remembers exactly which categories it relates (including the direction of the arrows) whereas FunctorΣ doesn't, it just remembers the content of the actual fields/coordinates that make up it's definition (the categories and their signatures are computed away).

I have no idea what this means for the design of the library. It seems useful that records "remember" their parameters for unification to work as expected, but clearly it breaks some useful identities. 🤷

[JasonGross]

I have no idea what this means for the design of the library. It seems useful that records "remember" their parameters for unification to work as expected, but clearly it breaks some useful identities. 🤷

I suspect the ideal design decision here is to have all of the constructions be records that don't remember their parameters (structural records), have thin wrappers for all of them in records that do remember their parameters (nominal records) for type inference, and then use the nominal records in all locations where the type signature reduces away (e.g., in arguments to definitions) but use the structural records in places where they one reduce away (in arguments to constructors and in the type signatures of other fields / non-wrapper-records).

So, e.g., the op construction for functors would take a nominal functor, but the construction of functor categories would use structural functors as the objects.

I'm not sure if there's a way to make this work in a syntactically nice way; Coq has coercions that could be used here, does Agda have something similar?

[JacquesCarette]

I think we could create some "forget" functions that go from nominal to structural for when we want to explicitly do that. I think we generally want to keep things as nominal as possible. Generally, CT seems to work quite well that way, so I wouldn't want to be "less typed".

Experimenting with functor categories to have them use structural functors as the objects is worth trying out (I will, when I have a window of time).

Agda does not have coercions. But it does make it easy to have multiple records with shared fields and build them easily. So I think that syntactically, it won't look much different.

[JasonGross]

But it does make it easy to have multiple records with shared fields and build them easily

How does this work? / Are there examples?

[TOTBWF]

The ones that come to mind are NTHelper and NIHelper.

I've been thinking about this whole bundling situation for a while now, and I think I have a generic solution. Perhaps something like:

record Bundled₂ {a b p} {A : Set a} {B : Set b} (P : A → B → Set p) : Set (a ⊔ b ⊔ p) where
  field
    elem₁   : A
    elem₂   : B
    bundled : P elem₁ elem₂

StructuralFunctor : (o ℓ e o′ ℓ′ e′ : Level) → Set (suc o ⊔ suc ℓ ⊔ suc e ⊔ suc o′ ⊔ suc ℓ′ ⊔ suc e′)
StructuralFunctor o ℓ e o′ ℓ′ e′ = Bundled₂ (Functor {o} {ℓ} {e} {o′} {ℓ′} {e′})

could work?

[JasonGross]

I think you have it backwards; structural functors should be able to be the same even when the categories don't line up.

[HuStmpHrrr]

I am aware of iterated sigma types used in unimath but what it buys doesn't seem to pay off what it loses. Agda in some sense is optimized for records. also I find that the definitional equality with iterated sigmas is somewhat accidental. surely it would be very desirable if we have this. that definitely requires changes to the language itself.