Equality-in-equality-out category theory in cubical Agda

category-theory-eq-in-eq-out.md

Equality-in-equality-out category theory in cubical Agda

Now that equality has become computationally relevant but composition of equality remains cumbersome, the statement of various equality laws in the cubical library feels "wrong". Here I want to explore an alternative approach.

What I'm not proposing

To avoid confusion, I want to start by emphasizing what I'm not proposing.

We could aim for the following principle:

Every index/parameter to a non-identity type in an operation's signature, should be a unique variable.

Two parts are crucial here: unique and variable. Both combined ensure that the type of any operation's argument, as well as its output type, is fully unconstrained, and all constraints are expressed by additional equality arguments. For example the types for identity and diagrammatic composition would no longer be:

id : Hom[ x , x ]
seq : Hom[ x , y ] → Hom[ y , z ] → Hom[ x , z ]

but should become

id : x' ≡ x → Hom[ x' , x ]
seq : x' ≡ x → y' ≡ y → z' ≡ z → Hom[ x , y' ] → Hom[ y , z' ] → Hom[ x' , z ]

We could relax our principle a bit by allowing inputs to constrain the output or vice versa, and get

id : x' ≡ x → Hom[ x' , x ]
seq : y' ≡ y → Hom[ x , y' ] → Hom[ y , z ] → Hom[ x , z ]

Still, I expect this to be very annoying in practice: when implementing composition of morphisms, we get to deal with an equality which has computational content that may not be the reflexive path. This feels like a complication, more than a simplification.

What I am proposing

What I am proposing is to finetune operations -- primarily equality laws but also the action of natural transformations -- so as to simplify the implementation of identity and composition.

Functor laws

Let's start by having a look at the functor laws for a functor F : Functor C D:

F-id F : F ⟪ id C ⟫ ≡ id D
F-seq F : F ⟪ φ ⋆⟨ C ⟩ χ ⟫ ≡ F ⟪ φ ⟫ ⋆⟨ D ⟩ F ⟪ χ ⟫

These are implemented by refl for the identity functor, but for composition we need two steps:

G ⟪ F ⟪ id C ⟫ ⟫
  ≡⟨ cong (G ⟪_⟫) (F-id F) ⟩
G ⟪ id D ⟫
  ≡⟨ F-id G ⟩
id E

G ⟪ F ⟪ φ ⋆⟨ C ⟩ χ ⟫ ⟫
  ≡⟨ cong (G ⟪_⟫) (F-seq F) ⟩
G ⟪ F ⟪ φ ⟫ ⋆⟨ D ⟩ F ⟪ χ ⟫ ⟫
  ≡⟨ F-seq G ⟩
G ⟪ F ⟪ φ ⟫ ⟫ ⋆⟨ E ⟩ G ⟪ F ⟪ χ ⟫ ⟫

Since paths in cubical Agda have computational content, taking two steps has a computational meaning: we are composing isomorphisms in the Hom-set. Of course, according to the definition of a Category in the Cubical library, the Hom-set is required to be an hSet, but that just means that there is no problem up to a path. Definitionally, this composition may not yield the most favorable path. Indeed, in cubical Agda, composition does not reduce on reflexive paths, so there is a real risk of annoyance here.

We can instead reformulate the functor laws as follows:

F-id' F : φ ≡ id C → F ⟪ φ ⟫ ≡ id D
F-seq' F : ψ ≡ φ ⋆⟨ C ⟩ χ → F ⟪ ψ ⟫ ≡ F ⟪ φ ⟫ ⋆⟨ D ⟩ F ⟪ χ ⟫

This way, we can implement

F-id' Id = idfun _
F-id' (G ∘F F) = F-id G ∘ F-id F
F-seq' Id = idfun _
F-seq' (G ∘F F) = F-seq' G ∘ F-seq' F

Category laws

The unit and associativity laws of a category express functoriality of Hom[ x ,_] and Hom[_, y ]. Let us instantiate the above functor laws for these functors. Then we get:

