[Agda] HITs without paths

[Nils Anders Danielsson]

Hi,

Now we have Cubical Agda with HITs. When you define a HIT you have to
use path equality for the higher constructors. However, perhaps you want
to use some other kind of equality (the cubical identity type or, for
the time being at the cost of losing canonicity, propositional
equality). In my case I had a development that made use of postulated
HITs and propositional equality, and I wanted to replace the postulated
HITs, but I did not want to switch to path equality.

Let me illustrate how this can be accomplished, using the circle as a
first example. I'm defining the circle in a module that is parametrised
by an arbitrary notion of "equality with J", axiomatised in a certain
way (for details, see the links below). I will construct an interface to
the circle that uses this equality, denoted by _≡_.

Here's a definition of the circle as a HIT:

   data 𝕊¹ : Set where
     base  : 𝕊¹
     loop′ : base P.≡ base

P._≡_ stands for path equality. Any two "equalities with J" are
isomorphic (with the isomorphisms mapping reflexivity to reflexivity),
so we can turn path equality into _≡_:

   loop : base ≡ base
   loop = _↔_.from ≡↔≡ loop′

Let us now construct an eliminator for the circle, matching the
eliminator discussed in the HoTT book. Given a motive P : 𝕊¹ → Set p, a
value b : P base and an equality ℓ : subst P loop b ≡ b the eliminator
"elim" should have type (x : 𝕊¹) → P x, it should map base to b, and the
equality dcong elim loop ≡ ℓ should hold (where dcong has type
(x≡y : x ≡ y) → subst B x≡y (f x) ≡ f y):

   elim : (x : 𝕊¹) → P x
   elim base      = b
   elim (loop′ i) = ?

As can be seen above the base case is easy to handle. What about the
case for loop′? Here we should provide some value in P (loop′ i) that is
definitionally equal to b when i is 0̲ or 1̲:

   elim (loop′ i) = lemma i
     where
     lemma : P.[ (λ i → P (loop′ i)) ] b ≡ b
     lemma = ?

Here I will make use of the following bijection (where all equalities
are path equalities):

   heterogeneous↔homogeneous :
     (P : I → Set p) {p : P 0̲} {q : P 1̲} →
     ([ P ] p ≡ q) ↔ transport P 0̲ p ≡ q

(P.[_]_≡_ is dependent path equality, and I'm using the name transport
for Agda.Primitive.Cubical.primTransp.) This bijection can be used to
prove the following lemma:

   subst≡→[]≡ :
     {eq : x P.≡ y} →
     subst B (_↔_.from ≡↔≡ eq) u ≡ v →
     P.[ (λ i → B (eq i)) ] u ≡ v

This lemma can be used to complete the definition of elim, using the
assumption ℓ : subst P loop b ≡ b:

   elim (loop′ i) = subst≡→[]≡ ℓ i

We should also prove that dcong elim loop ≡ ℓ. This follows from the
following lemma:

   dcong-subst≡→[]≡ :
     {eq₁ : x P.≡ y} {eq₂ : subst B (_↔_.from ≡↔≡ eq₁) (f x) ≡ f y} →
     P.hcong f eq₁ ≡ subst≡→[]≡ eq₂ →
     dcong f (_↔_.from ≡↔≡ eq₁) ≡ eq₂

Here P.hcong has the following type (where all equalities are path
equalities):

   (f : (x : A) → B x) (x≡y : x ≡ y) →
   [ (λ i → B (x≡y i)) ] f x ≡ f y

The equality P.hcong elim base′ ≡ subst≡→[]≡ ℓ holds by definition. Here
is the complete definition of the eliminator:

   module Elim
     (P : 𝕊¹ → Set p)
     (b : P base)
     (ℓ : subst P loop b ≡ b)
     where

     elim : (x : 𝕊¹) → P x
     elim base      = b
     elim (loop′ i) = subst≡→[]≡ ℓ i

     elim-loop : dcong elim loop ≡ ℓ
     elim-loop = dcong-subst≡→[]≡ (refl _)

A non-dependent eliminator can easily be derived from the dependent one:

   module Rec (b : A) (ℓ : b ≡ b) where

     private
       module E = Elim
         (const A)
         b
         (subst (const A) loop b  ≡⟨ subst-const _ ⟩
          b                       ≡⟨ ℓ ⟩∎
          b                       ∎)

     rec : 𝕊¹ → A
     rec = E.elim

     rec-loop : cong rec loop ≡ ℓ
     rec-loop = dcong≡→cong≡ E.elim-loop

Here the lemma dcong≡→cong≡ has the following type:

   {x≡y : x ≡ y} {fx≡fy : f x ≡ f y} →
   dcong f x≡y ≡ trans (subst-const _) fx≡fy →
   cong f x≡y ≡ fx≡fy

However, in this case it may be preferable to define a non-dependent
eliminator directly:

   module Rec (b : A) (ℓ : b ≡ b) where

     rec : 𝕊¹ → A
     rec base      = b
     rec (loop′ i) = _↔_.to ≡↔≡ ℓ i

     rec-loop : cong rec loop ≡ ℓ
     rec-loop = cong-≡↔≡ (refl _)

