module 1Lab.Univalence.SIP where

# Structure Identity Principle🔗

In mathematics in general, it’s often *notationally* helpful
to identify isomorphic *structures* (e.g.: groups) in a proof.
However, when this mathematics is done using material set theory as a
foundations, this identification is merely a shorthand — nothing
*prevents* you from distinguishing isomorphic groups in ZFC by,
for instance, asking about membership of a particular set in the
underlying set of each group.

In univalent mathematics, it’s a theorem that no family of types can
distinguish between isomorphic structures. Univalence is this statement, but for
*types*. For structures built out of types, it seems like we
would need a bit more power, but in reality, we don’t!

“Structure Identity Principle” is the name for several related theorems in Homotopy Type Theory, which generically say that “paths on a structure are isomorphisms of that structure”.

For instance, the version in the HoTT Book says that if a structure
`S`

on the objects of a univalent category
`S`

can be described in a certain way, then the category of
`S`

-structured objects of `C`

is univalent. As a
benefit, the Book version of the SIP characterises the
*homomorphisms* of `S`

-structures, not just the
*isomorphisms*. As a downside, it only applies to set-level structures.

record Structure {ℓ₁ ℓ₂} (ℓ₃ : _) (S : Type ℓ₁ → Type ℓ₂) : Type (lsuc (ℓ₁ ⊔ ℓ₃) ⊔ ℓ₂) where constructor HomT→Str field

The material on this page, especially the definition of `is-univalent`

and `is-transport-str`

, is adapted
from Internalizing
Representation Independence with Univalence. The SIP
formalised here says, very generically, that a `Structure`

is a family of types
`S : Type → Type`

, and a `type with`

structure is an
inhabitant of the `total space`

`Σ S`

.

What sets a `Structure`

apart from a type
family is a notion of *homomorphic equivalence*: Given an
equivalence of the underlying types, the predicate
`is-hom (A , x) (B , y) eqv`

should represent what it means
for `eqv`

to take the `x`

-structure on
`A`

to the `y`

-structure on `B`

.

is-hom : (A B : Σ _ S) → (A .fst ≃ B .fst) → Type ℓ₃

As a grounding example, consider equipping types with group
structure: If `(A , _⋆_)`

and `(B , _*_)`

are
types with group structure (with many fields omitted!), and
`f : A → B`

is the underlying map of an equivalence
`A ≃ B`

, then `is-hom`

would be
$\forall (x y\colon A) f(x \star y) = f(x) * f(y)$
- the “usual” definition of group homomorphism.

open Structure public Type-with : ∀ {ℓ ℓ₁ ℓ₂} {S : Type ℓ → Type ℓ₁} → Structure ℓ₂ S → Type _ Type-with {S = S} _ = Σ _ S

A structure is said to be **univalent** if a homomorphic
equivalence of structures `A`

, `B`

induces a path
of the structures, over the univalence axiom — that is, if
`is-hom`

agrees with what it means
for “S X” and “S Y” to be identified, where this identification is
dependent on one induced by univalence.

is-univalent : Structure ℓ S → Type _ is-univalent {S = S} ι = ∀ {X Y} → (f : X .fst ≃ Y .fst) → ι .is-hom X Y f ≃ PathP (λ i → S (ua f i)) (X .snd) (Y .snd)

The notation `A ≃[ σ ] B`

stands for
the type of σ-homomorphic equivalences, i.e. those equivalences of the
types underlying `A`

and `B`

that σ identifies as
being homomorphic.

_≃[_]_ : Σ _ S → Structure ℓ S → Σ _ S → Type _ A ≃[ σ ] B = Σ[ f ∈ A .fst ≃ B .fst ] (σ .is-hom A B f)

## The principle🔗

The **structure identity principle** says that, if
`S`

is a `univalent structure`

, then the
path space of `Σ S`

is equivalent to the space of
S-homomorphic equivalences of types. Again using groups as a grounding
example: identification of groups is group isomorphism.

SIP : {σ : Structure ℓ S} → is-univalent σ → {X Y : Σ _ S} → (X ≃[ σ ] Y) ≃ (X ≡ Y) SIP {S = S} {σ = σ} is-univ {X} {Y} = X ≃[ σ ] Y ≃⟨⟩ Σ[ e ∈ X .fst ≃ Y .fst ] (σ .is-hom X Y e) ≃⟨ Σ-ap (ua , univalence⁻¹) is-univ ⟩≃ Σ[ p ∈ X .fst ≡ Y .fst ] PathP (λ i → S (p i)) (X .snd) (Y .snd) ≃⟨ Iso→Equiv Σ-pathp-iso ⟩≃ (X ≡ Y) ≃∎