⋆IdR' : φ ≡ id → (λ θ → θ ⋆ φ) ≡ (λ θ → θ)
⋆AssocR' : ψ ≡ φ ⋆ χ → (λ θ → θ ⋆ ψ) ≡ (λ θ → (θ ⋆ φ) ⋆ χ)
⋆IdL' : φ ≡ id → (λ θ → φ ⋆ θ) ≡ (λ θ → θ)
⋆AssocL' : ψ ≡ φ ⋆ χ → (λ θ → ψ ⋆ θ) ≡ (λ θ → φ ⋆ (χ ⋆ θ))

Of course ⋆AssocL' and ⋆AssocR' are logically equivalent propositions, and these laws are logically equivalent to the usual category laws. We could either settle for having four laws with some redundancy (which may be practical for computational purposes) or we could opt for an associativity law from which both ⋆AssocL' and ⋆AssocR' are easily provable:

⋆Assoc' : σ ≡ φ ⋆ χ → τ ≡ χ ⋆ ψ → σ ⋆ ψ ≡ φ ⋆ τ

However,

• ⋆Assoc' is provable from either ⋆AssocL' or ⋆AssocR' by composition with the unused path argument, and
• proving ⋆Assoc' in a specific category will probably very often involve a composition anyway,

so it seems best to keep ⋆AssocL' and ⋆AssocR' as the category laws and ⋆Assoc' as a general theorem.

Natural transformations

Current status

A natural transformation ν : NatTrans F G between functors F G : Functor C D consist of an operation and a law:

