------------------------------------------------------------------------
-- Code related to the paper "Higher Inductive Type Eliminators
-- Without Paths"
--
-- Nils Anders Danielsson
------------------------------------------------------------------------
-- Note that the code does not follow the paper exactly. For instance,
-- some definitions use bijections (functions with quasi-inverses)
-- instead of equivalences. Furthermore type universes are called
-- "Set a" instead of "Type a".
{-# OPTIONS --cubical --safe #-}
module README.HITs-without-paths where
import Equality
import Equality.Id
import Equality.Instances-related
import Equality.Path
import Equality.Path.Isomorphisms
import Equality.Propositional
import Function-universe
import H-level
import H-level.Truncation.Propositional
import Quotient
import Suspension
------------------------------------------------------------------------
-- 1: Introduction
-- The propositional truncation operator.
∥_∥ = H-level.Truncation.Propositional.∥_∥
-- Equality defined as an inductive family with a single constructor
-- refl.
_≡_ = Equality.Propositional._≡_
------------------------------------------------------------------------
-- 2: An Axiomatisation of Equality With J
-- The code uses an axiomatisation of "equality with J", as discussed
-- in the text. The axiomatisation is a little convoluted in order to
-- support using equality at all universe levels. Furthermore, also as
-- discussed in the text, the axiomatisation supports choosing
-- specific definitions for other functions, like cong, to make the
-- code more usable when it is instantiated with Cubical Agda paths
-- (for which the canonical definition of cong computes in a different
-- way than typical definitions obtained using J).
-- Equality and reflexivity.
≡-refl = Equality.Reflexive-relation
-- The J rule and its computation rule.
J-J-refl = Equality.Equality-with-J₀
-- Extended variants of the two definitions above.
Equivalence-relation⁺ = Equality.Equivalence-relation⁺
Equality-with-J = Equality.Equality-with-J
Equality-with-paths = Equality.Path.Equality-with-paths
-- The extended variants are inhabited for all universe levels if the
-- basic ones are inhabited for all universe levels.
J₀⇒Equivalence-relation⁺ = Equality.J₀⇒Equivalence-relation⁺
J₀⇒J = Equality.J₀⇒J
Equality-with-J₀⇒Equality-with-paths =
Equality.Path.Equality-with-J₀⇒Equality-with-paths
-- To see how the code is axiomatised, see the module header of, say,
-- Circle.
import Circle
-- Any two notions of equality satisfying the axioms are pointwise
-- isomorphic, and the isomorphisms map canonical proofs of
-- reflexivity to canonical proofs of reflexivity.
--
-- Note that in some cases the code uses bijections (_↔_) instead of
-- equivalences (_≃_).
instances-isomorphic =
Equality.Instances-related.all-equality-types-isomorphic
-- Cubical Agda paths, the Cubical Agda identity type family, and a
-- definition of equality as an inductive family with a single
-- constructor refl are instances of the axioms. (The last instance is
-- for Equality-with-J rather than Equality-with-paths, because the
-- latter definition is defined in Cubical Agda, and the instance is
-- not.)
paths-instance = Equality.Path.equality-with-paths
id-instance = Equality.Id.equality-with-paths
inductive-family-instance = Equality.Propositional.equality-with-J
------------------------------------------------------------------------
-- 3: Homogeneous Paths
-- The path type constructor.
Path = Equality.Path._≡_
-- Zero and one.
0̲ = Equality.Path.0̲
1̲ = Equality.Path.1̲
-- Reflexivity.
reflᴾ = Equality.Path.refl
-- Minimum, maximum and negation.
min = Equality.Path.min
max = Equality.Path.max
-_ = Equality.Path.-_
-- The primitive transport operation.
open Equality.Path using (transport)
-- The J rule and transport-refl.
Jᴾ = Equality.Path.elim
transport-refl = Equality.Path.transport-refl
-- Transitivity (more general than in the paper).
transᴾ = Equality.Path.htransʳ
------------------------------------------------------------------------
-- 4: Heterogeneous Paths
-- Pathᴴ.
Pathᴴ = Equality.Path.[_]_≡_
-- The eliminator elimᴾ for the propositional truncation operator.
module ∥_∥ where
elimᴾ = H-level.Truncation.Propositional.elimᴾ′
-- Pathᴴ≡Path and Pathᴴ≃Path.
Pathᴴ≡Path = Equality.Path.heterogeneous≡homogeneous
Pathᴴ≃Path = Equality.Path.heterogeneous↔homogeneous
-- The lemma substᴾ.
substᴾ = Equality.Path.subst
-- The lemmas subst and subst-refl from the axiomatisation.
subst = Equality.Equality-with-J.subst
subst-refl = Equality.Equality-with-J.subst-refl
-- The axiomatisation makes it possible to choose the implementations
-- of to-path and from-path.
to-path = Equality.Path.Equality-with-paths.to-path
from-path = Equality.Path.Equality-with-paths.from-path
-- The code mostly uses a pointwise isomorphism between the arbitrary
-- notion of equality and paths instead of from-path and to-path.
≡↔≡ = Equality.Path.Derived-definitions-and-properties.≡↔≡
-- The lemmas subst≡substᴾ, subst≡≃Pathᴴ, subst≡→Pathᴴ and
-- subst≡→substᴾ≡ (which is formulated as a bijection).
subst≡substᴾ = Equality.Path.Isomorphisms.subst≡subst
subst≡≃Pathᴴ = Equality.Path.Isomorphisms.subst≡↔[]≡
subst≡→Pathᴴ = Equality.Path.Isomorphisms.subst≡→[]≡
subst≡→substᴾ≡ = Equality.Path.Isomorphisms.subst≡↔subst≡
-- The lemmas congᴰ and congᴰ-refl from the axiomatisation.
congᴰ = Equality.Equality-with-J.dcong
congᴰ-refl = Equality.Equality-with-J.dcong-refl
-- The lemmas congᴴ and congᴰᴾ.
congᴴ = Equality.Path.hcong
congᴰᴾ = Equality.Path.dcong
-- The proofs congᴰ≡congᴰᴾ, congᴰᴾ≡congᴴ, congᴰ≡congᴴ and
-- dependent‐computation‐rule‐lemma.
congᴰ≡congᴰᴾ = Equality.Path.Isomorphisms.dcong≡dcong
congᴰᴾ≡congᴴ = Equality.Path.dcong≡hcong
congᴰ≡congᴴ = Equality.Path.Isomorphisms.dcong≡hcong
dependent‐computation‐rule‐lemma =
Equality.Path.Isomorphisms.dcong-subst≡→[]≡
------------------------------------------------------------------------
-- 5: The Circle Without Paths
-- The circle and loop.
𝕊¹ = Circle.𝕊¹
loop = Circle.loop
-- The lemmas cong and cong-refl from the axiomatisation.
cong = Equality.Equality-with-J.cong
cong-refl = Equality.Equality-with-J.cong-refl
-- The lemma non-dependent-computation-rule-lemma.
non-dependent-computation-rule-lemma =
Equality.Path.Isomorphisms.cong-≡↔≡
-- The lemma trans, which is actually a part of the axiomatisation
-- that I use, but which can be proved using the J rule.
trans = Equality.Equivalence-relation⁺.trans
J₀⇒trans = Equality.J₀⇒Equivalence-relation⁺
-- The lemma subst-const.
subst-const = Equality.Derived-definitions-and-properties.subst-const
-- The lemma congᴰ≡→cong≡.
congᴰ≡→cong≡ = Equality.Derived-definitions-and-properties.dcong≡→cong≡
-- Eliminators and computation rules.
module 𝕊¹ where
elimᴾ = Circle.elimᴾ
recᴾ = Circle.recᴾ
elim = Circle.elim
elim-loop = Circle.elim-loop
rec = Circle.rec
rec-loop = Circle.rec-loop
rec′ = Circle.rec′
rec′-loop = Circle.rec′-loop
------------------------------------------------------------------------
-- 6: Set Quotients Without Paths
-- The definition of h-levels.
Contractible = Equality.Derived-definitions-and-properties.Contractible
H-level = H-level.H-level
Is-proposition = Equality.Derived-definitions-and-properties.Is-proposition
Is-set = Equality.Derived-definitions-and-properties.Is-set
-- Set quotients.
_/_ = Quotient._/_
-- Some lemmas.
H-levelᴾ-suc≃H-levelᴾ-Pathᴴ = Equality.Path.H-level-suc↔H-level[]≡
index-irrelevant = Equality.Path.index-irrelevant
transport-transport = Equality.Path.transport∘transport
heterogeneous-irrelevance = Equality.Path.heterogeneous-irrelevance
heterogeneous-UIP = Equality.Path.heterogeneous-UIP
H-level≃H-levelᴾ = Equality.Path.Isomorphisms.H-level↔H-level
-- A generalisation of Π-cong. Note that equality is provably
-- extensional in Cubical Agda.
Π-cong = Function-universe.Π-cong
extensionality = Equality.Path.ext
-- Variants of the constructors.
[]-respects-relation = Quotient.[]-respects-relation
/-is-set = Quotient./-is-set
-- Eliminators.
module _/_ where
elimᴾ′ = Quotient.elimᴾ′
elimᴾ = Quotient.elimᴾ
recᴾ = Quotient.recᴾ
elim = Quotient.elim
rec = Quotient.rec
------------------------------------------------------------------------
-- 7: More Examples
-- Suspensions.
module Susp where
Susp = Suspension.Susp
elimᴾ = Suspension.elimᴾ
recᴾ = Suspension.recᴾ
meridian = Suspension.meridian
elim = Suspension.elim
elim-meridian = Suspension.elim-meridian
rec = Suspension.rec
rec-meridian = Suspension.rec-meridian
-- The propositional truncation operator.
module Propositional-truncation where
elimᴾ′ = H-level.Truncation.Propositional.elimᴾ′
elimᴾ = H-level.Truncation.Propositional.elimᴾ
recᴾ = H-level.Truncation.Propositional.recᴾ
trivial = H-level.Truncation.Propositional.truncation-is-proposition
elim = H-level.Truncation.Propositional.elim
rec = H-level.Truncation.Propositional.rec
------------------------------------------------------------------------
-- 8: An Alternative Approach
-- Circle and Circleᴾ, combined into a single definition.
Circle = Circle.Circle
-- Circleᴾ≃Circle, circleᴾ and circle.
Circleᴾ≃Circle = Circle.Circle≃Circle
circleᴾ = Circle.circleᴾ
circle = Circle.circle
-- The computation rule for the higher constructor.
elim-loop-circle = Circle.elim-loop-circle
-- Alternative definitions of Circleᴾ≃Circle and circle that (at the
-- time of writing) do not give the "correct" computational behaviour
-- for the point constructor.
Circleᴾ≃Circle′ = Circle.Circle≃Circle′
circle′ = Circle.circle′
------------------------------------------------------------------------
-- 9: Discussion
-- The interval.
import Interval
-- Pushouts.
import Pushout
-- A general truncation operator.
import H-level.Truncation
-- The torus.
import Torus