The proof of the `SIP`

follows essentially from
`univalence`

, and the fact that
`Σ types respect equivalences`

.
In one fell swoop, we convert from the type of homomorphic equivalences
to a dependent pair of paths. By the characterisation of `path spaces of Σ types`

, this
latter pair is equivalent to `X ≡ Y`

.

sip : {σ : Structure ℓ S} → is-univalent σ → {X Y : Σ _ S} → (X ≃[ σ ] Y) → (X ≡ Y) sip σ = SIP σ .fst

# Structure Combinators🔗

Univalent structures can be built up in an algebraic manner through
the use of *structure combinators*. These express closure of
structures under a number of type formers. For instance, if
`S`

and `T`

are univalent structures, then so is
`λ X → S X → T X`

.

The simplest case of univalent structure is the *constant
structure*, which is what you get when you equip a type
`X`

with a choice of inhabitant of some other type
`Y`

, unrelated to `X`

. Since the given function is
`f : A → B`

, it can’t act on `T`

, so the notion of
homomorphism is independent of `f`

.

Constant-str : (A : Type ℓ) → Structure {ℓ₁} ℓ (λ X → A) Constant-str T .is-hom (A , x) (B , y) f = x ≡ y Constant-str-univalent : {A : Type ℓ} → is-univalent (Constant-str {ℓ₁ = ℓ₁} A) Constant-str-univalent f = _ , id-equiv

The next simplest case is considering the identity function as a
structure. In that case, the resulting structured type is that of a
*pointed type*, whence the name `Pointed-str`

.

The name `Pointed-str`

breaks down when it
is used with some of the other combinators: A type equipped with the
`product`

of two `pointed structures`

is indeed a
“bipointed structure”, but a type equipped with `maps between`

two `pointed structures`

is a type
equipped with an endomorphism, which does not necessitate a point.

Pointed-str : Structure ℓ (λ X → X) Pointed-str .is-hom (A , x) (B , y) f = f .fst x ≡ y

This is univalent by `ua-pathp≃path`

, which says
`PathP (ua f) x y`

is equivalent to
`f .fst x ≡ y`

.

Pointed-str-univalent : is-univalent (Pointed-str {ℓ}) Pointed-str-univalent f = ua-pathp≃path _

If `S`

and `T`

are univalent structures, then
so is their pointwise product. The notion of a
`S × T`

-homomorphism is that of a function homomorphic for
both `S`

and `T`

, simultaneously:

Product-str : Structure ℓ S → Structure ℓ₂ T → Structure _ (λ X → S X × T X) Product-str S T .is-hom (A , x , y) (B , x' , y') f = S .is-hom (A , x) (B , x') f × T .is-hom (A , y) (B , y') f Product-str-univalent : {σ : Structure ℓ₁ S} {τ : Structure ℓ₂ T} → is-univalent σ → is-univalent τ → is-univalent (Product-str σ τ) Product-str-univalent {S = S} {T = T} {σ = σ} {τ} θ₁ θ₂ {X , x , y} {Y , x' , y'} f = (σ .is-hom (X , x) (Y , x') _ × τ .is-hom (X , y) (Y , y') _) ≃⟨ Σ-ap (θ₁ f) (λ _ → θ₂ f) ⟩≃ (PathP _ _ _ × PathP _ _ _) ≃⟨ Iso→Equiv Σ-pathp-iso ⟩≃ PathP (λ i → S (ua f i) × T (ua f i)) (x , y) (x' , y') ≃∎

If `S`

and `T`

are univalent structures, then
so are the families of functions between them. For reasons we’ll see
below, this is called `Str-function-str`

(a rather
redundant name!) instead of `Function-str`

.

Str-function-str : Structure ℓ₁ S → Structure ℓ₂ T → Structure _ (λ X → S X → T X) Str-function-str {S = S} σ τ .is-hom (A , f) (B , g) h = {s : S A} {t : S B} → σ .is-hom (A , s) (B , t) h → τ .is-hom (A , f s) (B , g t) h Str-function-str-univalent : {σ : Structure ℓ₁ S} {τ : Structure ℓ₂ T} → is-univalent σ → is-univalent τ → is-univalent (Str-function-str σ τ) Str-function-str-univalent {S = S} {T = T} {σ = σ} {τ} θ₁ θ₂ eqv = Π-impl-cod≃ (λ s → Π-impl-cod≃ λ t → function≃ (θ₁ eqv) (θ₂ eqv)) ∙e funext-dep≃

