{-# OPTIONS -vtc.def:10 -vtc.ip.boundary:30 #-} open import 1Lab.Prelude open import Data.Id.Base open import Data.Bool module Data.Image where
Images and replacement🔗
The image of a function is the subtype of where points are merely equipped with a fibre of . This has the expected universal property: we can factor any into
and is universal among factorisations of through a subtype of its codomain.
In general, we can consider images of arbitrary functions , where is a -small type, and is a -small type; This results in a type , which, according to the rules for assigning universe levels, lives in the th universe. While the rules are that way for good reasons, in this case, they defy intuition: the type , in a sense, is “at most the size of ”.
Can we do better? It turns out that we can! This generally goes by the name of type-theoretic replacement, after Rijke (Rijke 2017, sec. 5); in turn, the name replacement comes from the axiom of material set theory sayings the image of a set under a function is again set.1 Here we implement a slight generalization of Evan Cavallo’s construction in terms of higher induction-recursion.
We understand this construction as generalising the first isomorphism theorem from the setting of algebraic structures2 to the setting of general types. Recall that the first isomorphism theorem says you can compute as the quotient .3
If we’re working with sets, that’s the end of it: We can define a relation by , which can be made to live in the zeroth universe, so lives in the same universe as . That’s because, when working with sets, there are no coherence problems to get stuck on: we can first define as a higher inductive type, then, separately, define the embedding .
However, in the case of general types, we would like the h-level of to match that of , so we certainly can’t set-truncate.
Anyway, The next immediate attempt might be a type which looks like
data Im1 {ℓa ℓb} {A : Type ℓa} {B : Type ℓb} (f : A → B) : Type (ℓa ⊔ ℓb) where inc : A → Im1 f quot : ∀ x y → f x ≡ f y → inc x ≡ inc y
But this type isn’t particularly well-behaved. For example, the Im1-image of the identity map on the unit type is the circle. This can be established by writing equivalences back and forth, but in the interest of brevity (and our dependency graph), we show it has a non-trivial path.
Cover : Im1 {A = ⊤} {⊤} (λ { tt → tt }) → Type Cover (inc x) = Bool Cover (quot tt tt _ i) = ua (not , not-is-equiv) i Im1-nontriv : subst Cover (quot tt tt refl) true ≡ false Im1-nontriv = refl
It’s fairly common that defining higher inductive types like this will, sometimes, introduce more paths than you might expect. For an analogy, if we were interested in computing propositional truncations instead, our type Im1 above would correspond to this “one-step truncation”:
data Tr1 {ℓa} (A : Type ℓa) : Type ℓa where inc : A → Tr1 A quot : (x y : A) → inc x ≡ inc y
And, investigating the case of truncations, we might come up with a couple different fixes. One is to define a process that could be iterated: each step adds new paths, and at the limit — the sequential co-limit — we have our original type. This can be made to work for the propositional truncation, and (Rijke 2017)’s construction of the image is similar in spirit.
But if we have recursive higher inductive types, where the type being defined can appear in the arguments to its own path constructors, we can sometimes do these constructions in a single big, recursive step. That’s the usual propositional truncation. A guiding, heuristic principle would be to avoid “green slime”: do not mention the constructors of the type in the endpoints of the path constructor.
Types without green slime are much more merciful than the judges of coherence hell, because you don’t have to match to apply the path constructors, as you would in Tr1: If you have the arguments handy, you can apply them targeting arbitrary points. Lovely! But In the image case, this still doesn’t really work, because we don’t want to identify arbitrary points. Our requirements are something like this:
A tractable description: finitely many constructors, and hopefully “no more than a few”. This guarantees that we can tell Agda Agda about the construction and actually work with it, which is also important.
Without any green slime, to hopefully avoid the coherent issues.
So that points from are identified in exactly how they would be identified in under .
If we had such a type, we could define an embedding , which tells us how to compute the path spaces in : . In fact, since images are almost entirely characterised by having such an embedding, we can use our hypothetical to rewrite the third bullet point:
- With a constructor coherently mapping proofs of to .
Also, note that, since we were trying to get a smaller image, we can’t just use ’s path types: those live at the same universe as . What we can do instead is parametrise over an [identity system] on , a reflexive family of types which is equivalent to but which might be smaller. So, our requirement on identifications should be
- With a constructor coherently mapping proofs of to .
But, identity system or not, this is hopeless, right? We don’t know how to specify without first defining ; and it makes no sense to define before its domain type. The only way forward would be to somehow define them at the same time. That’s impossible, right?
Higher induction-recursion🔗
It’s actually totally possible to, at least in Agda, define higher inductive types at the same time as we define pattern-matching functions on them. And that’s exactly what we’ll do: specify higher-inductively at the same time as we define by recursion. Our three bullet points from before become the specification of the inductive type!
module Replacement {ℓₐ ℓₜ ℓᵢ} {A : Type ℓₐ} {T : Type ℓₜ} {_∼_ : T → T → Type ℓᵢ} {rr : ∀ x → x ∼ x} (locally-small : is-identity-system _∼_ rr) (f : A → T) where private module ls = Ids locally-small data Image : Type (ℓₐ ⊔ ℓᵢ) embed : Image → T data Image where inc : A → Image quot : ∀ {r r′} → embed r ∼ embed r′ → r ≡ r′ coh : ∀ r → quot (rr (embed r)) ≡ refl embed (inc a) = f a embed (quot p i) = locally-small .to-path p i embed (coh r i j) = to-path-refl {a = embed r} locally-small i j
Well, there’s still a minor coherence quibble. To show that
image-embedding
is an embedding, we need quot to send the reflexivity of
the identity system to the actual reflexivity path. But that’s a single
coherence constructor, not infinitely many, and it’s satisfied by our
projection function. We’ll show that it’s an embedding by showing that
it’s coherently cancellable, i.e. that we have an equivalence
.
embed-is-embedding : is-embedding embed embed-is-embedding = cancellable→embedding λ {x y} → Iso→Equiv (from , iso (ap embed) invr (invl {x} {y})) where from : ∀ {x y} → embed x ≡ embed y → x ≡ y from path = quot (ls.from path) invr : ∀ {x y} → is-right-inverse (ap embed {x} {y}) from invr = J (λ y p → from (ap embed p) ≡ p) (ap quot (transport-refl _) ∙ coh _) invl : ∀ {x y} → is-left-inverse (ap embed {x} {y}) from invl p = ls.ε _
As usual with these things, we can establish properties of Image without caring about the higher constructors.
Image-elim-prop : ∀ {ℓ′} {P : Image → Type ℓ′} → (∀ x → is-prop (P x)) → (∀ x → P (inc x)) → ∀ x → P x Image-elim-prop pprop pinc (inc x) = pinc x Image-elim-prop pprop pinc (quot {x} {y} p i) = is-prop→pathp (λ i → pprop (quot p i)) (Image-elim-prop pprop pinc x) (Image-elim-prop pprop pinc y) i Image-elim-prop pprop pinc (coh r i j) = is-prop→squarep (λ i j → pprop (coh r i j)) (λ _ → Image-elim-prop pprop pinc r) (is-prop→pathp (λ i → pprop _) _ _) (λ _ → Image-elim-prop pprop pinc r) (λ _ → Image-elim-prop pprop pinc r) i j
From which surjectivity follows immediately:
inc-is-surjective : ∀ a → ∥ fibre inc a ∥ inc-is-surjective = Image-elim-prop (λ _ → squash) (λ x → inc (x , refl))
Comparison🔗
We define a “comparison” map from the resized image to the “ordinary” image. This map is a bit annoying to define, and it relies on being able to easily map from the Image into propositions. It’s definitional that projecting from Image→image gives our embedding, since that’s how we define the map.
Image→image : Image → image f Image→image x .fst = embed x Image→image x .snd = Image-elim-prop {P = λ x → ∥ fibre f (embed x) ∥} (λ _ → squash) (λ x → inc (x , refl)) x
Establishing that Image→image is an equivalence is one of the rare cases where it’s easier to show that it has contractible fibres. That’s because we can eliminate the propositional truncation as the first step, and deal only with untruncated data from then on.
Image→image-is-equiv : is-equiv Image→image Image→image-is-equiv .is-eqv (x , p) = ∥-∥-elim {P = λ p → is-contr (fibre Image→image (x , p))} (λ _ → is-contr-is-prop) (λ { (i , p) → J (λ x p → is-contr (fibre Image→image (x , inc (i , p)))) (work′ i) p }) p where work′ : (f⁻¹x : A) → is-contr (fibre Image→image (f f⁻¹x , inc (_ , refl))) work′ f⁻¹x .centre = inc f⁻¹x , refl -- inc f⁻¹x , refl
Contracting the fibres is where we get some mileage out of having gotten the green slime out of quot. We have to show , as elements of the image, but we have an assumption that , which, under quot, is exactly what we need.
work′ f⁻¹x .paths (i , α) = Σ-pathp (quot (ls.from (sym (ap fst α)))) $ Σ-prop-square (λ _ → squash) $ commutes→square $ (ap₂ _∙_ (ls.ε (sym (ap fst α))) refl ∙ ∙-inv-l _ ∙ sym (∙-id-l _))
Keep in mind that material set theory says “is a set” in a very different way than we do; They mean it about size.↩︎
A class which includes , as models of the trivial theory↩︎
The meaning of kernel we’re using generalises slightly that of groups, where a normal subgroup completely determines an equivalence relation. Instead, we mean the kernel pair, the pullback of a morphism along itself.↩︎
References
- Rijke, Egbert. 2017. “The Join Construction.” arXiv. https://doi.org/10.48550/ARXIV.1701.07538.