N-ob ν : (c : ob C) → D [ F ⟅ c ⟆ , G ⟅ c ⟆ ]
N-hom ν : (φ : C [ c , c' ]) → F ⟪ φ ⟫ ⋆ N-ob ν c' ≡ N-ob ν c ⋆ G ⟪ φ ⟫

Natural transformations can be composed in two dimensions, which we will denote:

_⋆N_ : NatTrans F G → NatTrans G H → NatTrans F H
_∘FN_ : NatTrans F2 G2 → NatTrans F1 G1 → NatTrans (F2 ∘F F1) (G2 ∘F G1)

The usage of ⋆ and ∘ is inverse to what is usually done because here they stand for diagrammatic vs. reverse order.

When we consider the interaction of the composition operations with N-ob, we find that _⋆N_ is unproblematic:

N-ob (μ ⋆N ν) c = N-ob μ c ⋆⟨ D ⟩ N-ob ν c

but the composition ν2 ∘FN ν1 is already annoying because the output of N-ob ν1 c is a morphism which cannot be fed to N-ob ν2. Instead, we need to feed N-ob ν2 either the object F1 ⟅ c ⟆ or G1 ⟅ c ⟆ (we have to invoke N-hom ν2 to see that it doesn't matter which one, so our definition will be computationally asymmetric) and then compose the resulting morphisms in a dimension perpendicular to the dimension of composition of ν1 and ν2.

Considering N-hom, we can prove both N-hom (μ ⋆N ν) and N-hom (ν2 ∘FN ν1) with one composition of commuting diagrams, but the latter of course follows the asymmetric and perpendicular pattern of N-ob (ν2 ∘FN ν1).

Alternative approach

I propose instead to view natural transformations ν : NatTrans F G as profunctor morphisms from C [ _ , _ ] to D [ F ⟅ _ ⟆ , G ⟅ _ ⟆ ]. (I am fully aware that a profunctor morphism is a special case of a natural transformation and that I am, as such, relying on the concept that I am rejecting. However, the problem with the current formulation of natural transformations is that it complicates _∘FN_, which is not an interesting operation for profunctor morphisms.) A natural transformation would then have the following operations and laws:

N-hom' ν : C [ x , y ] → D [ F ⟅ x ⟆ , G ⟅ y ⟆ ]
N-natL' ν : ψ ≡ φ ⋆⟨ C ⟩ χ → N-hom' ν ψ ≡ F ⟪ φ ⟫ ⋆⟨ D ⟩ N-hom' ν χ
N-natR' ν : ψ ≡ φ ⋆⟨ C ⟩ χ → N-hom' ν ψ ≡ N-hom' ν φ ⋆⟨ D ⟩ G ⟪ χ ⟫

A first thing to remark is that N-ob can be reimplemented by applying N-hom' to the identity. Subsequently, N-hom can be reproved by composing both naturality laws.

Now implementing _∘FN_ is a piece of cake:

N-hom'  (ν2 ∘FN ν1) = N-hom'  ν2 ∘ N-hom'  ν1
N-natL' (ν2 ∘FN ν1) = N-natL' ν2 ∘ N-natL' ν1
N-natR' (ν2 ∘FN ν1) = N-natR' ν2 ∘ N-hom'N-natR' ν1

When implementing N-hom' (μ ⋆N ν), we are given ψ : C [ x , z ] and we need to feed each transformation a morphism. These should have types φ : C [ x , y ] and χ : C [ y , z ] (for arbitrary y) so that the results N-hom' μ φ : D [ F ⟅ x ⟆ , G ⟅ y ⟆ ] and N-hom' ν χ : D [ G ⟅ y ⟆ , H ⟅ z ⟆ ] can be composed to the desired N-hom' (μ ⋆N ν) ψ : D [ F ⟅ x ⟆ , H ⟅ z ⟆ ]. In order to shed more light on this remarkable situation, we shall briefly consider profunctor morphisms in general, although that section can be mostly ignored.

Profunctor morphisms

A profunctor is of course a special case of a functor (either from the product category or, after currying, to the presheaf category) but I prefer to define it directly as a bifunctor.

A profunctor ℙ : Profunctor A B consists of:

ℙ [_,_] : ob A → ob B → hSet
_⦉_ : A [ a1 , a2 ] → ℙ [ a2 , b ] → ℙ [ a1 , b ]
_⦊_ : ℙ [ a , b1 ] → B [ b1 , b2 ] → ℙ [ a , b2 ]
id-⦉ : α ≡ id A → (λ π → α ⦉ π) ≡ (λ π → π)
⦊-id : β ≡ id B → (λ π → π ⦊ β) ≡ (λ π → π)
seq-⦉ : ψ ≡ φ ⋆⟨ A ⟩ χ → (λ π → ψ ⦉ π) ≡ (λ π → φ ⦉ (χ ⦉ π))
seq-⦊ : ψ ≡ φ ⋆⟨ B ⟩ χ → (λ π → π ⦊ ψ) ≡ (λ π → (π ⦊ φ) ⦊ χ)
⦉-⦊ : απ ≡ α ⦉ π → πβ ≡ π ⦊ β → απ ⦊ β ≡ α ⦉ πβ

For the Hom-profunctor, these are implemented by _⋆_, _⋆_, ⋆IdL', ⋆IdR', ⋆AssocL', ⋆AssocR' and ⋆Assoc' respectively. (Of course similar to ⋆Assoc', the law ⦉-⦊ which takes two equalities could be split up in two laws assuming that either equality is refl.)

Similar to a reformulated natural transformation, a profunctor morphism ν : ProfHom ℙ ℚ consists of:

PH-hom' ν : ℙ [ a , b ] → ℚ [ a , b ]
PH-natL' ν : απ ≡ α ⦉⟨ ℙ ⟩ π → PH-hom' ν απ ≡ α ⦉⟨ ℚ ⟩ PH-hom' ν π
PH-natR' ν : πβ ≡ π ⦊⟨ ℙ ⟩ β → PH-hom' ν πβ ≡ PH-hom' ν π ⦊⟨ ℚ ⟩ β

Profunctor morphisms can be composed in two ways:

_⊗PH_ : ∀ {ℙ1 ℚ1 : Profunctor A B} {ℙ2 ℚ2 : Profunctor B C}
  → ProfHom ℙ1 ℚ1 → ProfHom ℙ2 ℚ2 → ProfHom (ℙ1 ⊗ ℙ2) (ℚ1 ⊗ ℚ2)
  -- Corresponds to _⋆N_
_∘PH_ : ∀ {ℙ ℚ ℝ : Profunctor A B}
  → ProfHom ℚ ℝ → ProfHom ℙ ℚ → ProfHom ℙ ℝ
  -- Corresponds to _∘FN_

The second composition is implemented straightforwardly:

PH-hom'  (ν2 ∘PH ν1) = PH-hom'  ν2 ∘ PH-hom'  ν1
PH-natL' (ν2 ∘PH ν1) = PH-natL' ν2 ∘ PH-natL' ν1
PH-natR' (ν2 ∘PH ν1) = PH-natR' ν2 ∘ PH-natR' ν1

In order to make sense of the first composition, we first need to look at composition of profunctors. The underlying set is given by a coend:

-- pseudosyntax:
(ℙ1 ⊗ ℙ2) [ a , c ] = Coend[ b ∈ B ] (ℙ1 [ a , b ]) × (ℙ2 [ b , c ])

Below, 𝕋 is a profunctor 𝕋 : Profunctor C C or analogous. Note that (ℙ1 [ a , b ]) × (ℙ2 [ b , c ]) can be seen as a profunctor in b.

--pseudosyntax:
data Coend[ c ∈ C ] 𝕋 [ c , c ] : hSet where
  coend : {x : ob C} → 𝕋 [ x , x ] → Coend[ c ∈ C ] 𝕋 [ c , c ]
  extranat : (φ : C [ x , y ]) → (τ : 𝕋 [ y , x ]) → φτ ≡ φ ⦉ τ → τφ ≡ τ ⦊ φ → coend {x} φτ ≡ coend {y} τφ

So (ℙ1 ⊗ ℙ2) [ a , c ] contains pairs of elements of ℙ1 and ℙ2 whose middle point matches up, and we identify pairs that are related by moving the middle point along a morphism in B, making the pairing operation extranatural.

Although the required construction of the coend is quite complex, once defined it seems very straightforward to implement _⊗PH_.

Back to natural transformations

When trying to define μ ⋆N ν, we are dealing with profunctor morphisms from C [ _ , _ ] to D [ F ⟅ _ ⟆ , G ⟅ _ ⟆ ] and D [ G ⟅ _ ⟆ , H ⟅ _ ⟆ ] respectively. These can be easily composed using _⊗PH_ to a profunctor morphism from C [ _ , _ ] ⊗ C [ _ , _ ] to D [ F ⟅ _ ⟆ , G ⟅ _ ⟆ ] ⊗ [ G ⟅ _ ⟆ , H ⟅ _ ⟆ ]. From the latter, we can simply map to D [ F ⟅ _ ⟆ , H ⟅ _ ⟆ ] by composing, which is indeed extranatural. Conversely, we need to map from C [ _ , _ ] to C [ _ , _ ] ⊗ C [ _ , _ ], which can be done in two equal but computationally different ways:

• we can use id C on the left
• we can use id C on the right
• had we defined the coend differently, then we could use id C on both sides and let the given morphism linger in the middle.

The above observations lead to two implementations of _⋆N_:

• We can do

  N-hom' (μ ⋆N ν) φ = N-hom' μ (id C) ⋆⟨ D ⟩ N-hom' ν φ

  Then
  • N-natR' (μ ⋆N ν) follows directly from ⋆AssocR' applied to N-natR' ν
  • N-natL' (μ ⋆N ν) is proven by composing diagrams obtained by applying ⋆Assoc' to N-natL' μ and N-natR' μ and applying ⋆AssocL' to N-natL' ν.
• We can do

  N-hom' (μ ⋆N ν) φ = N-hom' μ φ ⋆⟨ D ⟩ N-hom' ν (id C)

  Then the laws are proven dually.

"So now _∘FN_ is simplified but _⋆N_ has become a total mess."

Well, yes and no. Yes: clearly. But no: if we reimplement the original fields N-ob and N-hom in terms of the new fields as described above, then the resulting implementation of _⋆N_ is exactly what it used to be (perhaps up to associativity for path composition).