Lecture 3-1: The Structure Identity Principle

In Lecture 2-X we saw how univalence can be used to show that paths between types the same as equivalences between those types. But what if our types have extra structure, like algebraic operations or axioms? In this Lecture, we extend univalence to the Structure Identity Principle, which shows that paths between structured types are equivalent to structure-preserving equivalences between those types.

We’ll be following the paper Internalizing representation independence with univalence, by Angiuli, Cavallo, Mörtberg and Zeuner.

What exactly is “structure”? A structure on a type is some collection of functions involving that type and axioms that those functions have to satisfy. To describe that collection, we will simply use a function from types to types: the input type is the “carrier” type of the structure, and the output type is the extra data that that is necessary to equip the carrier with the specified structure.

StrNotion : (ℓ ℓ' : Level) → Type (ℓ-suc (ℓ-max ℓ ℓ'))
StrNotion ℓ ℓ' = Type ℓ → Type ℓ'

Almost the simplest example of a structure we can give is that of a “magma”, which is simply a binary operation that need not satisfy any additional properties.

Magma-Str : StrNotion ℓ ℓ
Magma-Str X = X → X → X

So, to say that a type X is a magma, that is, X has a magma structure, we have to equip it with an element of Magma-Str X. The type of all magmas (with a fixed universe level) is then:

record Magmaʳ (ℓ : Level) : Type (ℓ-suc ℓ) where
  constructor Magma-data
  field
    typ : Type ℓ
    str : Magma-Str typ

open Magmaʳ

So for example, the natural numbers form a Magma.

ℕ-Magmaʳ : Magmaʳ ℓ-zero
ℕ-Magmaʳ .typ = ℕ 
ℕ-Magmaʳ .str = _+ℕ_

Show that the booleans form a Magma under and.

Bool-and-Magmaʳ : Magmaʳ ℓ-zero
-- Exercise:
-- Bool-and-Magmaʳ = {!!}

We usually want to know that our operations obey some axioms. For example, a “semigroup” is a type with an associative binary operation.

Semigroup-Str : StrNotion ℓ ℓ
Semigroup-Str X = 
  Σ[ _·_ ∈ (X → X → X) ] 
  ((x y z : X) → x · (y · z) ≡ (x · y) · z)

record Semigroupʳ (ℓ : Level) : Type (ℓ-suc ℓ) where
  constructor Semigroup-data
  field
    type : Type ℓ
    str : Semigroup-Str type

open Semigroupʳ

We have already seen that addition of natural numbers is associative, so this shows that ℕ is also a semigroup:

ℕ-Semigroup : Semigroupʳ ℓ-zero
ℕ-Semigroup .type = ℕ 
ℕ-Semigroup .str = _+ℕ_ , +ℕ-assoc

A single type can support many non-equal versions of the same structure. We could have done just the same with Bool and and.

Notions of structure like this are what we are going to generalise. Given a notion of structure S : Type ℓ → Type ℓ', an S-structured type is an element of

record Type-with (ℓ : Level) (S : StrNotion ℓ ℓ') : Type (ℓ-max (ℓ-suc ℓ) ℓ') where
  constructor Type-with-data
  field
    type : Type ℓ
    str : S type

open Type-with

explode-Type-with : {ℓ : Level} {S : StrNotion ℓ ℓ'} 
  → Type-with ℓ S ≃ (Σ[ X ∈ Type ℓ ] S X)
explode-Type-with 
  = inv→equiv (λ t → t .type , t .str) 
              (λ p → Type-with-data (p .fst) (p .snd)) 
              (λ _ → refl) 
              (λ _ → refl)

So, we reconstruct our Magma and Semigroup types as

Magma : (ℓ : Level) → Type (ℓ-suc ℓ)
Magma ℓ = Type-with ℓ Magma-Str

Semigroup : (ℓ : Level) → Type (ℓ-suc ℓ)
Semigroup ℓ = Type-with ℓ Semigroup-Str

ℕ-Magma : Magma ℓ-zero
ℕ-Magma .type = ℕ
ℕ-Magma .str = _+ℕ_

Bool-and-Magma : Magma ℓ-zero
Bool-and-Magma .type = Bool 
Bool-and-Magma .str = _and_

Caution: The definitions of Magma and Semigroup above should more properly be called ∞-Magma and ∞-Semigroup, because we have not assumed that the underlying types X are sets. General types have higher-dimensional paths, and to be well behaved, a notion of structure typically has to 1) kill the higher paths or 2) add equations explaining how the operations interact with paths. Here’s how option 1) looks here:

Semigroup-Set-Str : StrNotion ℓ ℓ
Semigroup-Set-Str X = Σ[ _·_ ∈ (X → X → X) ] ((x y z : X) → x · (y · z) ≡ (x · y) · z) × isSet X

Semigroup-Set : (ℓ : Level) → Type (ℓ-suc ℓ)
Semigroup-Set ℓ = Σ[ X ∈ Type ℓ ] Semigroup-Set-Str X

ℕ-Semigroup-Set : Semigroup-Set ℓ-zero
ℕ-Semigroup-Set = ℕ , _+ℕ_ , +ℕ-assoc , isSet-ℕ

Structured Equivalences

Not all functions between structured types respect the structure that the types come with. For magmas, semigroups, monoids, groups and so on, we are only interested in homomorphisms: those functions that respect the underlying binary operation. This is easy to describe as a type.

isMagmaHom : (A B : Magma ℓ) → (A .type → B .type) → Type ℓ
isMagmaHom (Type-with-data A _·A_) (Type-with-data B _·B_) f
  = (a₁ a₂ : A) → f (a₁ ·A a₂) ≡ (f a₁) ·B (f a₂)

The function isZero : ℕ → Bool is a homomorphism, as long as we choose the right Magma structure on both sides.

isZero-isHom : isMagmaHom ℕ-Magma Bool-and-Magma isZero
-- Exercise:
-- isZero-isHom a a' = {!!}

An equivalence of magmas is an ordinary equivalence between types so that the underlying function is a homomorphism in this above sense. (isZero is of course not an equivalence.)

_≃[Magma]_ : (A B : Magma ℓ) → Type ℓ
A ≃[Magma] B = Σ[ e ∈ A .type ≃ B .type ] (isMagmaHom A B (e .map))

Again, this situation is what we want to generalise to other notions of structure. Let us define a “notion of structured equivalence” to be the extra information that an equivalence needs in order to respect the structures on the types at either end. In the magma case, this is the isMagmaHom type. A structured equivalence is then an equivalence together with an instance of this information.

StrEquivNotion : (S : StrNotion ℓ ℓ'') (ℓ' : Level) → Type (ℓ-max (ℓ-suc (ℓ-max ℓ ℓ')) ℓ'')
StrEquivNotion S ℓ' = (A B : Type-with _ S) → A .type ≃ B .type → Type ℓ'