## Example: magmas🔗

We provide an example of applying the SIP, and the structure
combinators:
**$\infty$-magmas**.
Recall that a magma is a set equipped with a binary operation,
with no further conditions imposed. In HoTT, we can relax this even
further: An
$\infty$-magma
is a `Type`

- that is, an
$\infty$-groupoid
- equipped with a binary operation.

private binop : Type → Type binop X = X → X → X

We can impose a `Structure`

on `binop`

by applying nested `Function-str`

and `Pointed-str`

. Since this
structure is built out of structure combinators, it’s automatically
univalent:

∞-Magma : Structure lzero binop ∞-Magma = Str-function-str Pointed-str (Str-function-str Pointed-str Pointed-str) ∞-Magma-univ : is-univalent ∞-Magma ∞-Magma-univ = Str-function-str-univalent {τ = Str-function-str Pointed-str Pointed-str} Pointed-str-univalent (Str-function-str-univalent {τ = Pointed-str} Pointed-str-univalent Pointed-str-univalent)

The type of `∞-Magma`

homomorphisms generated
by this equivalence is slightly inconvenient: Instead of getting
$f (x \star y) = f x * f y$,
we get something that is parameterised over two paths:

_ : {A B : Type-with ∞-Magma} {f : A .fst ≃ B .fst} → ∞-Magma .is-hom A B f ≡ ( {s : A .fst} {t : B .fst} → f .fst s ≡ t → {x : A .fst} {y : B .fst} → f .fst x ≡ y → f .fst (A .snd s x) ≡ B .snd t y) _ = refl

This condition, although it looks a lot more complicated, is essentially the same as the standard notion:

fixup : {A B : Type-with ∞-Magma} {f : A .fst ≃ B .fst} → ((x y : A .fst) → f .fst (A .snd x y) ≡ B .snd (f .fst x) (f .fst y)) → ∞-Magma .is-hom A B f fixup {A = A} {B} {f} path {s} {t} p {s₁} {t₁} q = f .fst (A .snd s s₁) ≡⟨ path _ _ ⟩≡ B .snd (f .fst s) (f .fst s₁) ≡⟨ ap₂ (B .snd) p q ⟩≡ B .snd t t₁ ∎

As an example, we equip the type of booleans with two ∞-magma
structures, one given by conjunction, one by disjunction, and prove that
`not`

identifies them, as
∞-magmas:

Conj : Type-with ∞-Magma Conj .fst = Bool Conj .snd false false = false Conj .snd false true = false Conj .snd true false = false Conj .snd true true = true

Disj : Type-with ∞-Magma Disj .fst = Bool Disj .snd false false = false Disj .snd false true = true Disj .snd true false = true Disj .snd true true = true

I claim that `not`

is a
$\infty$-magma
isomorphism between `Conj`

and `Disj`

:

not-iso : Conj ≃[ ∞-Magma ] Disj not-iso .fst = not , not-is-equiv not-iso .snd = fixup {A = Conj} {B = Disj} {f = _ , not-is-equiv} λ where false false → refl false true → refl true false → refl true true → refl

It’s not clear that this should be the case, especially since the
case analysis obfuscates the result further. However, writing
$\land$
and
$\lor$
for the actions of `Conj`

and `Disj`

(as one should!), then we
see that `not-iso`

says exactly that

$\neg (x \land y) = \neg x \lor \neg y$

From this and the SIP we get that `Conj`

and `Disj`

are the same
$\infty$-magma:

Conj≡Disj : Conj ≡ Disj Conj≡Disj = sip ∞-Magma-univ not-iso

We have a similar phenomenon that happens with NAND and NOR:

Nand : Type-with ∞-Magma Nand .fst = Bool Nand .snd false false = true Nand .snd false true = true Nand .snd true false = true Nand .snd true true = false

Nor : Type-with ∞-Magma Nor .fst = Bool Nor .snd false false = true Nor .snd false true = false Nor .snd true false = false Nor .snd true true = false

