Thierry Coquand and I have proved that, for a large class of algebraic structures, isomorphism implies equality (assuming univalence).
A class of algebraic structures
Structures in this class consist of a type, some operations on this type, and propositional axioms that can refer to operations and other axioms.
N-ary functions are defined in the following way (using Agda notation):
_^_⟶_ : Set → ℕ → Set → Set A ^ zero ⟶ B = B A ^ suc n ⟶ B = A → (A ^ n ⟶ B)
The class of algebraic structures is then defined in two steps. In the first step codes for structures, Structure, are defined mutually with a decoding function, ⟦_⟧, using induction-recursion:
mutual
infixl 5 _+operator_ _+axiom_
data Structure : Set₁ where
empty : Structure
-- N-ary functions.
_+operator_ : Structure → (n : ℕ) → Structure
-- Arbitrary propositional axioms.
_+axiom_ : (s : Structure)
(P : Σ (∀ A → ⟦ s ⟧ A → Set) λ P →
∀ A s → Propositional (P A s)) →
Structure
⟦_⟧ : Structure → Set → Set₁
⟦ empty ⟧ A = ↑ _ ⊤
⟦ s +operator n ⟧ A = ⟦ s ⟧ A × (A ^ n ⟶ A)
⟦ s +axiom (P , P-prop) ⟧ A = Σ (⟦ s ⟧ A) (P A)
Here Propositional B means that B is of h-level 1, and ↑ _ ⊤ stands for the unit type, lifted to Set₁.
In the second step the decoding function’s Set argument is instantiated:
⟪_⟫ : Structure → Set₁ ⟪ s ⟫ = Σ Set ⟦ s ⟧
As a simple example of an algebraic structure in this class we can define semigroups (over sets). The definition uses function extensionality to prove that the axioms are propositional. Note that the first axiom states that the underlying type is a set. This assumption is used to prove that the other axiom is propositional:
semigroup :
({A : Set} {B : A → Set} → Extensionality A B) →
Structure
semigroup ext =
empty
+axiom
( (λ A _ → Is-set A)
, is-set-prop
)
+operator 2
+axiom
( (λ { _ (_ , _∙_) →
∀ x y z → x ∙ (y ∙ z) ≡ (x ∙ y) ∙ z })
, assoc-prop
)
where
is-set-prop = …
assoc-prop = λ { _ ((_ , A-set) , _) → … }
Semigroup :
({A : Set} {B : A → Set} → Extensionality A B) →
Set₁
Semigroup ext = ⟪ semigroup ext ⟫
Isomorphisms
We can also define what it means for two structures to be isomorphic. The property of being an n-ary function morphism is defined in the following way:
Is-_-ary-morphism :
(n : ℕ) {A B : Set} → (A ^ n ⟶ A) → (B ^ n ⟶ B) → (A → B) → Set
Is- zero -ary-morphism f₁ f₂ m = m f₁ ≡ f₂
Is- suc n -ary-morphism f₁ f₂ m =
∀ x → Is- n -ary-morphism (f₁ x) (f₂ (m x)) m
This definition can be lifted to structures by ignoring the (propositional) axioms:
Is-structure-morphism :
(s : Structure) →
{A B : Set} → ⟦ s ⟧ A → ⟦ s ⟧ B →
(A → B) → Set
Is-structure-morphism empty _ _ m = ⊤
Is-structure-morphism (s +axiom _) (s₁ , _) (s₂ , _) m =
Is-structure-morphism s s₁ s₂ m
Is-structure-morphism (s +operator n) (s₁ , op₁) (s₂ , op₂) m =
Is-structure-morphism s s₁ s₂ m × Is- n -ary-morphism op₁ op₂ m
Two “top-level” structures are then defined to be isomorphic if there is a homomorphic bijection between the corresponding Sets:
Isomorphism : (s : Structure) → ⟪ s ⟫ → ⟪ s ⟫ → Set Isomorphism s (A , s₁) (B , s₂) = Σ (A ↔ B) λ m → Is-structure-morphism s s₁ s₂ (_↔_.to m)
Here m : A ↔ B means that m is a bijection from A to B, and _↔_.to m is the corresponding function of type A → B.
The result
Finally we can state the main result. Isomorphic structures are equal, assuming univalence:
Univalence-axiom′ (Set ²/≡) Set → Univalence-axiom lzero → (s : Structure) (s₁ s₂ : ⟪ s ⟫) → Isomorphism s s₁ s₂ → s₁ ≡ s₂
Here Univalence-axiom lzero is the full univalence axiom at universe level zero, and Univalence-axiom′ (Set ²/≡) Set is a special case of the univalence axiom at universe level one.
For the proof, see the code listing. The proof uses Voevodsky’s transport theorem (called subst-unique in the code).
In the future we may generalise the result to a larger class of structures, but the class above fits nicely in a blog post.
Homotopy Type Theory 
Cool! I really like the encoding using induction-recursion.
We experimented with universal algebra in Coq in [1] (type class quoting, …).
However, it became quite heavy. Do any of these issues become easier in agda?
[1] Bas Spitters and Eelis van der Weegen – Type Classes for Mathematics in Type Theory
Interactive theorem proving and the formalization of mathematics, Special Issue of Mathematical Structures in Computer Science, 21, 1-31, 2011 10.1017/S0960129511000119.
I’m not sure what issues you refer to. Perhaps Randy Pollack’s “Dependently Typed Records in Type Theory” is relevant: Randy shows how to use induction-recursion to encode record types with manifest fields and “with”.
I find it a bit puzzling that, in this definition of structure morphisms, axioms are ignored. This sounds a bit too simple to be true. If you think about it, it is possible to encode some algebraic structures either with operations and axioms.
For example, you may define groups by having a constant neutral operation 1, a multiplication operation _×_ and an inverse operation _⁻¹, with an axiom ∀a, a × a⁻¹ = 1, or with 1 and _×_ as only operations, with an axiom that ∀a∃!b, a × b = 1. In the latter case, the inverse operation is entirely encoded as an invertibility axiom. The corresponding notion of structure isomorphism in your framework will therefore be sensibly weaker, as it doesn’t directly give you preservation of inverses.
One can surely prove that those two formulations of groups are equivalent, to ensure that the notion of morphism in the latter case is in fact as strong as the first one. What would be a notion of (iso)morphism between *structures* (rather than structure instances) in your framework?
Yet, maybe it is possible to have a stronger notion of morphisms, with a notion of axiom preservation, so that this separate equivalence-of-structures step isn’t needed to get guarantees of preservation of inverses: I would expect the image of a structure morphism to be a sub-structure that satisfies the axioms. This could be provable generically but it would require a reified description of axioms (to even describe the relativization of the axiom to the morphism image), while this presentation admits arbitrary propositional predicates.
Is the invertibility axiom that you suggest propositional? I’m not sure how to interpret the quantifiers, but with a propositional interpretation you don’t get an actual inversion function, so the definition wouldn’t be equivalent to the other one. (Update: As has been pointed out below certain propositional statements actually give you useful functions.)
Anyway, this doesn’t really matter: the main result holds also for any stronger notion of isomorphism.
As Nils says, the axioms have to be propositional (ie they really are axioms, not computationally relevant axioms).
I you interpret the existential quantifier as a dependent sum, then your “axiom” is not propositional anymore so you cannot apply the theorem.
I you interpret the existential quantifier as the propositional reflection of a dependent sum, then you cannot extract an inverse from it anymore (because knowing that a set is not empty is not enough to conclude that it’s inhabited).
But in a monoid, inverses are unique as soon as they exist, even constructively. And if a set is inhabited and has at most one element, then you can choose that element. (I think this is a different distinction from ‘nonempty’ and ‘inhabited’ — both of those are propositions, one of them double-negated, while here we’re comparing the proposition ‘inhabited’ to the not-necessarily-proposition ‘has a specified element’.) So I think in this case, they really should be equivalent.
Indeed, if inverses are unique as soon as they exist, this should be equivalent. But then the notion of morphism will not be weaker, it will automatically preserve inverses.
But I was indeed confusing “nonempty” and “such that the h-prop reflection has a specified element”. I’m not sure if we should say “inhabited” for the second case. Sounds like a good word but for me if something is inhabited then I can extract an element of it. Here I think this would be only true when eliminating into another h-prop.
That’s right, the notion of morphism should also not be weaker in this case.
I think “inhabited” (i.e. “there exists an element”) can only mean “equipped with a specified element” if you choose the propositions-as-types logic. If you choose the propositions-as-hprops logic, then the meaning of “inhabited” is exactly that the h-prop reflection has an element.
When we have the propositions-as-hprops logic available, I think that insisting on using the propositions-as-types logic anyway impoverishes our language, since if “inhabited” means “equipped with a specified element” then what word is left to mean that the hprop reflection has an element? In my experience, all mathematicians (aside from type theorists wedded to the PAT logic) distinguish between a set having an element (which, if they are classical mathematicians, they call being “nonempty”) and being equipped with a specified element (one fairly standard word for this is being “pointed”).
The propositions-as-hprops logic is also the correct one semantically, when thinking of the model in simplicial sets or in more general higher toposes.
> In my experience, all mathematicians (aside from type theorists wedded to the PAT logic) distinguish between a set having an element (which, if they are classical mathematicians, they call being “nonempty”) and being equipped with a specified element (one fairly standard word for this is being “pointed”).
Sure, but then they say that if a set is inhabited, then you can choose such an element. Here I think it could be possible to have an inhabited type (in the propositions-as-hprops logic) which cannot be equipped with a specified element. That’s a distinction I’ve never seen before.
It’s completely standard in the sort of constructive mathematics that’s used as the internal logic of toposes. (Of course, in any one inhabited type you can always choose an element; the only problem comes when you have a possibly-infinite family of inhabited types.)
Additionally, even for a classical mathematician who believes in the axiom of choice, there is a difference between being able to choose an element and being equipped with a specified element.
My point was that even for one particular inhabited type, you may not be able to choose an element, because there could be a type A with no function [A] -> A. Am I wrong?
You can’t necessarily choose one element once and for all (that is, make the type pointed). But for purposes of any particular proof, you can choose an element, since a proof is a term belonging to an hprop, so you can use the elimination rule for [A].
A general comment about this result.
The main application is for transport of properties: it follows that if we have
s0 isomorphic to s1 and we prove a property P(s0), then we also have P(s1).
This should be useful for modularization: we can replace freely a
structure by another one which is isomorphic.
This transport of properties is -not- valid in set theory: we can define two monoids
s0 = (N,0,+) and s1 = (N-{0}, 1, +’) with x +’ y = x + y -1. These two
monoids are isomorphic, but in set theory, it is possible to formulate
a property true for s0 and not for s1: the property is that the carrier set contains 0.