record StrEquiv {S : StrNotion ℓ ℓ'} (ι : StrEquivNotion S ℓ'') (A : Type-with ℓ S) (B : Type-with ℓ S) : Type (ℓ-max ℓ ℓ'') where
  constructor StrEquiv-data
  field
    eq : A .type ≃ B .type
    proof : ι A B eq

open StrEquiv

explode-StrEquiv : {S : StrNotion ℓ ℓ'} {ι : StrEquivNotion S ℓ''} {A : Type-with ℓ S} {B : Type-with ℓ S}
  → StrEquiv ι A B ≃ (Σ[ e ∈ A .type ≃ B .type ]  ι A B e)
explode-StrEquiv 
  = inv→equiv (λ t → t .eq , t .proof)
              (λ p → StrEquiv-data (p .fst) (p .snd))
              (λ _ → refl)
              (λ _ → refl)

To make this easier to read, we’ll add some nicer syntax for these structured equivalences.

_≃[_]_ : {S : StrNotion ℓ ℓ'} → (A : Type-with ℓ S) (ι : StrEquivNotion S ℓ'') (B : Type-with ℓ S) → Type (ℓ-max ℓ ℓ'')
A ≃[ ι ] B = StrEquiv ι A B

Magma-EquivNotion : StrEquivNotion Magma-Str ℓ
Magma-EquivNotion A B e = isMagmaHom A B (e .map)

How do we know when we’ve chosen the right notion of structure for our equivalences? Well, the crucial feature of equivalences is univalence; that equivalences between types can be turned into paths in the universe. We will use this as a guide for our structured equivalences. Whatever the notion of structured equivalence is, it should be possible to turn it into a path between the structures, as a path-over the path between types given by univalence. That is, we will seek to inhabit the following type.

-- mvrnote: should rename this, not propositional
StrNotion-isUnivalent : (S : StrNotion ℓ ℓ') (ι : StrEquivNotion S ℓ'') → Type (ℓ-max (ℓ-max (ℓ-suc ℓ) ℓ') ℓ'')
StrNotion-isUnivalent S ι =
  {A B : Type-with _ S} (e : A .type ≃ B .type)
  → ι A B e ≃ PathP (λ i → S (ua e i)) (A .str) (B .str)

For our Magma-EquivNotion, this is:

≃[Magma]-univalent : {A B : Magma ℓ} (e : A .type ≃ B .type)  →
  isMagmaHom A B (e .map) ≃ PathP (λ i → Magma-Str (ua e i)) (A .str) (B .str)

We can indeed prove this, by gluing together lots of equivalences that we’ve already shown in previous lectures. It’s boring and fiddly, so we’ll just do it for you.

The upshot of knowing ≃[Magma]-univalent is that we can upgrade univalence to something that works on entire magmas, and not just their underlying types. This is what we call the structure identity principle.

SIP-Magma : {A B : Magma ℓ} → (A ≃[ Magma-EquivNotion ] B) ≃ (A ≡ B)
SIP-Magma {A = A} {B = B} =
  (A ≃[ Magma-EquivNotion ] B)
    ≃⟨ explode-StrEquiv ⟩
  Σ[ e ∈ (A .type ≃ B .type) ] Magma-EquivNotion A B e
    ≃⟨ Σ-map-≃ (invEquiv univalence) ≃[Magma]-univalent ⟩
  Σ[ p ∈ (A .type ≡ B .type) ] PathP (λ i → Magma-Str (p i)) (A .str) (B .str)
    ≃⟨ ΣPath≃PathΣ ⟩
  (A .type , A .str) ≡ (B .type , B .str)
    ≃⟨ ap-≃ (invEquiv explode-Type-with) ⟩
  (A ≡ B)
    ∎e

This works totally generically using the abstract setup we have been developing so far. Try putting the pieces together!

module _ {S : StrNotion ℓ ℓ'} {ι : StrEquivNotion S ℓ'}
  (θ : StrNotion-isUnivalent S ι) (A B : Type-with ℓ S)
  where

  SIP : (A ≃[ ι ] B) ≃ (A ≡ B)
  -- Exercise:
  -- SIP = {!!}

  sip : (A ≃[ ι ] B) → A ≡ B
  -- Exercise:
  -- sip = {!!}

  sipInv : A ≡ B → A ≃[ ι ] B
  -- Exercise:
  -- sipInv = {!!}

Transferring Proofs

Alright, that was a lot of set-up, so let’s try and get some payoff. Once we have paths between structures, we can attempt to transfer proofs between those structures.

First, an easy warmup. Bool is also a magma under or, and in fact the function not is a structured equivalence between these two versions of Bool as a magma.

Bool-or-Magma : Magma ℓ-zero
Bool-or-Magma .type = Bool 
Bool-or-Magma .str = _or_

not-isMagmaHom : (a a' : Bool) → not (a or a') ≡ (not a and not a')
not-isMagmaHom true true = refl
not-isMagmaHom true false = refl
not-isMagmaHom false true = refl
not-isMagmaHom false false = refl

not-[Magma]≃ : Bool-or-Magma ≃[ Magma-EquivNotion ] Bool-and-Magma
not-[Magma]≃ .eq = not-≃ 
not-[Magma]≃ .proof = not-isMagmaHom

Bool-or≡Bool-and : Bool-or-Magma ≡ Bool-and-Magma
Bool-or≡Bool-and = sip ≃[Magma]-univalent Bool-or-Magma Bool-and-Magma not-[Magma]≃

Way back in Lecture 2-X, we showed that or is an associative operation. We can use this path that we just proved to transfer this proof over to and.

or≡and : PathP (λ i → Magma-Str (Bool-or≡Bool-and i .type)) 
  _or_
  _and_
or≡and i = Bool-or≡Bool-and i .str

and-assoc : (m n o : Bool) → m and (n and o) ≡ (m and n) and o
and-assoc = transport (λ i → (m n o : Bool-or≡Bool-and i .type) → 
                         or≡and i m (or≡and i n o) ≡ or≡and i (or≡and i m n) o)
            or-assoc

This wasn’t too impressive, because and-assoc would have been easy enough to prove by hand. But this works for equivalences of any complexity. For a more interesting example, let’s look at a binary representation of the natural numbers.

We can think of a binary number as being built up from left to right, one digit at a time. Starting with the empty string corresponding to zero, each additional digit doubles the value of all the previous digits, and then decides whether or not to add 1. For 1101 say, we have

corresponds to $0$
1 corresponds to $1 + (2 \times 0) = 1$
11 corresponds to $1 + (2 \times 1) = 3$
110 corresponds to $0 + (2 \times 3) = 6$
1101 corresponds to $1 + (2 \times 6) = 13$

This is what we want to capture as an inductive data-type, with a catch: we don’t want our binary strings to be allowed to begin with a string of pointless 0s. To avoid this, we will replace the “just multiply by two” option with an “add one and multiply by two” option, so that we no longer have many different ways to represent zero.

In all, we have partitioned the natural numbers into three categories: zero, non-zero even (so $n = 2 \times (1 + k)$ ), or odd (so $n = 1 + (2 \times k)$ ).

Aside: We’ve stolen this encoding from the redtt project.

data ℕᵇ : Type where
  zeroᵇ   : ℕᵇ
  2×[1+_] : ℕᵇ → ℕᵇ    -- n → 2 × (1+n) = nonzero even numbers
  1+[2×_] : ℕᵇ → ℕᵇ    -- n → 1 + (2×n) = odd numbers

These can be easily converted from and to regular natural numbers. In one direction by ordinary induction and sucᵇ:

sucᵇ : ℕᵇ → ℕᵇ
sucᵇ zeroᵇ     = 1+[2× zeroᵇ ]
sucᵇ 2×[1+ b ] = 1+[2× (sucᵇ b) ]
sucᵇ 1+[2× b ] = 2×[1+ b ]

ℕ→ℕᵇ : ℕ → ℕᵇ
ℕ→ℕᵇ zero = zeroᵇ
ℕ→ℕᵇ (suc n) = sucᵇ (ℕ→ℕᵇ n)

In the other direction, by turning the constructors of ℕᵇ into the corresponding operations on ℕ.

ℕᵇ→ℕ : ℕᵇ → ℕ
-- Exercise: (Use `doubleℕ`!)
-- ℕᵇ→ℕ b = {!!}

These functions are components of an equivalence.

ℕᵇ→ℕ-suc : (n : ℕᵇ) → ℕᵇ→ℕ (sucᵇ n) ≡ suc (ℕᵇ→ℕ n)
ℕᵇ→ℕ-suc zeroᵇ       = refl
ℕᵇ→ℕ-suc 2×[1+ b ] i = suc (doubleℕ (ℕᵇ→ℕ-suc b i))
ℕᵇ→ℕ-suc 1+[2× b ]   = refl

ℕᵇ≃ℕ : ℕᵇ ≃ ℕ
ℕᵇ≃ℕ = inv→equiv ℕᵇ→ℕ ℕ→ℕᵇ to-fro fro-to
  where
    to-fro : isSection ℕᵇ→ℕ ℕ→ℕᵇ
    to-fro zero = refl
    to-fro (suc n) =
      ℕᵇ→ℕ (sucᵇ (ℕ→ℕᵇ n)) ≡⟨ ℕᵇ→ℕ-suc (ℕ→ℕᵇ n) ⟩
      suc (ℕᵇ→ℕ (ℕ→ℕᵇ n)) ≡⟨ ap suc (to-fro n) ⟩
      suc n ∎

    sucᵇ-to-doubleℕ : (n : ℕ) → sucᵇ (ℕ→ℕᵇ (doubleℕ n)) ≡ 1+[2× (ℕ→ℕᵇ n)]
    sucᵇ-to-doubleℕ zero      = refl
    sucᵇ-to-doubleℕ (suc n) i = sucᵇ (sucᵇ (sucᵇ-to-doubleℕ n i))

    fro-to : isRetract ℕᵇ→ℕ ℕ→ℕᵇ
    fro-to zeroᵇ = refl
    fro-to 2×[1+ b ] =
      sucᵇ (sucᵇ (ℕ→ℕᵇ (doubleℕ (ℕᵇ→ℕ b)))) ≡⟨ ap sucᵇ (sucᵇ-to-doubleℕ (ℕᵇ→ℕ b)) ⟩
      2×[1+ ℕ→ℕᵇ (ℕᵇ→ℕ b) ]                 ≡⟨ ap 2×[1+_] (fro-to b) ⟩
      2×[1+ b ]                             ∎
    fro-to 1+[2× b ] =
      sucᵇ (ℕ→ℕᵇ (doubleℕ (ℕᵇ→ℕ b))) ≡⟨ sucᵇ-to-doubleℕ (ℕᵇ→ℕ b) ⟩
      1+[2× ℕ→ℕᵇ (ℕᵇ→ℕ b) ]          ≡⟨ ap 1+[2×_] (fro-to b) ⟩
      1+[2× b ]                      ∎

ℕᵇ≡ℕ : ℕᵇ ≡ ℕ
ℕᵇ≡ℕ = ua ℕᵇ≃ℕ

Now ℕᵇ also supports an inductive addition operation, so we can give it a Magma structure.

_+ℕᵇ_ : ℕᵇ → ℕᵇ → ℕᵇ
zeroᵇ    +ℕᵇ y          = y
2×[1+ b ] +ℕᵇ zeroᵇ     = 2×[1+ b ]
2×[1+ b ] +ℕᵇ 2×[1+ c ] = 2×[1+ sucᵇ (b +ℕᵇ c) ]
2×[1+ b ] +ℕᵇ 1+[2× c ] = sucᵇ 2×[1+ (b +ℕᵇ c) ]
1+[2× b ] +ℕᵇ zeroᵇ     = 1+[2× b ]
1+[2× b ] +ℕᵇ 2×[1+ c ] = sucᵇ 2×[1+ (b +ℕᵇ c) ]
1+[2× b ] +ℕᵇ 1+[2× c ] = sucᵇ 1+[2× (b +ℕᵇ c) ]

infixl 6 _+ℕᵇ_

ℕᵇ-Magma : Magma ℓ-zero
ℕᵇ-Magma .type = ℕᵇ 
ℕᵇ-Magma .str = _+ℕᵇ_

The last thing to do is verify that the ℕᵇ→ℕ function respects this Magma strucutre. This involves some pain, but we’ve done most of it for you.

doubleℕ-+ℕ : (n m : ℕ) → doubleℕ (n +ℕ m) ≡ doubleℕ n +ℕ doubleℕ m
doubleℕ-+ℕ zero m = refl
doubleℕ-+ℕ (suc n) m i = suc (suc (doubleℕ-+ℕ n m i))

ℕᵇ→ℕ-hom : (b c : ℕᵇ) → ℕᵇ→ℕ (b +ℕᵇ c) ≡ (ℕᵇ→ℕ b) +ℕ (ℕᵇ→ℕ c)
ℕᵇ→ℕ-hom zeroᵇ c = refl
ℕᵇ→ℕ-hom 2×[1+ b ] zeroᵇ = ap (suc ∘ suc) (sym (+ℕ-idr (doubleℕ (ℕᵇ→ℕ b))))
ℕᵇ→ℕ-hom 2×[1+ b ] 2×[1+ c ] =
  ℕᵇ→ℕ (2×[1+ b ] +ℕᵇ 2×[1+ c ])                         ≡⟨ refl ⟩
  ℕᵇ→ℕ (2×[1+ sucᵇ (b +ℕᵇ c) ])                          ≡⟨ refl ⟩
  doubleℕ (suc (ℕᵇ→ℕ (sucᵇ (b +ℕᵇ c))))                  ≡⟨ ap (doubleℕ ∘ suc) (ℕᵇ→ℕ-suc (b +ℕᵇ c)) ⟩
  doubleℕ (suc (suc (ℕᵇ→ℕ (b +ℕᵇ c))))                   ≡⟨ ap (doubleℕ ∘ suc ∘ suc) (ℕᵇ→ℕ-hom b c) ⟩
  doubleℕ (suc (suc (ℕᵇ→ℕ b +ℕ ℕᵇ→ℕ c)))                 ≡⟨ ap (doubleℕ ∘ suc) (sym (+ℕ-comm-helper (ℕᵇ→ℕ b) (ℕᵇ→ℕ c))) ⟩
  doubleℕ (suc (ℕᵇ→ℕ b) +ℕ suc (ℕᵇ→ℕ c))                 ≡⟨ doubleℕ-+ℕ (suc (ℕᵇ→ℕ b)) (suc (ℕᵇ→ℕ c)) ⟩
  doubleℕ (suc (ℕᵇ→ℕ b)) +ℕ doubleℕ (suc (ℕᵇ→ℕ c))       ≡⟨ refl ⟩
  ℕᵇ→ℕ (2×[1+ b ]) +ℕ ℕᵇ→ℕ (2×[1+ c ])                   ∎

ℕᵇ→ℕ-hom 2×[1+ b ] 1+[2× c ] =
  ℕᵇ→ℕ (2×[1+ b ] +ℕᵇ 1+[2× c ])                         ≡⟨ refl ⟩
  ℕᵇ→ℕ 1+[2× sucᵇ (b +ℕᵇ c) ]                            ≡⟨ refl ⟩
  suc (doubleℕ (ℕᵇ→ℕ (sucᵇ (b +ℕᵇ c))))                  ≡⟨ ap (suc ∘ doubleℕ) (ℕᵇ→ℕ-suc (b +ℕᵇ c)) ⟩
  suc (doubleℕ (suc (ℕᵇ→ℕ (b +ℕᵇ c))))                   ≡⟨ ap (suc ∘ doubleℕ ∘ suc) (ℕᵇ→ℕ-hom b c) ⟩
  suc (doubleℕ (suc (ℕᵇ→ℕ b +ℕ ℕᵇ→ℕ c)))                 ≡⟨ ap (suc ∘ suc ∘ suc) (doubleℕ-+ℕ (ℕᵇ→ℕ b)(ℕᵇ→ℕ c)) ⟩
  suc (suc (suc (doubleℕ (ℕᵇ→ℕ b) +ℕ doubleℕ (ℕᵇ→ℕ c)))) ≡⟨ ap (suc ∘ suc) (sym (+ℕ-comm-helper (doubleℕ (ℕᵇ→ℕ b)) (doubleℕ (ℕᵇ→ℕ c))))  ⟩
  suc (suc (doubleℕ (ℕᵇ→ℕ b) +ℕ suc (doubleℕ (ℕᵇ→ℕ c)))) ≡⟨ refl ⟩
  (doubleℕ (suc (ℕᵇ→ℕ b)) +ℕ suc (doubleℕ (ℕᵇ→ℕ c)))     ≡⟨ refl ⟩
  ℕᵇ→ℕ (2×[1+ b ]) +ℕ ℕᵇ→ℕ (1+[2× c ])                   ∎

ℕᵇ→ℕ-hom 1+[2× b ] zeroᵇ = ap suc (sym (+ℕ-idr (doubleℕ (ℕᵇ→ℕ b))))

ℕᵇ→ℕ-hom 1+[2× b ] 2×[1+ c ] =
  -- Exercise:
  -- ℕᵇ→ℕ (1+[2× b ] +ℕᵇ 2×[1+ c ])                         ≡⟨ {!!} ⟩
  -- ℕᵇ→ℕ 1+[2× sucᵇ (b +ℕᵇ c) ]                            ≡⟨ {!!} ⟩
  -- suc (doubleℕ (ℕᵇ→ℕ (sucᵇ (b +ℕᵇ c))))                  ≡⟨ {!!} ⟩
  -- suc (doubleℕ (suc (ℕᵇ→ℕ (b +ℕᵇ c))))                   ≡⟨ {!!} ⟩
  -- suc (doubleℕ (suc (ℕᵇ→ℕ b +ℕ ℕᵇ→ℕ c)))                 ≡⟨ {!!} ⟩
  -- suc (doubleℕ (ℕᵇ→ℕ b +ℕ suc (ℕᵇ→ℕ c)))                 ≡⟨ {!!} ⟩
  -- suc (doubleℕ (ℕᵇ→ℕ b) +ℕ doubleℕ (suc (ℕᵇ→ℕ c)))       ≡⟨ {!!} ⟩
  -- (suc (doubleℕ (ℕᵇ→ℕ b)) +ℕ (doubleℕ (suc (ℕᵇ→ℕ c))))   ≡⟨ {!!} ⟩
  -- ℕᵇ→ℕ (1+[2× b ]) +ℕ ℕᵇ→ℕ (2×[1+ c ])                   ∎

ℕᵇ→ℕ-hom 1+[2× b ] 1+[2× c ] =
  -- Exercise:
  -- ℕᵇ→ℕ (1+[2× b ] +ℕᵇ 1+[2× c ])                         ≡⟨ {!!} ⟩
  -- ℕᵇ→ℕ 2×[1+ b +ℕᵇ c ]                                   ≡⟨ {!!} ⟩
  -- (doubleℕ (suc (ℕᵇ→ℕ (b +ℕᵇ c))))                       ≡⟨ {!!} ⟩
  -- (doubleℕ (suc (ℕᵇ→ℕ b +ℕ ℕᵇ→ℕ c)))                     ≡⟨ {!!} ⟩
  -- suc (suc (doubleℕ (ℕᵇ→ℕ b +ℕ ℕᵇ→ℕ c)))                 ≡⟨ {!!} ⟩
  -- suc (suc (doubleℕ (ℕᵇ→ℕ b) +ℕ doubleℕ (ℕᵇ→ℕ c)))       ≡⟨ {!!} ⟩
  -- (suc (doubleℕ (ℕᵇ→ℕ b))) +ℕ (suc (doubleℕ (ℕᵇ→ℕ c)))   ≡⟨ {!!} ⟩
  -- (ℕᵇ→ℕ 1+[2× b ]) +ℕ (ℕᵇ→ℕ 1+[2× c ])                   ∎

ℕᵇ≃[Magma]ℕ : ℕᵇ-Magma ≃[ Magma-EquivNotion ] ℕ-Magma
ℕᵇ≃[Magma]ℕ .eq = ℕᵇ≃ℕ
ℕᵇ≃[Magma]ℕ .proof = ℕᵇ→ℕ-hom

ℕᵇ-Magma≡ℕ-Magma : ℕᵇ-Magma ≡ ℕ-Magma
ℕᵇ-Magma≡ℕ-Magma = sip ≃[Magma]-univalent ℕᵇ-Magma ℕ-Magma ℕᵇ≃[Magma]ℕ

Now we can transfer proofs about ℕ to proofs about ℕᵇ with essentially no effort. Showing +ℕᵇ-assoc by hand would be painful!

+ℕ≡+ℕᵇ : PathP (λ i → ℕᵇ≡ℕ (~ i) → ℕᵇ≡ℕ (~ i) → ℕᵇ≡ℕ (~ i)) _+ℕ_ _+ℕᵇ_
+ℕ≡+ℕᵇ i = ℕᵇ-Magma≡ℕ-Magma (~ i) .str

+ℕᵇ-assoc : (m n o : ℕᵇ) → m +ℕᵇ (n +ℕᵇ o) ≡ (m +ℕᵇ n) +ℕᵇ o
+ℕᵇ-assoc = 
  transport (λ i → (m n o : ℕᵇ≡ℕ (~ i)) → +ℕ≡+ℕᵇ i m (+ℕ≡+ℕᵇ i n o) 
                                        ≡ +ℕ≡+ℕᵇ i (+ℕ≡+ℕᵇ i m n) o)
  +ℕ-assoc

Thank goodness!

Queues

Let’s do an example that points towards some applications in computer science. Here’s a structure we could use for a first-in, first-out queue:

Maybe : Type ℓ → Type ℓ
Maybe A = ⊤ ⊎ A

Queue-Str : Type → StrNotion ℓ ℓ
Queue-Str A X = X × (A → X → X) × (X → Maybe (X × A))

There are three components, with the following interpretation:

emp, the empty queue,
enq, which “enqueues” a new element onto the back of the queue,
deq, which “dequeues” an element off the front of the queue, either giving back the new queue and the removed element, or giving back nothing if the queue is empty.

These are just the raw operations that we would expect a queue to have, but nothing actually forces it to behave reasonably. (For example, we could define a Queue-Str that is just ⊤ always, regardless of what the type A is.)

To force the queues to actually do something, we’ll want them to satisfy at least the following axioms:

return-or-enq : (Q : Type-with ℓ (Queue-Str A)) → A → Maybe (Q .type × A) → Q .type × A
return-or-enq (Type-with-data Q (emp , enq , deq)) a (inl tt) = emp , a
return-or-enq (Type-with-data Q (emp , enq , deq)) a (inr (q , b)) = enq a q , b

Queue-Axioms : Type-with ℓ (Queue-Str A) → Type ℓ
Queue-Axioms {A = A} (Type-with-data Q (emp , enq , deq)) = 
     (deq emp ≡ inl tt)
   × ((a : A) (q : Q) → deq (enq a q) ≡ inr (return-or-enq (Type-with-data Q (emp , enq , deq)) a (deq q)))
   × ((a a' : A) → (q q' : Q) → enq a q ≡ enq a' q' → (a ≡ a') × (q ≡ q'))
   × ((q q' : Q) → deq q ≡ deq q' → q ≡ q')

In words, these say:

There’s nothing on the front of the empty queue,
Enqueueing then dequeueing is the same as dequeuing and enqueueing (taking care when the queue starts empty)
Enqueueing is an injective operation
Dequeueing is an injective operation (when you include the element that gets dequeued)

Let’s see our first queue implementation: a simple list, where elements are enqueued onto to the front of the list, and dequeued from the back of the list.

SlowQueue : Type → Type
SlowQueue A = List A

empˢ : SlowQueue A
empˢ = []

enqˢ : A → SlowQueue A → SlowQueue A
enqˢ = _::_

deqMap : {X Y : Type ℓ} → (X → Y) → Maybe (X × A) → Maybe (Y × A)
deqMap f = ⊎-map idfun (λ (x , a) → (f x , a))

deqˢ : SlowQueue A → Maybe (SlowQueue A × A)
deqˢ [] = inl tt
deqˢ (x :: []) = inr ([] , x)
deqˢ (x :: x' :: xs) = deqMap (enqˢ x) (deqˢ (x' :: xs))

SlowQueue-model : (A : Type) → Type-with ℓ-zero (Queue-Str A)
SlowQueue-model A .type = SlowQueue A 
SlowQueue-model A .str = empˢ , enqˢ , deqˢ

What makes this “slow”? Well, every time we dequeue, we walk through the whole list to get to the end element, and reconstruct a new list that has that element removed.

There is a famous solution to this problem, which replaces the single list by a pair of lists. Elements are enqueued onto the front of the first list and dequeued from the front of the second list. Whenever this second list is empty, we replace it with the reverse of the front list, so that we indeed end up with a first-in, first-out queue. The cost of reaching the back of the queue for every deque is replaced by an occasional “batch” operation which does the work once.

Aside: This kind of “batched” queue mvrnote: reference “amortised cost”

In cubical type theory we can do one better,

data FastQueue (A : Type) : Type where
  FQ⟨_,_⟩ : (xs : List A) → (ys : List A) → FastQueue A
  tilt : (xs ys : List A) → (z : A) → FQ⟨ xs ++ [ z ] , ys ⟩ ≡ FQ⟨ xs , ys ++ [ z ] ⟩
  trunc : isSet (FastQueue A)

empᶠ : FastQueue A
empᶠ = FQ⟨ [] , [] ⟩

enqᶠ : A → FastQueue A → FastQueue A
enqᶠ a FQ⟨ xs , ys ⟩ = FQ⟨ a :: xs , ys ⟩
enqᶠ a (tilt xs ys z i) = tilt (a :: xs) ys z i
enqᶠ a (trunc q q' α β i j) =
  trunc _ _ (λ i → enqᶠ a (α i)) (λ i → enqᶠ a (β i)) i j

Dequeueing is a little more difficult, and we’ll need to prove some basic facts about lists. We’ll do them all now to get them out of the way.

++-unit-l : (xs : List A) → [] ++ xs ≡ xs
++-unit-l xs = refl

++-unit-r : (xs : List A) → xs ++ [] ≡ xs
++-unit-r [] = refl
++-unit-r (x :: xs) = ap (_::_ x) (++-unit-r xs)

++-assoc : (xs ys zs : List A) → (xs ++ ys) ++ zs ≡ xs ++ ys ++ zs
++-assoc [] ys zs = refl
++-assoc (x :: xs) ys zs = ap (_::_ x) (++-assoc xs ys zs)

reverse-++ : (xs ys : List A) → reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
reverse-++ [] ys = sym (++-unit-r (reverse ys))
reverse-++ (x :: xs) ys =
  reverse ((x :: xs) ++ ys)
    ≡⟨ ap (λ zs → zs ++ [ x ]) (reverse-++ xs ys) ⟩
  (reverse ys ++ reverse xs) ++ [ x ]
    ≡⟨ ++-assoc (reverse ys) (reverse xs) [ x ] ⟩
  reverse ys ++ reverse (x :: xs) 
    ∎

reverse-snoc : (xs : List A) (y : A) → reverse (xs ++ [ y ]) ≡ y :: reverse xs
reverse-snoc [] y = refl
reverse-snoc (x :: xs) y = ap (_++ [ x ]) (reverse-snoc xs y)

reverse-reverse : (xs : List A) → reverse (reverse xs) ≡ xs
reverse-reverse [] = refl
reverse-reverse (x :: xs) = 
  reverse (reverse (x :: xs)) ≡⟨ reverse-snoc (reverse xs) x ⟩
  x :: reverse (reverse xs)   ≡⟨ ap (x ::_) (reverse-reverse xs) ⟩
  x :: xs ∎

isProp-≡List : isSet A → (xs ys : List A) → isProp (xs ≡List ys)
isProp-≡List sA [] [] = isProp-⊤
isProp-≡List sA [] (y :: ys) = isProp-∅
isProp-≡List sA (x :: xs) [] = isProp-∅
isProp-≡List sA (x :: xs) (y :: ys) = isProp-× (sA x y) (isProp-≡List sA xs ys)

isSet-List : isSet A → isSet (List A)
isSet-List sA xs ys = isProp-equiv (≡≃≡List xs ys) (isProp-≡List sA xs ys)

multitilt : (xs ys zs : List A) → FQ⟨ xs ++ reverse zs , ys ⟩ ≡ FQ⟨ xs , ys ++ zs ⟩
multitilt xs ys [] = λ i → FQ⟨ (++-unit-r xs i) , (sym (++-unit-r ys) i) ⟩
multitilt xs ys (z :: zs) =
  FQ⟨ xs ++ reverse (z :: zs) , ys ⟩     ≡⟨ ap (λ ws → FQ⟨ ws , ys ⟩) (sym (++-assoc xs (reverse zs) [ z ])) ⟩
  FQ⟨ (xs ++ reverse zs) ++ [ z ] , ys ⟩ ≡⟨ tilt (xs ++ reverse zs) ys z ⟩
  FQ⟨ xs ++ reverse zs , ys ++ [ z ] ⟩   ≡⟨ multitilt xs (ys ++ [ z ]) zs ⟩
  FQ⟨ xs , (ys ++ [ z ]) ++ zs ⟩         ≡⟨ ap (λ ws → FQ⟨ xs , ws ⟩) (++-assoc ys [ z ] zs) ⟩
  FQ⟨ xs , ys ++ z :: zs ⟩               ∎

deqʳ-flush : List A → Maybe (FastQueue A × A)
deqʳ-flush [] = inl tt
deqʳ-flush (x :: xs) = inr (FQ⟨ [] , xs ⟩ , x)

deqᶠ : isSet A → FastQueue A → Maybe (FastQueue A × A)
deqᶠ sA FQ⟨ xs , [] ⟩ = deqʳ-flush (reverse xs)
deqᶠ sA FQ⟨ xs , y :: ys ⟩ = inr (FQ⟨ xs , ys ⟩ , y)
deqᶠ sA (tilt xs [] z i) = path i
  where
  path = deqʳ-flush (reverse (xs ++ [ z ]))              ≡⟨ ap deqʳ-flush (reverse-++ xs [ z ]) ⟩
         inr (FQ⟨ [] , [] ++ reverse xs ⟩ , z)           ≡⟨ ap (λ q → inr (q , z)) (sym (multitilt [] [] (reverse xs))) ⟩
         inr (FQ⟨ [] ++ reverse (reverse xs) , [] ⟩ , z) ≡⟨ ap (λ ys → inr (FQ⟨ ys , [] ⟩ , z)) (reverse-reverse xs) ⟩
         inr (FQ⟨ xs , [] ⟩ , z)                         ∎
deqᶠ sA (tilt xs (y :: ys) z i) = inr (tilt xs ys z i , y)
deqᶠ sA (trunc q q' α β i j) = isSet-⊎ isSet-⊤ (isSet-× trunc sA) (deqᶠ sA q) (deqᶠ sA q') (λ k → deqᶠ sA (α k)) (λ k → deqᶠ sA (β k)) i j

FastQueue-model : (A : Type) → isSet A → Type-with ℓ-zero (Queue-Str A)
FastQueue-model A sA .type = FastQueue A 
FastQueue-model A sA .str = empᶠ , enqᶠ , deqᶠ sA

-- mvrnote: rename to slow→fast etc or something
quot : {A : Type} → SlowQueue A → FastQueue A
quot xs = FQ⟨ xs , [] ⟩

eval : {A : Type} → isSet A → FastQueue A → SlowQueue A
eval sA FQ⟨ xs , ys ⟩ = xs ++ reverse ys
eval sA (tilt xs ys z i) = path i -- mvrnote: cleanup into equational reasoning
  where
  path : (xs ++ [ z ]) ++ reverse ys ≡ xs ++ reverse (ys ++ [ z ])
  path =
    ++-assoc xs [ z ] (reverse ys)
    ∙ ap (_++_ xs) (sym (reverse-++ ys [ z ]))
eval sA (trunc q q' α β i j) = isSet-List sA (eval sA q) (eval sA q') (λ k → eval sA (α k)) (λ k → eval sA (β k)) i j

quot∘eval : {A : Type} → (sA : isSet A) → isRetract (eval {A = A} sA) quot
quot∘eval sA FQ⟨ xs , ys ⟩ = multitilt xs [] ys
quot∘eval sA (tilt xs ys z i) j =
  isSet→Square trunc
  (λ i → quot (eval sA (tilt xs ys z i)))
  (tilt xs ys z)
  (multitilt (xs ++ [ z ]) [] ys)
  (multitilt xs [] (ys ++ [ z ]))
  i j
quot∘eval sA (trunc q q' α β i j) =
  toPathP 
  {A = λ i → PathP (λ j → quot (eval sA (trunc q q' α β i j)) ≡ trunc q q' α β i j) (quot∘eval sA q) (quot∘eval sA q')}
  {a₀ = λ k → quot∘eval sA (α k)}
  {a₁ = λ k → quot∘eval sA (β k)}
  (isProp-equiv (PathP≃Path _) (isProp→isSet (trunc (quot (eval sA q')) q') _ _) _ _)
  i j

eval∘quot : {A : Type} → (sA : isSet A) → isSection (eval {A = A} sA) quot
eval∘quot sA = ++-unit-r

quotEquiv : isSet A → SlowQueue A ≃ FastQueue A
quotEquiv sA = inv→equiv quot (eval sA) (quot∘eval sA) (eval∘quot sA)

mvrnote: Now if you have any sense, you are dreading the prospect of coming up with the notion of structured equivalence for Queue-Str and proving that it is univalent.

Structure, Compositionally

mvrnote: prose

record UnivalentNotion (ℓ ℓ' ℓ'' : Level) : Type (ℓ-suc (ℓ-max ℓ (ℓ-max ℓ' ℓ''))) where
  constructor univalentNotionData
  field
    notion : StrNotion ℓ ℓ' -- "structureFor"?
    equivNotion : StrEquivNotion notion ℓ'' -- "isStructurePreserving"
    univalenceNotion : StrNotion-isUnivalent notion equivNotion -- "isUnivalent"

open UnivalentNotion

Constant-UStr : (A : Type ℓ') → UnivalentNotion ℓ ℓ' ℓ'
Constant-UStr A .notion _ = A
Constant-UStr A .equivNotion X₁ X₂ _ = X₁ .str ≡ X₂ .str
Constant-UStr A .univalenceNotion e = idEquiv _

Pointed-UStr : UnivalentNotion ℓ ℓ ℓ
Pointed-UStr .notion X = X
Pointed-UStr .equivNotion A B f = f .map (str A) ≡ str B
Pointed-UStr .univalenceNotion f = Path≃ua-PathP f

-- mvrnote: projection helper functions?
Product-UStr : (S₁ : UnivalentNotion ℓ ℓ₁ ℓ₁') → (S₂ : UnivalentNotion ℓ ℓ₂ ℓ₂') → UnivalentNotion ℓ (ℓ-max ℓ₁ ℓ₂) (ℓ-max ℓ₁' ℓ₂')
Product-UStr S₁ S₂ .notion X = S₁ .notion X × S₂ .notion X
Product-UStr S₁ S₂ .equivNotion X₁ X₂ f = (S₁ .equivNotion (Type-with-data (X₁ .type) (X₁ .str .fst)) (Type-with-data (X₂ .type) (X₂ .str .fst)) f) × (S₂ .equivNotion (Type-with-data (X₁ .type) (X₁ .str .snd)) (Type-with-data (X₂ .type) (X₂ .str .snd)) f)
Product-UStr S₁ S₂ .univalenceNotion e = ΣPath≃PathΣ ∘e (×-map-≃ (S₁ .univalenceNotion e) (S₂ .univalenceNotion e))

Function-UStr : (S : UnivalentNotion ℓ ℓ₁ ℓ₁') → (T : UnivalentNotion ℓ ℓ₂ ℓ₂') → UnivalentNotion ℓ (ℓ-max ℓ₁ ℓ₂) (ℓ-max (ℓ-max ℓ₁ ℓ₁') ℓ₂')
Function-UStr S T .notion X = S .notion X → T .notion X
Function-UStr S T .equivNotion X₁ X₂ e =  (s₁ : S .notion (X₁ .type)) (s₂ : S .notion (X₂ .type)) → S .equivNotion (Type-with-data (X₁ .type) s₁) (Type-with-data (X₂ .type) s₂)  e → T .equivNotion (Type-with-data (X₁ .type) (X₁ .str s₁)) (Type-with-data (X₂ .type) (X₂ .str s₂)) e
Function-UStr S T .univalenceNotion e = funextP-ump-≃ ∘e Π-map-cod≃ (λ s → Π-map-cod≃ (λ t → →-map-≃ (invEquiv (S .univalenceNotion e)) (T .univalenceNotion e)))

Axioms-Str : {ℓa : Level} → (S : UnivalentNotion ℓ ℓ' ℓ'') → (axioms : (X : Type ℓ) → S .notion X → Type ℓa) → (axioms-are-Props : (X : Type ℓ) (s : S .notion X) → isProp (axioms X s))→ UnivalentNotion ℓ (ℓ-max ℓ' ℓa) ℓ''
Axioms-Str S ax isP .notion X = Σ[ s ∈ S .notion X ] (ax X s)
Axioms-Str S ax isP .equivNotion X₁ X₂ e = S .equivNotion (Type-with-data (X₁ .type) (X₁ .str .fst)) (Type-with-data (X₂ .type) (X₂ .str .fst)) e
Axioms-Str S ax isP .univalenceNotion {X₁} {X₂} e =
  S .equivNotion (Type-with-data (X₁ .type) (X₁ .str .fst)) (Type-with-data (X₂ .type) (X₂ .str .fst)) e
    ≃⟨ S .univalenceNotion e ⟩
  PathP (λ i → S .notion (ua e i)) (X₁ .str .fst) (X₂ .str .fst)
    ≃⟨ invEquiv (Σ-fst-≃ λ _ → isContr-retract (equiv→retract (PathP≃Path _)) (isProp→isContr≡ (isP _ _) _ _)) ⟩
  Σ[ p ∈ PathP (λ i → S .notion (ua e i)) (X₁ .str .fst) (X₂ .str .fst) ] PathP (λ i → ax (ua e i) (p i)) (X₁ .str .snd) (X₂ .str .snd)
    ≃⟨ ΣPath≃PathΣ ⟩
  PathP (λ i → Axioms-Str S ax isP .notion (ua e i)) (X₁ .str .fst , X₁ .str .snd) (X₂ .str .fst , X₂ .str .snd)
    ∎e

mvrnote: Re-do magma

Let’s reconstruct the Magma example using these new combinators.

Magma-Strᵥ₂ : UnivalentNotion ℓ ℓ ℓ
Magma-Strᵥ₂ = Function-UStr Pointed-UStr (Function-UStr Pointed-UStr Pointed-UStr)

Magmaᵥ₂ : (ℓ : Level) → Type (ℓ-suc ℓ)
Magmaᵥ₂ ℓ = Type-with ℓ (Magma-Strᵥ₂ .notion)

That was certainly much less work, but did we get the right thing out? Not quite. The structure itself is correct:

_ = λ {ℓ : Level} 
  → test-identical
    (Magma-Str {ℓ})
    (Magma-Strᵥ₂ {ℓ} .notion)

But the notion of homomorphism is not, instead of reconstructing isMagmaHom, instead we get the following equivalent but more annoying type.

isMagmaHomᵥ₂ : (A B : Magmaᵥ₂ ℓ) → (A .type → B .type) → Type ℓ
isMagmaHomᵥ₂ A B f
  = (a₁ : A .type) → (b₁ : B .type) → f a₁ ≡ b₁
  → (a₂ : A .type) → (b₂ : B .type) → f a₂ ≡ b₂
  → f (a₁ ·A a₂) ≡ b₁ ·B b₂
  where _·A_ = A .str
        _·B_ = B .str
  
_ = λ {ℓ : Level} (A B : Type-with ℓ (Magma-Strᵥ₂ .notion)) (e : A .type ≃ B .type)
  → test-identical 
    (Magma-Strᵥ₂ .equivNotion A B e) 
    (isMagmaHomᵥ₂ A B (e .map))

Transport Structures

Let’s spend some time trying to work around this.

record TransportNotion (ℓ ℓ' : Level) : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  constructor univalentNotionData
  field
    notion : StrNotion ℓ ℓ'
    equivAction : {X Y : Type ℓ} → X ≃ Y → notion X ≃ notion Y
    transportStr : {X Y : Type ℓ} (e : X ≃ Y) (s : notion X) → equivAction e .map s ≡ subst notion (ua e) s
open TransportNotion

TransportNotion→UnivalentNotion : TransportNotion ℓ ℓ' → UnivalentNotion ℓ ℓ' ℓ'
TransportNotion→UnivalentNotion T .notion = T .notion
TransportNotion→UnivalentNotion T .equivNotion X Y e = T .equivAction e .map (X .str) ≡ (Y .str)
TransportNotion→UnivalentNotion T .univalenceNotion {X} {Y} e =
  T .equivAction e .map (X .str) ≡ (Y .str)
    ≃⟨ path→equiv (ap (_≡ (Y .str)) (T .transportStr e (X .str))) ⟩
  subst (T .notion) (ua e) (X .str) ≡ (Y .str)
    ≃⟨ invEquiv (PathP≃Path _) ⟩
  PathP (λ i → T .notion (ua e i)) (X .str) (Y .str)
  ∎e

Constant-TrStr : (A : Type ℓ') → TransportNotion ℓ ℓ'
Constant-TrStr A .notion _ = A
Constant-TrStr A .equivAction _ = idEquiv _
Constant-TrStr A .transportStr e _ = sym (transport-refl _)

Pointed-TrStr : TransportNotion ℓ ℓ
Pointed-TrStr .notion X = X
Pointed-TrStr .equivAction e = e
Pointed-TrStr .transportStr e _ = sym (transport-refl _)

Product-TrStr : (S₁ : TransportNotion ℓ ℓ₁) → (S₂ : TransportNotion ℓ ℓ₂) → TransportNotion ℓ (ℓ-max ℓ₁ ℓ₂)
Product-TrStr S₁ S₂ .notion X = S₁ .notion X × S₂ .notion X
Product-TrStr S₁ S₂ .equivAction e = ×-map-≃ (S₁ .equivAction e) (S₂ .equivAction e)
Product-TrStr S₁ S₂ .transportStr e (s₁ , s₂) i = (S₁ .transportStr e s₁ i , S₂ .transportStr e s₂ i)

Function-UStr+ : (S : TransportNotion ℓ ℓ₁) → (T : UnivalentNotion ℓ ℓ₂ ℓ₂') → UnivalentNotion ℓ (ℓ-max ℓ₁ ℓ₂) (ℓ-max ℓ₁ ℓ₂')
Function-UStr+ S T .notion X = S .notion X → T .notion X
Function-UStr+ S T .equivNotion X Y e =
   (s : S .notion (X .type)) → T .equivNotion (Type-with-data (X .type) (X .str s)) (Type-with-data (Y .type) (Y .str (S .equivAction e .map s))) e
Function-UStr+ S T .univalenceNotion {X} {Y} e =
  ((x : S .notion (X .type)) → T .equivNotion (Type-with-data (X .type) (X .str x)) (Type-with-data (Y .type) (Y .str (S .equivAction e .map x))) e)
    ≃⟨ Π-map-cod≃ (λ x → T .univalenceNotion e) ⟩
  ((s : S .notion (X .type)) → PathP (λ i → T .notion (ua e i)) (X .str s) (Y .str (S .equivAction e .map s)))
    ≃⟨ path→equiv (λ i → ((s : S .notion (X .type)) → PathP (λ i → T .notion (ua e i)) (X .str s) (Y .str (S .transportStr e s i)))) ⟩
  ((s : S .notion (X .type)) → PathP (λ i → T .notion (ua e i)) (X .str s) (Y .str (subst (S .notion) (ua e) s)))
    ≃⟨ Π-map-cod≃ (λ _ → path→equiv (PathP≡Path' _ _ _) ) ⟩
  ((x : S .notion (X .type)) → X .str x ≡ transport (λ i → T .notion (ua e (~ i))) (Y .str (subst (S .notion) (ua e) x)))
    ≃⟨ funext-≃ ⟩
  X .str ≡ (λ z → transport (λ i → T .notion (ua e (~ i))) (Y .str (subst (S .notion) (ua e) z)))
    ≃⟨ invEquiv (path→equiv (PathP≡Path' _ (X .str) (Y .str)))  ⟩
  PathP (λ i → S .notion (ua e i) → T .notion (ua e i)) (X .str) (Y .str)
    ∎e

Magma-Strᵥ₃ : UnivalentNotion ℓ ℓ ℓ
Magma-Strᵥ₃ = Function-UStr+ Pointed-TrStr (Function-UStr+ Pointed-TrStr Pointed-UStr)

_ = λ (ℓ : Level) (A B : Type-with ℓ Magma-Str) (e : A .type ≃ B .type)
  → test-identical 
    (Magma-Strᵥ₃ .equivNotion A B e) 
    (isMagmaHom A B (e .map))

Queues again

Maybe-Str : (S : Type ℓ → Type ℓ₁) → Type ℓ → Type ℓ₁
Maybe-Str S X = Maybe (S X)

Maybe-TrStr : TransportNotion ℓ ℓ' → TransportNotion ℓ ℓ'
Maybe-TrStr S .notion X = Maybe (S .notion X)
Maybe-TrStr S .equivAction e = ⊎-map-≃ (idEquiv ⊤) (S .equivAction e)
Maybe-TrStr S .transportStr e (inl x) = refl
Maybe-TrStr S .transportStr e (inr x) = ap inr (S .transportStr e x)

Queue-UStr : (A : Type) → UnivalentNotion ℓ ℓ ℓ
Queue-UStr A = Product-UStr
  Pointed-UStr
  (Product-UStr (Function-UStr+ (Constant-TrStr A) (Function-UStr+ Pointed-TrStr Pointed-UStr))
                          (Function-UStr+ Pointed-TrStr (TransportNotion→UnivalentNotion (Maybe-TrStr (Product-TrStr Pointed-TrStr (Constant-TrStr A))))))

deqMap-∘ : {B C D : Type ℓ}
 (g : C → D) (f : B → C)
 → ∀ r → deqMap {A = A} g (deqMap f r) ≡ deqMap (g ∘ f) r
deqMap-∘ g f (inl _) = refl
deqMap-∘ g f (inr (b , a)) = refl


-- Now it only remains to prove that this is an equivalence of queue structures
quot∘emp : quot {A = A} empˢ ≡ empᶠ
quot∘emp = refl

quot∘enq : (x : A) → (xs : SlowQueue A) → quot (enqˢ x xs) ≡ enqᶠ x (quot xs)
quot∘enq x xs = refl

quot∘deq : (sA : isSet A) → (xs : SlowQueue A) → deqMap quot (deqˢ xs) ≡ deqᶠ sA (quot xs)
quot∘deq sA [] = refl
quot∘deq sA (x :: []) = refl
quot∘deq sA (x :: x' :: xs) =
  deqMap-∘ quot (enqˢ x) (deqˢ (x' :: xs))
  ∙ sym (deqMap-∘ (enqᶠ x) quot (deqˢ (x' :: xs)))
  ∙ ap (deqMap (enqᶠ x)) (quot∘deq sA (x' :: xs))
  ∙ lemma x x' (reverse xs)
  where
  lemma : ∀ x x' ys → deqMap (enqᶠ x) (deqʳ-flush (ys ++ [ x' ])) ≡ deqʳ-flush ((ys ++ [ x' ]) ++ [ x ])
  lemma x x' [] i        = inr (tilt [] [] x i , x')
  lemma x x' (y :: ys) i = inr (tilt [] (ys ++ [ x' ]) x i , y)

quotEquivHasQueueEquivStr : (sA : isSet A) → Queue-UStr A .equivNotion (SlowQueue-model A) (FastQueue-model A sA) (quotEquiv sA)
quotEquivHasQueueEquivStr sA = quot∘emp , quot∘enq , quot∘deq sA

Let’s get some payoff. There are lots of things we might like to be true about queues, and they are easy to prove about our SlowQueue.

mvrnote: Project ideas?

References and Further Reading

mvrnote: https://1lab.dev/1Lab.Univalence.SIP.html Internalizing Representation Independence with Univalence https://arxiv.org/abs/2009.05547 https://github.com/agda/cubical/blob/master/Cubical/Data/BinNat/BinNat.agda https://staff.math.su.se/anders.mortberg/slides/PalmgrenMemorial2020.pdf https://dl.acm.org/doi/abs/10.1145/3373718.3394755

Old

mvrnote: to be sorted/deleted

We will now revisit the previous simplified monoid structure to show how we can construct it as a univalent structure.

Notice how we only used the raw monoid structure to define the univalent structure above! We did that because there is a need to carefully separate the raw structure of a type from its axioms. The reason for that is that we need to show that every axiom on a structure is also a proposition.

We define an axiom structure as follows:

We can now use our new axiom structure to extend the raw monoid structure to a full monoid with all of its axioms.

-- RawMonoidStructure : StrNotion ℓ ℓ
-- RawMonoidStructure = ProductStr PointedStr (FunctionStr PointedStr (FunctionStr PointedStr PointedStr))

-- RawMonoidEquivStr : StrEquivNotion RawMonoidStructure ℓ
-- RawMonoidEquivStr = ProductEquivStr PointedEquivStr (FunctionEquivStr PointedEquivStr (FunctionEquivStr PointedEquivStr PointedEquivStr))

-- RawMonoid : (ℓ : Level) → Type (ℓ-suc ℓ)
-- RawMonoid ℓ = Type-with ℓ RawMonoidStructure


-- ≃[Monoid]-univalent : StrNotion-isUnivalent (RawMonoidStructure {ℓ}) (RawMonoidEquivStr {ℓ})
-- ≃[Monoid]-univalent = productStrNotion-isUnivalent
--   {S₁ = PointedStr} pointedStrNotion-isUnivalent
--   {S₂ = FunctionStr PointedStr (FunctionStr PointedStr PointedStr)} (functionStrNotion-isUnivalent {T = FunctionStr PointedStr PointedStr} pointedStrNotion-isUnivalent (functionStrNotion-isUnivalent {T = PointedStr} pointedStrNotion-isUnivalent pointedStrNotion-isUnivalent))

-- RawMonoidEquivStr : StrEquivNotion RawMonoidStructure ℓ
-- RawMonoidEquivStr (A , (εA , _·A_)) (B , (εB , _·B_)) (φ , t) =
--   (φ εA ≡ εB) × ((a a' : A) → φ (a ·A a') ≡ φ a ·B φ a')

-- MonoidAxioms : (A : Type ℓ) → RawMonoidStructure A → Type ℓ
-- MonoidAxioms A (e , _·_) =
--     isSet A
--   × ((x y z : A) → x · (y · z) ≡ (x · y) · z)
--   × ((x : A) → x · e ≡ x)
--   × ((x : A) → e · x ≡ x)

-- MonoidStructure : StrNotion ℓ ℓ
-- MonoidStructure = AxiomsStr RawMonoidStructure MonoidAxioms

-- Monoid : (ℓ : Level) → Type (ℓ-suc ℓ)
-- Monoid ℓ = Type-with ℓ MonoidStructure

-- MonoidEquivStr : StrEquivNotion MonoidStructure ℓ
-- MonoidEquivStr = AxiomsEquivStr RawMonoidEquivStr MonoidAxioms

-- isPropMonoidAxioms : (M : Type ℓ) (s : RawMonoidStructure M) → isProp (MonoidAxioms M s)
-- isPropMonoidAxioms M (e , _·_) = isPropΣ isProp-isSet λ s →
--   isProp× (isPropΠ λ _ → isPropΠ λ _ → isPropΠ λ _ → s _ _) (
--   isProp× (isPropΠ λ _ → s _ _)
--           (isPropΠ λ _ → s _ _))
  -- mvrnote: Or directly, eg
  -- λ x y i → (λ x₁ y₁ z → s _ _ (fst x x₁ y₁ z) (fst y x₁ y₁ z) i) , ({!!} , {!!})

-- monoidStrNotion-isUnivalent : ∀ {ℓ} → StrNotion-isUnivalent (MonoidStructure {ℓ}) (MonoidEquivStr {ℓ})
-- monoidStrNotion-isUnivalent = axiomsStrNotion-isUnivalent _ isPropMonoidAxioms rawMonoidStrNotion-isUnivalent

Introduction to Homotopy Type Theory in Cubical Agda