not-iso' : Nand ≃[ ∞-Magma ] Nor not-iso' .fst = not , not-is-equiv not-iso' .snd = fixup {A = Nand} {B = Nor} {f = _ , not-is-equiv} λ where false false → refl false true → refl true false → refl true true → refl

# Transport Structures🔗

As an alternative to equipping a type family
`S : Type → Type`

with a notion of S-homomorphism, we can
equip it with a notion of *action*. Equipping a structure with a
notion of action canonically equips it with a notion of
homomorphism:

Equiv-action : (S : Type ℓ → Type ℓ₁) → Type _ Equiv-action {ℓ = ℓ} S = {X Y : Type ℓ} → (X ≃ Y) → (S X ≃ S Y) Action→Structure : {S : Type ℓ → Type ℓ₁} → Equiv-action S → Structure _ S Action→Structure act .is-hom (A , x) (B , y) f = act f .fst x ≡ y

A **transport structure** is a structure
`S : Type → Type`

with a choice of equivalence action
`α : Equiv-action S`

which agrees with the “intrinsic” notion
of equivalence action that is induced by the computation rules for
transport.

is-transport-str : {S : Type ℓ → Type ℓ₁} → Equiv-action S → Type _ is-transport-str {ℓ = ℓ} {S = S} act = {X Y : Type ℓ} (e : X ≃ Y) (s : S X) → act e .fst s ≡ subst S (ua e) s

While the above definition of `transport structure`

is natural, it can
sometimes be unwieldy to work with. Using `univalence`

, the condition for
being a transport structure can be weakened to “preserves the identity
equivalence”, with no loss of generality:

preserves-id : {S : Type ℓ → Type ℓ} → Equiv-action S → Type _ preserves-id {ℓ = ℓ} {S = S} act = {X : Type ℓ} (s : S X) → act (id , id-equiv) .fst s ≡ s

The proof is by equivalence induction: To show something about all
`Y : Type, x : X ≃ Y`

(with X fixed), it suffices to cover
the case where `Y`

is `X`

and `e`

is
the identity equivalence. This case is by the assumption that `σ preserves id`

.

preserves-id→is-transport-str : (σ : Equiv-action S) → preserves-id σ → is-transport-str σ preserves-id→is-transport-str {S = S} σ pres-id e s = EquivJ (λ _ e → σ e .fst s ≡ subst S (ua e) s) lemma' e where

Unfortunately we can not directly use the assumption that
`σ`

preserves `id`

in the proof, but it can be used as the final step in an equational
proof:

lemma' : σ (id , id-equiv) .fst s ≡ subst S (ua (id , id-equiv)) s lemma' = sym ( subst S (ua (id , id-equiv)) s ≡⟨ ap (λ p → subst S p s) ua-id-equiv ⟩≡ transport refl s ≡⟨ transport-refl _ ⟩≡ s ≡⟨ sym (pres-id s) ⟩≡ σ (id , id-equiv) .fst s ∎ )

sym-transport-str : {S : Type ℓ → Type ℓ₂} (α : Equiv-action S) (τ : is-transport-str α) {X Y : Type ℓ} (e : X ≃ Y) (t : S Y) → equiv→inverse (α e .snd) t ≡ subst S (sym (ua e)) t sym-transport-str {S = S} α τ e t = sym (transport⁻transport (ap S (ua e)) (ae.from t)) ·· sym (ap (subst S (sym (ua e))) (τ e (ae.from t))) ·· ap (subst S (sym (ua e))) (ae.ε t) where module ae = Equiv (α e)

If `S`

is a `transport structure`

, then its canonical
equipment as a `Structure`

is univalent:

is-transport→is-univalent : {S : Type ℓ → Type ℓ₁} (a : Equiv-action S) → is-transport-str a → is-univalent (Action→Structure a) is-transport→is-univalent {S = S} act is-tr {X , s} {Y , t} eqv = act eqv .fst s ≡ t ≃⟨ path→equiv (ap (_≡ t) (is-tr eqv s)) ⟩≃ subst S (ua eqv) s ≡ t ≃⟨ path→equiv (sym (PathP≡Path (λ i → S (ua eqv i)) s t)) ⟩≃ PathP (λ i → S (ua eqv i)) s t ≃∎

We can mix and match these different notions of structure at will. For example, a more convenient definition of function univalent structure uses an equivalence action on the domain:

