------------------------------------------------------------------------ -- Code related to the paper "Isomorphism Is Equality" by Thierry -- Coquand and Nils Anders Danielsson -- -- The code is written by Nils Anders Danielsson ------------------------------------------------------------------------ -- Note that the code has been changed after the paper was published. {-# OPTIONS --cubical-compatible --safe #-} module README.Isomorphism-is-equality where ---===================================================================== -- 2: Preliminaries ------------------------------------------------------------------------ -- 2.1: Hierarchy of Types -- The lifting operator ↑. (Note that Agda is universe-polymorphic.) import Prelude ------------------------------------------------------------------------ -- 2.2: Quantifiers -- Σ, ∃ and _×_. (The code sometimes uses ∃ instead of Σ.) import Prelude ------------------------------------------------------------------------ -- 2.3: Equality -- Axiomatisations of equality, used in order to ensure that the -- elimination rule (J) does not compute. J is called elim in the -- code. import Equality -- Bijections (_↔_), the key property of equality of Σ-types -- (Σ-≡,≡↔≡). import Bijection -- Extensionality. import Equality -- "∀ x. f x ≡ g x is in bijective correspondence with f ≡ g" -- (extensionality-isomorphism). import Equivalence ------------------------------------------------------------------------ -- 2.4: More Types -- ⊤, ⊥, _+_ (called _⊎_ in the code), ℕ. import Prelude -- Logical equivalences (_⇔_). import Logical-equivalence ------------------------------------------------------------------------ -- 2.5: Univalent Foundations -- Contractible. import Equality -- H-level, Is-proposition, Is-set. import H-level -- Results that can be used to establish that a type has a certain -- h-level. import H-level import H-level.Closure import Equality.Decidable-UIP -- Propositional second components of pairs can be dropped -- (ignore-propositional-component). import Function-universe -- Is-equivalence, subst P eq is an equivalence -- (subst-is-equivalence), _≃_, _≃_ is logically equivalent to _↔_ and -- related properties (_≃_.bijection, ↔⇒≃, ↔↔≃, ⇔↔≃), Σ and Π preserve -- equivalences (Σ-preserves, Π-preserves). import Equivalence -- More congruence properties (including _⊎-cong_ and →-cong). import Function-universe -- ≡⇒≃, Univalence, ≃⇒≡, the univalence axiom implies extensionality -- (dependent-extensionality), the transport theorem -- (transport-theorem), resp eq is an equivalence -- (resp-is-equivalence), resp eq preserves compositions -- (resp-preserves-compositions). import Univalence-axiom ---===================================================================== -- 3: Isomorphism Is Equality ------------------------------------------------------------------------ -- 3.1: Parameters -- The parameters are represented using a record type called Universe. import Univalence-axiom.Isomorphism-is-equality.Simple ------------------------------------------------------------------------ -- 3.2: Codes for Structures -- Code, Instance, Is-isomorphism, Isomorphic, Carrier, element, -- equality-pair-lemma. import Univalence-axiom.Isomorphism-is-equality.Simple ------------------------------------------------------------------------ -- 3.3: Main Theorem -- The main result (isomorphism-is-equality), isomorphism is equal to -- equality (isomorphic≡≡), the right-to-left direction of the -- bijection is equal to a simple function -- (from-isomorphism-is-equality). import Univalence-axiom.Isomorphism-is-equality.Simple ------------------------------------------------------------------------ -- 3.4: A Universe -- U, El, cast, resp, resp-id, Is-isomorphism′, -- isomorphism-definitions-isomorphic. import Univalence-axiom.Isomorphism-is-equality.Simple -- The operators _→-eq_ (→-cong-⇔), _×-eq_ (_×-cong_) and _+-eq_ -- (_⊎-cong_). import Function-universe -- The operators _→-rel_, _×-rel_ and _+-rel_ (_⊎-rel_). import Prelude ------------------------------------------------------------------------ -- 3.5: Examples -- Monoids, posets, discrete fields, fixpoint operators. import Univalence-axiom.Isomorphism-is-equality.Simple ---===================================================================== -- 4: Related Work -- Aczel's structure identity principle (structure-identity-principle). import Structure-identity-principle -- The structure identity principle can be used to prove a slightly -- restricted variant of our main theorem (isomorphism-is-equality′, -- from-isomorphism-is-equality′). import Univalence-axiom.Isomorphism-is-equality.Structure-identity-principle