Here the lemma cong-≡↔≡ has been used:

   {eq₁ : x P.≡ y} {eq₂ : f x ≡ f y} →
   P.cong f eq₁ ≡ _↔_.to ≡↔≡ eq₂ →
   cong f (_↔_.from ≡↔≡ eq₁) ≡ eq₂

Let us now see how a truncated HIT can be handled: the propositional
truncation operator. Here is the underlying HIT:

   data ∥_∥ (A : Set a) : Set a where
     ∣_∣                        : A → ∥ A ∥
     truncation-is-proposition′ : P.Is-proposition ∥ A ∥

The truncation constructor can be turned into a function that uses _≡_
instead of path equality:

   truncation-is-proposition : Is-proposition ∥ A ∥
   truncation-is-proposition =
     _↔_.from (H-level↔H-level 1) truncation-is-proposition′

Here I have used the fact that the H-level predicate for _≡_ is
pointwise isomorphic to the H-level predicate for path equality.

The eliminator can be defined in the following way:

   elim :
     (P : ∥ A ∥ → Set p) →
     (∀ x → Is-proposition (P x)) →
     ((x : A) → P ∣ x ∣) →
     (x : ∥ A ∥) → P x
   elim P P-prop f ∣ x ∣                              = f x
   elim P P-prop f (truncation-is-proposition′ x y i) = lemma i
     where
     lemma : P.[ (λ i → P (truncation-is-proposition′ x y i)) ]
               elim P P-prop f x ≡ elim P P-prop f y
     lemma = P.heterogeneous-irrelevance
               (_↔_.to (H-level↔H-level 1) ∘ P-prop)

The case for the truncation constructor uses the lemma
heterogeneous-irrelevance (all equalities in the type signature are path
equalities):

   heterogeneous-irrelevance :
     {P : A → Set p} →
     (∀ x → Is-proposition (P x)) →
     {x≡y : x ≡ y} {p₁ : P x} {p₂ : P y} →
     [ (λ i → P (x≡y i)) ] p₁ ≡ p₂

This lemma follows directly from the following isomorphism (where again
all equalities are path equalities):

   ∀ (P : I → Set p) i →
   H-level (suc n) (P i) ↔ (∀ x y → H-level n ([ P ] x ≡ y))

Note the similarity to Voevodsky's definition of h-levels. This
isomorphism in turn follows from heterogeneous↔homogeneous.

Set truncation constructors can be handled in a similar way, see the set
quotients that I link to below.

A potential disadvantage of the approach outlined above is that it uses
eliminators rather than pattern matching, and one might lose out on some
of the advantages of the cubical approach. An advantage might be that
one can work with something that one is familiar with, rather than
dimension variables, paths, and so on. Wrapping one's head around
Cubical Agda can take a while. For instance, it was nontrivial for me to
prove heterogeneous↔homogeneous, but I got some useful help from Anders
Mörtberg and Andrea Vezzosi (and once I was done Andrea informed me that
he had proved the result while I was working on it).

The approach above has worked for all HITs that I have tried to apply it
to. Links to some code listings:

* The circle:
   http://www.cse.chalmers.se/~nad/listings/equality/Circle.html
* The propositional truncation operator:
   http://www.cse.chalmers.se/~nad/listings/equality/H-level.Truncation.Propositional.html
* Set quotients:
   http://www.cse.chalmers.se/~nad/listings/equality/Quotient.html
* The interval:
   http://www.cse.chalmers.se/~nad/listings/equality/Interval.html
* Suspensions:
   http://www.cse.chalmers.se/~nad/listings/equality/Suspension.html
* A general truncation operator:
   http://www.cse.chalmers.se/~nad/listings/equality/H-level.Truncation.html

Links in these files lead in one or more steps to the other definitions
mentioned above.

The code above can be found in my "equality" library:

   git clone http://www.cse.chalmers.se/~nad/repos/equality/

Quite a few modules in this library are parametrised by an arbitrary
notion of "equality with J", and can be instantiated with at least
propositional equality, path equality, and the cubical identity type.

Fredrik Nordvall Forsberg recently worked on making Agda ensure that
modules with the K rule turned off do not depend on modules with the K
rule turned on, and I turned off the K rule in a majority of the
standard library's modules. Now it is, at least in some cases,
straightforward to use modules from the equality library and the
standard library in the same development. Here is one example:

   {-# OPTIONS --cubical --safe #-}

   -- Standard library modules.

   open import Data.Product
   open import Relation.Binary.PropositionalEquality using (_≡_)

   -- Equality library modules.

   open import Equality.Propositional hiding (_≡_)
   open import H-level.Truncation.Propositional equality-with-J as T
     using (∥_∥)

   -- Mere existence.

   Exists : (A : Set) → (A → Set) → Set
   Exists A B = ∥ Σ A B ∥

   -- A non-dependent eliminator.

   rec :
     {A C : Set} {B : A → Set} →
     Is-proposition C →
     ((x : A) → B x → C) →
     Exists A B → C
   rec p f = T.rec p (uncurry f)

-- 
/NAD