Function-str : Equiv-action S → Structure ℓ T → Structure _ (λ X → S X → T X) Function-str {S = S} act str .is-hom (A , f) (B , g) e = (s : S A) → str .is-hom (A , f s) (B , g (act e .fst s)) e

This alternative definition of structure is univalent when
`T`

is a univalent structure and `S`

is a
transport structure:

Function-str-univalent : (α : Equiv-action S) → is-transport-str α → (τ : Structure ℓ T) → is-univalent τ → is-univalent (Function-str α τ) Function-str-univalent {S = S} {T = T} α α-tr τ τ-univ {X , f} {Y , g} eqv = ((s : S X) → τ .is-hom (X , f s) (Y , _) eqv) ≃⟨ Π-cod≃ (λ s → τ-univ eqv ∙e path→equiv (ap (PathP (λ i → T (ua eqv i)) (f s) ∘ g) (α-tr _ _))) ⟩≃ ((s : S X) → PathP (λ i → T (ua eqv i)) (f s) _) ≃⟨ (hetero-homotopy≃homotopy e⁻¹) ∙e funext-dep≃ ⟩≃ _ ≃∎

To see why `Function-str`

is more convenient
than `the previous definition`

- which
is why it gets the shorter name - it’s convenient to consider how the
`pointed structure`

acts on
equivalences: *not at all*. Recall the definition of ∞-magma
equivalence generated by `Str-function-str`

:

private _ : {A B : Type-with ∞-Magma} {f : A .fst ≃ B .fst} → ∞-Magma .is-hom A B f ≡ ( {s : A .fst} {t : B .fst} → f .fst s ≡ t → {x : A .fst} {y : B .fst} → f .fst x ≡ y → f .fst (A .snd s x) ≡ B .snd t y) _ = refl

Let’s rewrite `∞-Magma`

using `Function-str`

to see how it
compares:

∞-Magma′ : Structure lzero binop ∞-Magma′ = Function-str id (Function-str id Pointed-str) _ : {A B : Type-with ∞-Magma} {f : A .fst ≃ B .fst} → ∞-Magma′ .is-hom A B f ≡ ( (x y : A .fst) → f .fst (A .snd x y) ≡ B .snd (f .fst x) (f .fst y)) _ = refl

Much better! This gets rid of all those redundant paths that were
previously present, using the fact that `λ X → X`

*does
not need to act on equivalences*.

In general, transport structures are closed under all of the same
operations as univalent structures, which begs the question: Why mention
univalent structures at all? The reason is that a definition of
structure homomorphism is very often needed, and the data of a univalent
structure is perfect to use in the definition of `SIP`

.

##
The closure properties of transport structures are in this
`<details>`

tag to keep the length of the page shorter

Constant-action : (A : Type ℓ) → Equiv-action {ℓ = ℓ₁} (λ X → A) Constant-action A eqv = _ , id-equiv Constant-action-is-transport : {A : Type ℓ} → is-transport-str {ℓ = ℓ₁} (Constant-action A) Constant-action-is-transport f s = sym (transport-refl _) Id-action-is-transport : is-transport-str {ℓ = ℓ} {ℓ₁ = ℓ} id Id-action-is-transport f s = sym (transport-refl _) Product-action : Equiv-action S → Equiv-action T → Equiv-action (λ X → S X × T X) Product-action actx acty eqv = Σ-ap (actx eqv) λ x → acty eqv Product-action-is-transport : {α : Equiv-action S} {β : Equiv-action T} → is-transport-str α → is-transport-str β → is-transport-str (Product-action α β) Product-action-is-transport α-tr β-tr e s = Σ-pathp (α-tr e (s .fst)) (β-tr e (s .snd)) Function-action : Equiv-action S → Equiv-action T → Equiv-action (λ X → S X → T X) Function-action actx acty eqv = function≃ (actx eqv) (acty eqv) Function-action-is-transport : {α : Equiv-action S} {β : Equiv-action T} → is-transport-str α → is-transport-str β → is-transport-str (Function-action α β) Function-action-is-transport {S = S} {α = α} {β = β} α-tr β-tr eqv f = funext λ x → ap (β eqv .fst ∘ f) (sym-transport-str α α-tr eqv x) ∙ β-tr eqv (f (subst S (sym (ua eqv)) x))

# Adding Axioms🔗

