EqPtdSigmas.lagda

# Questions about an axiom for equality of pointed sigma types

In the Agda 2.4.2.4 code below I am allowing K-based pattern matching.

## Basics

We need some standard imports and definitions.

\begin{code}
open import Level renaming (zero to Z ; suc to S)
open import Function hiding (_∋_)
open import Data.Empty
open import Data.Nat hiding (_>_ ; _<_ ; _⊔_)
open import Data.Product hiding (<_,_>)
  renaming (proj₁ to fst ; proj₂ to snd ; curry to cu ; uncurry to uc)

record ⊤ {l} : Set l where constructor tt

open import Relation.Binary.PropositionalEquality

infix 4 _Σ≡_
infixl 9 _⊚_

_⊚_ : {§A : _}{A : Set §A}{x y z : A} → x ≡ y → y ≡ z → x ≡ z
_⊚_ = subst (flip _≡_ _) ∘ sym

_Σ≡_ : {§A §B : _}{A : Set §A}{B : A → Set §B} (x y : Σ A B) → Set (§A ⊔ §B)
_Σ≡_ {B = B} x y = Σ (fst x ≡ fst y) λ p → subst B p (snd x) ≡ snd y

≡→Σ≡ : {§A §B : _}{A : Set §A}{B : A → Set §B}{x y : Σ A B} →
       x ≡ y → x Σ≡ y
≡→Σ≡ refl = refl , refl

Σ≡→≡ : {§A §B : _}{A : Set §A}{B : A → Set §B}{x y : Σ A B} →
       x Σ≡ y → x ≡ y
Σ≡→≡ (refl , refl) = refl

module J where

  J : ∀ lA lP → Set _
  J lA lP = {A : Set lA}(P : {x y : A} → x ≡ y → Set lP)
            (m : ∀ x → P (refl {x = x})){x y : A}(p : x ≡ y) → P p

  j : {lA lP : _} → J lA lP
  j P m refl = m _

coe : {l : _}{X Y : Set l} → X ≡ Y → X → Y
coe = subst id

lem⊤ : ∀ {lA}{A : Set lA}(p : ⊤ ≡ A)(x : ⊤)(y : A) → coe p x ≡ y
lem⊤ p = let open J in
         j (λ {A}{B}(p : A ≡ B) → (q : ⊤ ≡ A)(x : A)(y : B) → coe p x ≡ y)
           (λ X p → subst (λ X → (x y : X) → x ≡ y) p λ _ _ → refl)
           p refl

isrip : ∀ {lA}{A : Set lA}(p : A ≡ A){x : A} → coe p x ≡ x -- uip!
isrip refl = refl

txe : {lA lB : _}{A : Set lA}{B : A → Set lB} →
      {f g : (a : A) → B a} → f ≡ g → (∀ x → f x ≡ g x)
txe refl _ = refl

Eq : ∀ {a}(A : Set a) → A → A → Set a
Eq A = _≡_ {A = A}
\end{code}

From now on I will avoid universe polymorphism as much as possible, in
order to enhance readability.

Pointed types are pairs of a type and an inhabitant of that type.

\begin{code}
Ptd = Σ Set id
\end{code}

## Definition: Distributivity of equality of pointed types over sigmas

One could think of making heterogeneous equality of pairs (i.e.,
equality of pointed sigma types) "friendlier" by assuming a property
such as the following:

\begin{code}
DistrEqPtdΣ = {A : Set}{B : A → Set}{C : Set}{D : C → Set}
              {a : A}{b : B a}{c : C}{d : D c} →
                   Eq Ptd (Σ A B , a , b) (Σ C D , c , d)
              ≡ (  Eq Ptd (A     , a    ) (C     , c    )
                 × Eq Ptd (  B a ,     b) (  D c ,     d))
\end{code}