Most mathematical objects of interest aren’t merely sets with
structure. More often, the objects we’re interested in have
*stuff* (the underlying type), *structure* (such as a
`SNS`

), and *properties* - for
instance, equations imposed on the structure. A concrete example may
help:

A

**pointed $\infty$-magma**is a pointed type equipped with a binary operation;A

**monoid**is a pointed $\infty$-magma with additional data witnessing that a) the type is a set; b) the operation is associative; and c) the point acts as a left- and right- identity for the operation.

Fortunately, the SIP again applies here: If you augment a standard
notion of structure with *axioms*, then identification of
structures with axioms is still isomorphism of the underlying
structures. For this, we require that the axioms are valued in propositions.

module _ (σ : Structure ℓ S) (axioms : (X : _) → S X → Type ℓ₃) where

First, the notion of structure that you get is just a lifting of the
underlying structure `σ`

to ignore the witnesses for the
axioms:

Axiom-str : Structure ℓ (λ X → Σ[ s ∈ S X ] (axioms X s)) Axiom-str .is-hom (A , s , a) (B , t , b) f = σ .is-hom (A , s) (B , t) f

Then, if the axioms are propositional, a calculation by equivalence
reasoning concludes what we wanted: `Axiom-str`

is univalent.

module _ (univ : is-univalent σ) (axioms-prop : ∀ {X} {s} → is-prop (axioms X s)) where Axiom-str-univalent : is-univalent Axiom-str Axiom-str-univalent {X = A , s , a} {Y = B , t , b} f = σ .is-hom (A , s) (B , t) f ≃⟨ univ f ⟩≃ PathP (λ i → S (ua f i)) s t ≃⟨ Σ-contract (λ x → PathP-is-hlevel 0 (contr b (axioms-prop b))) e⁻¹ ⟩≃ Σ[ p ∈ PathP (λ i → S (ua f i)) s t ] PathP (λ i → axioms (ua f i) (p i)) a b ≃⟨ Iso→Equiv Σ-pathp-iso ⟩≃ _ ≃∎

Here, another facet of the trade-offs between transport and univalent
structures make themselves clear: It’s possible (albeit less than
straightforward) to add axioms to a *univalent* structure, but
without imposing further structure on the axioms themselves, it is not
clear how to add axioms to a *transport* structure.

Regardless, a very useful consequence of the SIP is that axioms can
be lifted from equivalent underlying structures. For instance:
$\mathbb{N}$
can be defined as both unary numbers (the construction of `Nat`

), or as binary numbers. If you prove
that `Nat`

is a monoid, and
`Nat ≃ Bin`

as pointed ∞-magmas, then `Bin`

inherits the monoid structure.

transfer-axioms : {σ : Structure ℓ S} {univ : is-univalent σ} {axioms : (X : _) → S X → Type ℓ₃} → (A : Type-with (Axiom-str σ axioms)) (B : Type-with σ) → (A .fst , A .snd .fst) ≃[ σ ] B → axioms (B .fst) (B .snd) transfer-axioms {univ = univ} {axioms = axioms} A B eqv = subst (λ { (x , y) → axioms x y }) (sip univ eqv) (A .snd .snd)

# A Language for Structures🔗

The structure combinators can be abstracted away into a
*language* for defining structures. A `Str-term`

describes a structure,
that may be interpreted into a family of types, and defines both
transport and univalent structures.

data Str-term ℓ : (ℓ₁ : Level) → (Type ℓ → Type ℓ₁) → Typeω where s-const : ∀ {ℓ₁} (A : Type ℓ₁) → Str-term ℓ ℓ₁ (λ X → A) s∙ : Str-term ℓ ℓ (λ X → X) _s→_ : ∀ {ℓ₁ ℓ₂} {S} {T} → Str-term ℓ ℓ₁ S → Str-term ℓ ℓ₂ T → Str-term ℓ (ℓ₁ ⊔ ℓ₂) (λ X → S X → T X) _s×_ : ∀ {ℓ₁ ℓ₂} {S} {T} → Str-term ℓ ℓ₁ S → Str-term ℓ ℓ₂ T → Str-term ℓ (ℓ₁ ⊔ ℓ₂) (λ X → S X × T X) infixr 30 _s→_ _s×_

Since each term of the language corresponds to one of the combinators
for building univalent structures, a pair of *mutually recursive*
functions lets us derive a `Structure`

and an `action on equivalences`

from a
term, at the same time.

Term→structure : (s : Str-term ℓ ℓ₁ S) → Structure ℓ₁ S Term→action : (s : Str-term ℓ ℓ₁ S) → Equiv-action S Term→structure (s-const x) = Constant-str x Term→structure s∙ = Pointed-str Term→structure (s s→ s₁) = Function-str (Term→action s) (Term→structure s₁) Term→structure (s s× s₁) = Product-str (Term→structure s) (Term→structure s₁) Term→action (s-const x₁) x = _ , id-equiv Term→action s∙ x = x Term→action (s s→ s₁) = Function-action (Term→action s) (Term→action s₁) Term→action (s s× s₁) = Product-action (Term→action s) (Term→action s₁)

The reason for this mutual recursion is the same reason that
transport structures are considered in the first place: `Function-str`

gives much better
results for the definition of homomorphism than can be gotten directly
using `Str-function-str`

. As an example
of using the language, and the generated definition of homomorphism,
consider pointed ∞-magmas:

private Pointed∞Magma : Structure lzero _ Pointed∞Magma = Term→structure (s∙ s× (s∙ s→ (s∙ s→ s∙))) _ : {A B : Type-with Pointed∞Magma} {f : A .fst ≃ B .fst} → Pointed∞Magma .is-hom A B f ≡ ( (f .fst (A .snd .fst) ≡ B .snd .fst) × ((x y : A .fst) → f .fst (A .snd .snd x y) ≡ B .snd .snd (f .fst x) (f .fst y))) _ = refl

A homomorphic equivalence of pointed ∞-magmas is an equivalence of
their underlying types that preserves the basepoint and is homomorphic
over the operation. The use of `Term→action`

in contravariant
positions is responsible for making sure the computed `is-hom`

doesn’t have any redundant
paths in argument positions.

A mutually *inductive* argument proves that `Term→action`

produces transport
structures, and that `Term→structure`

produces
univalent structures. At every case, the proof is by appeal to a lemma
that was proved above.

Term→structure-univalent : (s : Str-term ℓ ℓ₁ S) → is-univalent (Term→structure s) Term→action-is-transport : (s : Str-term ℓ ℓ₁ S) → is-transport-str (Term→action s) Term→structure-univalent (s-const x) = Constant-str-univalent Term→structure-univalent s∙ = Pointed-str-univalent Term→structure-univalent (s s→ s₁) = Function-str-univalent (Term→action s) (Term→action-is-transport s) (Term→structure s₁) (Term→structure-univalent s₁) Term→structure-univalent (s s× s₁) = Product-str-univalent {σ = Term→structure s} {τ = Term→structure s₁} (Term→structure-univalent s) (Term→structure-univalent s₁) Term→action-is-transport (s-const x) = Constant-action-is-transport Term→action-is-transport s∙ = Id-action-is-transport Term→action-is-transport (s s→ s₁) = Function-action-is-transport {α = Term→action s} {β = Term→action s₁} (Term→action-is-transport s) (Term→action-is-transport s₁) Term→action-is-transport (s s× s₁) = Product-action-is-transport {α = Term→action s} {β = Term→action s₁} (Term→action-is-transport s) (Term→action-is-transport s₁)

## Descriptions of Structures🔗

To make convenient descriptions of structures-with-axioms, we
introduce a record type, `Str-desc`

, which packages together
the structure term and the properties that are imposed:

record Str-desc ℓ ℓ₁ S ax : Typeω where field descriptor : Str-term ℓ ℓ₁ S axioms : ∀ X → S X → Type ax axioms-prop : ∀ X s → is-prop (axioms X s) Desc→Fam : ∀ {ax} → Str-desc ℓ ℓ₁ S ax → Type ℓ → Type (ℓ₁ ⊔ ax) Desc→Fam {S = S} desc X = Σ[ S ∈ S X ] (desc .Str-desc.axioms _ S) Desc→Str : ∀ {ax} → (S : Str-desc ℓ ℓ₁ S ax) → Structure _ (Desc→Fam S) Desc→Str desc = Axiom-str (Term→structure descriptor) axioms where open Str-desc desc Desc→is-univalent : ∀ {ax} → (S : Str-desc ℓ ℓ₁ S ax) → is-univalent (Desc→Str S) Desc→is-univalent desc = Axiom-str-univalent (Term→structure descriptor) axioms (Term→structure-univalent descriptor) (λ {X} {s} → axioms-prop X s) where open Str-desc desc