This definition is inspired by the law for equality of pairs in
Observational Type Theory. There are a few differences, though: in OTT
universes are à la Tarski, and the identity type is an "heterogeneous"
(or "curried") relation defined by structural recursion (the law holds
definitionally) in a Prop. Furthermore, also equality of *types*
(`_<->_` in Conor McBride's "Dependently-typed Metaprogramming in
Agda") is defined by structural recursion.

The property `DistrEqPtdΣ`, instead, only concerns "typal" equality of
*pointed* Russell-style types: "Eq Set" is not involved.

I'd like to know whether `DistrEqPtdΣ` is a consistent assumption in
Agda (see the questions section at the end).

Some times ago (~ Nov 2013) I asked myself how `DistrEqPtdΣ` would
relate to other properties (Univalence and Injectivity of Type
Constructors), and whether it would help with dealing with encoding of
dependent records. A cleaned-up version of what I did back then
follows.

## `DistrEqPtdΣ` is inconsistent with Univalence

I don't think this proof requires UIP, unless `DistrEqPtdΣ` implies
UIP (does it?). As I didn't disable K, I won't try to prove this in
Agda. Here is a sketch which I hope to be correct (please let me know
if it isn't).

Under Univalence (Σ ℕ Fin , 1 , zero) ≡ (Σ ℕ Fin , 2 , suc zero) holds
because Σ ℕ Fin is "discrete" (i.e., its equality is decidable), hence
"homogeneous" (see Nicolai Kraus's post at
http://homotopytypetheory.org/2013/10/28/).

However, (Fin 1 , zero) ≡ (Fin 2 , suc zero) is empty because Fin 1 ≡
Fin 2 is easily refutable.

Therefore the LHS of equation in the type of `no` below is inhabited
under Univalence, while the RHS is empty.

\begin{code}
module _ (d : DistrEqPtdΣ) where

  open import Data.Fin

  no :   Eq Ptd (Σ ℕ Fin , 1 , zero) (Σ ℕ Fin , 2 , suc zero)
       ≡ (Eq Ptd (ℕ , 1) (ℕ , 2) × Eq Ptd (Fin 1 , zero) (Fin 2 , suc zero))
  no = d
\end{code}

## Under UIP, `DistrEqPtdΣ` is inconsistent with Injectivity of Type Constructors

It might appear less intuitive that `DistrEqPtdΣ` is also inconsistent
with "Injectivity of Type Constructors" or, more specifically,
injectivity of `Σ`, in this case under UIP.

We can define injectivity of `Σ` as a pair of two properties.

\begin{code}
record InjectiveΣ : Set₁ where
  field
    injΣ₁ : {A : Set}{B : A → Set}{C : Set}{D : C → Set} →
            Σ A B ≡ Σ C D → A ≡ C
    injΣ₂ : {A : Set}{B : A → Set}{C : Set}{D : C → Set}
            (p : Σ A B ≡ Σ C D) → B ≡ D ∘ coe (injΣ₁ p)
\end{code}

While `InjectiveΣ` can be inhabited by
enabling `--injective-type-constructors`, we will just assume the
property.

\begin{code}
module _ (A : Set)(B : A → Set)(C : Set)(D : C → Set)
         (injectiveΣ : InjectiveΣ) where

  open InjectiveΣ injectiveΣ
\end{code}

The idea is that the families `X = const ⊤` and `Y = λ b → if b then ⊤
else ⊥` are different, but `DistrEqPtdΣ` equates `(Σ Bool X , true ,
tt)` and `(Σ Bool Y , true , tt)`.

\begin{code}
  ¬fr : DistrEqPtdΣ → ⊥
  ¬fr d = subst Y h (snd (f false)) where
    open import Data.Bool
    X Y : Bool → Set
    X = const ⊤
    Y = λ b → if b then ⊤ else ⊥
    p1 : (Σ Bool X , true , tt) ≡ (Σ Bool Y , true , tt)
    p1 = coe (sym d) (refl , refl)
    p2 : Σ Bool X ≡ Σ Bool Y
    p2 = fst (≡→Σ≡ p1)
    f : Bool → Σ Bool Y
    f = coe p2 ∘ flip _,_ tt
    w : (p : Σ Bool X ≡ Σ Bool Y) → (fst ∘ coe p ∘ flip _,_ tt) ≡ id
    w p with isrip (injΣ₁ p) {false} | txe (injΣ₂ p) false
    w p | q | r rewrite q with coe r tt
    w p | q | r | ()
    h : fst (coe p2 (false , tt)) ≡ false
    h = txe (w p2) false
\end{code}

## Isomorphisms between encodings of dependently-typed records

### Obs 1: left-nested and right-nested records normalize to "non-dependent" ones

The following snippet proves that left-nested and right-nested
dependently-typed records (Pollack 2002), in the "unlabeled" version
often used by Conor McBride, can be normalised to lists of pointed
types.

\begin{code}
open import Data.List
open import Data.List.All
\end{code}

Lists of pointed types.

\begin{code}
module N where

  Cx = List Set

  ⟦_⟧ : Cx → Set -- aka All id, but Agda's stdlib has a large one
  ⟦     [] ⟧ = ⊤
  ⟦ A ∷ As ⟧ = A × ⟦ As ⟧

  Record = Σ Cx ⟦_⟧ -- ≅ List Ptd, but I'll skip that
\end{code}

Left-nested records.

\begin{code}
module L where

  mutual
    data Cx : Set₁ where
      ε   :                             Cx
      _>_ : (Γ : Cx)(τ : ⟦ Γ ⟧ → Set) → Cx

    ⟦_⟧ : Cx → Set
    ⟦ ε ⟧     = ⊤
    ⟦ Γ > τ ⟧ = Σ ⟦ Γ ⟧ τ

  Record = Σ Cx ⟦_⟧
\end{code}

Right-nested records.

\begin{code}
module R where

  data Cx : Set₁ where
    ε   :                         Cx
    _<_ : (S : Set)(τ : S → Cx) → Cx

  ⟦_⟧ : Cx → Set
  ⟦ ε     ⟧ = ⊤
  ⟦ S < T ⟧ = Σ S λ s → ⟦ T s ⟧

  Record = Σ Cx ⟦_⟧
\end{code}

In `LN` and `RN` we prove that `N.Record` is a retract of both
`L.Record` and `R.Record`.

\begin{code}
module LN where

  to : L.Record → N.Record
  to (L.ε , tt) = [] , tt
  to (Γ L.> τ , ts , t) = let Xs , xs = to (Γ , ts) in τ ts ∷ Xs , t , xs

  fr : N.Record → L.Record
  fr ([] , tt) = L.ε , tt
  fr (X ∷ Xs , x , xs) = let Γ , γ = fr (Xs , xs) in Γ L.> const X , γ , x

  to∘fr≡id : ∀ r → to (fr r) ≡ r
  to∘fr≡id ([] , _) = refl
  to∘fr≡id (X ∷ Xs , x , xs) rewrite to∘fr≡id (Xs , xs) = refl

module RN where

  to : R.Record → N.Record
  to (R.ε , tt) = [] , tt
  to (S R.< T , s , t) = let Xs , X = to (T s , t) in S ∷ Xs  , s , X

  fr : N.Record → R.Record
  fr ([] , tt) = R.ε , tt
  fr (X ∷ Xs , x , xs) = let T , t = fr (Xs , xs) in X R.< const T , x , t

  to∘fr≡id : ∀ r → to (fr r) ≡ r
  to∘fr≡id ([] , _) = refl
  to∘fr≡id (X ∷ Xs , x , xs) rewrite to∘fr≡id (Xs , xs) = refl
\end{code}

### Definition: Distributivity of equality of pointed *codes* over sigma *codes*

Around the same time I also asked myself whether the statement that "
1. left-nested dependently-typed records
2. right-nested dependently-typed records
3. lists of pointed types
are all isomorphic" could be a consequence of `DistrEqPtdΣ`.

I thought that might be the case but never attempted to prove it. I
have now tried and it doesn't actually seem to work. It appears one
needs a stronger, quite "universe-generic" statement, such as the
following:

\begin{code}
DistrEqPtd°Σ : ∀ lU → Set (S lU)
DistrEqPtd°Σ lU = (U1 : Set lU)(El1 : U1 → Set)
                  (U2 : Set lU)(El2 : U2 → Set)
                  (U3 : Set lU)(El3 : U3 → Set)
                  (°Σ : (A : U1) → (El1 A → U2) → U3)
                  (_°,_ : ∀ {A B} → (a : El1 A) → El2 (B a) → El3 (°Σ A B))
                  {A : U1}{B : El1 A → U2}{C : U1}{D : El1 C → U2}
                  {a : El1 A}{b : El2 (B a)}{c : El1 C}{d : El2 (D c)} →
                       Eq (Σ U3 El3) (°Σ A B   , a °, b) (°Σ C D    , c °, d)
                  ≡ (  Eq (Σ U1 El1) (   A     , a     ) (   C      , c     )
                     × Eq (Σ U2 El2) (     B a ,      b) (     D c  ,      d))
\end{code}

As shown below, `DistrEqPtd°Σ` generalises `DistrEqPtd`:

\begin{code}
private ↓ : DistrEqPtd°Σ (S Z) → DistrEqPtdΣ
        ↓ d = d Set id Set id Set id Σ _,_
\end{code}

It also looks a bit too strong: I don't really know whether this is
safe to assume.

### Obs 2: By assuming `DistrEqPtd°Σ`, we also obtain isomorphisms

The following code shows how `DistrEqPtd°Σ` entails that lists of
pointed types (`N.Record`) are not only a "normal form" for
left-nested and right-nested records (`L.Record`, `R.Record`), but
they are also isomorphic to both.

\begin{code}
module LN+ (d : DistrEqPtd°Σ (S Z)) where

  open LN

  fr∘to≡id : ∀ r → fr (to r) ≡ r
  fr∘to≡id (L.ε , _) = refl
  fr∘to≡id (Γ L.> τ , ts , t) rewrite fr∘to≡id (Γ , ts) =
    let p = d L.Cx L.⟦_⟧ Set id L.Cx L.⟦_⟧ L._>_ _,_ in
    coe (sym p) (refl , refl)

module RN+ (d : DistrEqPtd°Σ (S Z)) where

  open RN

  fr∘to≡id : ∀ r → fr (to r) ≡ r
  fr∘to≡id (R.ε , tt) = refl
  fr∘to≡id (S R.< T , s , t) rewrite fr∘to≡id (T s , t) =
    let p = d Set id R.Cx R.⟦_⟧ R.Cx R.⟦_⟧ R._<_ _,_ in
    coe (sym p) (refl , refl)
\end{code}

## Other encodings of (left-nested) records

Definitions "equivalent" to those in `N`, `L` and `R` easy to obtain
by induction over natural numbers: no `data` or inductive-recursive
definitions are really necessary, and in principle one could do "this"
in ITT without W (maybe η for Σs is required as well).

Let's consider left-nested records. Though one may object over the use
of the equality type in `⟦ε⟧` and `⟦>⟧`, it seems reasonable to say
that an encoding of left-nested record types is a family of sets that
satisfies the "predicate" `LeftNestedRecordFamSet`:

\begin{code}
record LeftNestedRecordFamSet (Cx : Set₁)(⟦_⟧ : Cx → Set) l : Set (S l) where
  constructor leftnested
  field
    ε   : Cx
    _>_ : (Γ : Cx)(τ : ⟦ Γ ⟧ → Set) → Cx
    ⟦ε⟧  :               ⟦ ε ⟧ ≡ ⊤
    ⟦>⟧  : ∀ {Γ τ} → ⟦ Γ > τ ⟧ ≡ Σ ⟦ Γ ⟧ τ

  * = coe (sym ⟦ε⟧) tt

  *-lem : (x : ⟦ ε ⟧) → * ≡ x
  *-lem = lem⊤ (sym ⟦ε⟧) _

  >_> : ∀ {Γ τ} → Σ ⟦ Γ ⟧ τ → ⟦ Γ > τ ⟧
  >_> {_}{_} = coe (sym ⟦>⟧)

  field -- initiality (sort of)
    elimCx⟦⟧ : (P : (Γ : Cx) → ⟦ Γ ⟧ → Set l) →
               P ε * →
               ((Γ : Cx)(τ : ⟦ Γ ⟧ → Set)(s : ⟦ Γ ⟧)(t : τ s) → P Γ s → P (Γ > τ) > s , t >) →
               (Γ : Cx)(xs : ⟦ Γ ⟧) → P Γ xs
    elimCx⟦⟧-ε : ∀ {P : (Γ : Cx) → ⟦ Γ ⟧ → Set l}{mε m>} →
                   elimCx⟦⟧ P mε m> ε *
                 ≡ mε
    elimCx⟦⟧-> : ∀ {P : (Γ : Cx) → ⟦ Γ ⟧ → Set l}{mε m> Γ τ s t} →
                   elimCx⟦⟧ P mε m> (Γ > τ) > s , t >
                 ≡ m> Γ τ s t (elimCx⟦⟧ P mε m> Γ s)
\end{code}

`L.Record` fits the bill.

\begin{code}
module L+++ where

  open L

  elimCx⟦⟧ : {l : _}(P : (Γ : Cx) → ⟦ Γ ⟧ → Set l) →
             P ε tt →
             ((Γ : Cx)(τ : ⟦ Γ ⟧ → Set)(s : ⟦ Γ ⟧)(t : τ s) → P Γ s → P (Γ > τ) (s , t)) →
             (Γ : Cx)(xs : ⟦ Γ ⟧) → P Γ xs
  elimCx⟦⟧ P mε m> ε       _       = mε
  elimCx⟦⟧ P mε m> (Γ > τ) (s , t) = m> Γ τ s t (elimCx⟦⟧ P mε m> Γ s)

  left : ∀ {l} → LeftNestedRecordFamSet L.Cx L.⟦_⟧ l
  left = leftnested L.ε L._>_ refl refl elimCx⟦⟧ refl refl
\end{code}

However, we can just use natural numbers and their eliminator to
obtain an "equivalent" definition.

\begin{code}
elimℕ : {l : _}(P : ℕ → Set l) → P zero → ((n : ℕ) → P n → P (suc n)) → (n : ℕ) → P n
elimℕ P mz ms zero    = mz
elimℕ P mz ms (suc n) = ms n (elimℕ P mz ms n)

module ℕL where

  Cx⟦⟧/ : (n : ℕ) → Σ Set₁ λ S → S → Set
  Cx⟦⟧/ = elimℕ _ (⊤ , λ _ → ⊤)
                  (λ n r → let Cx/n , ⟦_⟧/ = r in
                             (Σ Cx/n λ Γ → ⟦ Γ ⟧/ → Set)
                           , λ { (Γ , τ) → Σ ⟦ Γ ⟧/ λ s → τ s })

  Cx/ : ℕ → Set _
  Cx/ n = fst (Cx⟦⟧/ n)

  ⟦_⟧/ : ∀ {n} → Cx/ n → Set _
  ⟦_⟧/ {n} = snd (Cx⟦⟧/ n)

  Cx : Set _
  Cx = Σ ℕ Cx/

  ⟦_⟧ : Cx → Set _
  ⟦ n , Γ ⟧ = ⟦_⟧/ {n} Γ

  ε : Cx
  ε = zero , tt

  _>_ : (Γ : Cx)(τ : ⟦ Γ ⟧ → Set) → Cx
  (n , Γ) > τ = suc n , Γ , τ

  elimCx⟦⟧ : {l : _}(P : (Γ : Cx) → ⟦ Γ ⟧ → Set l) →
             P ε tt →
             ((Γ : Cx)(τ : ⟦ Γ ⟧ → Set)(s : ⟦ Γ ⟧)(t : τ s) → P Γ s → P (Γ > τ) (s , t)) →
             (Γ : Cx)(xs : ⟦ Γ ⟧) → P Γ xs
  elimCx⟦⟧ P mε m> = uc $ elimℕ C mz ms
    where C  = λ n → (Γ : Cx/ n)(xs : ⟦ n , Γ ⟧) → P (n , Γ) xs
          mz = λ _ _       → mε
          ms = λ n ih Γ xs → m> _ _ _ _ (ih _ _)

  Record = Σ Cx ⟦_⟧
\end{code}

Also this definition is a valid encoding of left-nested records.

\begin{code}
  left : ∀ {l} → LeftNestedRecordFamSet Cx ⟦_⟧ l
  left = leftnested ε _>_ refl refl elimCx⟦⟧ refl refl
\end{code}

## Questions

A) Is the name "distributivity of equality of pointed types over
   sigmas" appropriate?

If not, how should one call this property?

B) Is `DistrEqPtdΣ` consistent with Agda, with or without K?

C) Does `DistrEqPtdΣ` *imply* UIP?

My guess is that it does not.

D) Is `DistrEqPtd°Σ` consistent with Agda, with or without K?

E) If they are inconsistent, would the versions where (the outermost)
   equality is replaced by implication be safe instead?

For example, for `DistrEqPtdΣ`:

    Eq Ptd (A     , a    ) (C     , c    ) →
    Eq Ptd (  B a ,     b) (  D c ,     d) →
    Eq Ptd (Σ A B , a , b) (Σ C D , c , d)

F) (vague) Is there a categorical notion related to `LN.to` and `RN.to`?

G) On the alternative encodings of left-nested records:

- Is it possible to prove that `L.Record` and `ℕL.Record` are
  isomorphic under no assumptions?

- In case it isn't, is `DistrEqPtd°Σ` enough?

  I don't have time to try now, but it doesn't look straightforward.

- Do better studied assumption (e.g., Univalence in Agda --without-K) help?

- More interestingly: what consistent assumptions, if any, allow to
  prove that all families satisfying `LeftNestedRecordFamSet` are
  isomorphic?

H) Can `DistrEqPtdΣ` or `DistrEqPtd°Σ` provide a proof of `Even ≡ Odd → ⊥`?

See Martín Escardó's message to the HoTT list at
https://groups.google.com/forum/#!topic/homotopytypetheory/qydSwbvj1uE .

\begin{code}
open import Data.Nat

data IsEven : ℕ → Set
data IsOdd  : ℕ → Set

data IsEven where
  zero : IsEven zero
  even : ∀ {n} → IsOdd n → IsEven (suc n)

data IsOdd where
  odd : ∀ {n} → IsEven n → IsOdd (suc n)

Even = Σ _ IsEven
Odd  = Σ _ IsOdd

module _ (distrEqPtdΣ : DistrEqPtdΣ)(?? : ∀ {X} → X) where

  Even≢Odd : Even ≡ Odd → ⊥
  Even≢Odd p = ??
\end{code}

My understanding is that they do not.



Thanks in advance for any feedback! :-)

20151003 <matteo.acerbi@gmail.com>