defn: K-finite types

src/1Lab/Equiv.lagda.md

@@ -51,6 +51,7 @@ private
     A B : Type ℓ₁
 ```
 
+::: {.definition #fibre}
 A _homotopy fibre_, _fibre_ or _preimage_ of a function `f` at a point
 `y : B` is the collection of all elements of `A` that `f` maps to `y`.
 Since many choices of name are possible, we settle on the one that is
@@ -60,6 +61,7 @@ shortest and most aesthetic: `fibre`{.Agda}.
 fibre : (A → B) → B → Type _
 fibre f y = Σ _ λ x → f x ≡ y
 ```
+:::
 
 A function `f` is an equivalence if every one of its fibres is
 [[contractible]] - that is, for any element `y` in the range, there is

src/1Lab/Extensionality.agda

@@ -2,7 +2,7 @@ open import 1Lab.Reflection.Signature
 open import 1Lab.Path.IdentitySystem
 open import 1Lab.Reflection.HLevel
 open import 1Lab.Reflection.Subst
-open import 1Lab.Equiv.Embedding
+open import 1Lab.Function.Embedding
 open import 1Lab.HLevel.Retracts
 open import 1Lab.Reflection
 open import 1Lab.Type.Sigma

src/1Lab/Equiv/Embedding.lagda.md → src/1Lab/Function/Embedding.lagda.md

@@ -20,7 +20,7 @@ open import 1Lab.Type
 -->
 
 ```agda
-module 1Lab.Equiv.Embedding where
+module 1Lab.Function.Embedding where
 ```
 
 <!--

src/1Lab/Function/Surjection.lagda.md

@@ -0,0 +1,146 @@
+<!--
+```agda
+open import 1Lab.HIT.Truncation
+
+open import 1Lab.Function.Embedding
+open import 1Lab.Reflection.HLevel
+open import 1Lab.HLevel.Retracts
+open import 1Lab.HLevel
+open import 1Lab.Equiv
+open import 1Lab.Path
+open import 1Lab.Type
+
+open import Meta.Idiom
+open import Meta.Bind
+```
+-->
+
+```agda
+module 1Lab.Function.Surjection where
+```
+
+<!--
+```agda
+private variable
+  ℓ ℓ' : Level
+  A B C : Type ℓ
+```
+-->
+
+# Surjections {defines=surjection}
+
+A function $f : A \to B$ is a **surjection** if, for each $b : B$, we
+have $\| f^*b \|$: that is, all of its [[fibres]] are inhabited. Using
+the notation for [[mere existence|merely]], we may write this as
+
+$$
+\forall (b : B),\ \exists (a : A),\ f(a) = b\text{,}
+$$
+
+which is evidently the familiar notion of surjection.
+
+```agda
+is-surjective : (A → B) → Type _
+is-surjective f = ∀ b → ∥ fibre f b ∥
+```
+
+To abbreviate talking about surjections, we will use the notation $A
+\epi B$, pronounced "$A$ **covers** $B$".
+
+```agda
+_↠_ : Type ℓ → Type ℓ' → Type (ℓ ⊔ ℓ')
+A ↠ B = Σ[ f ∈ (A → B) ] is-surjective f
+```
+
+The notion of surjection is intimately connected with that of
+[[quotient]], and in particular with the elimination principle into
+[[propositions]]. We think of a surjection $A \to B$ as expressing that $B$
+can be "glued together" by [[introducing paths between|path]] the
+elements of $A$. Since any family of propositions respects these new
+paths, we can prove a property of $B$ by showing it for the "generators"
+coming from $A$:
+
+```agda
+is-surjective→elim-prop
+  : (f : A ↠ B)
+  → ∀ {ℓ} (P : B → Type ℓ)
+  → (∀ x → is-prop (P x))
+  → (∀ a → P (f .fst a))
+  → ∀ x → P x
+is-surjective→elim-prop (f , surj) P pprop pfa x =
+  ∥-∥-rec (pprop _) (λ (x , p) → subst P p (pfa x)) (surj x)
+```
+
+When the type $B$ is a set, we can actually take this analogy all the
+way to its conclusion: Given any cover $f : A \epi B$, we can produce an
+equivalence between $B$ and the quotient of $A$ under the [[congruence]]
+induced by $f$. See [[surjections are quotient maps]].
+
+## Closure properties
+
+The class of surjections contains the identity --- and thus every
+equivalence --- and is closed under composition.
+
+```agda
+∘-is-surjective
+  : {f : B → C} {g : A → B}
+  → is-surjective f
+  → is-surjective g
+  → is-surjective (f ∘ g)
+∘-is-surjective {f = f} fs gs x = do
+  (f*x , p) ← fs x
+  (g*fx , q) ← gs f*x
+  pure (g*fx , ap f q ∙ p)
+
+id-is-surjective : is-surjective {A = A} id
+id-is-surjective x = inc (x , refl)
+
+is-equiv→is-surjective : {f : A → B} → is-equiv f → is-surjective f
+is-equiv→is-surjective eqv x = inc (eqv .is-eqv x .centre)
+```
+
+<!--
+```agda
+Equiv→Cover : A ≃ B → A ↠ B
+Equiv→Cover f = f .fst , is-equiv→is-surjective (f .snd)
+```
+-->
+
+## Relationship with equivalences
+
+We have defined [[equivalences]] to be the maps with [[contractible]]
+fibres; and surjections to be the maps with _inhabited_ fibres. It
+follows that a surjection is an equivalence _precisely if_ its fibres
+are also [[propositions]]; in other words, if it is an [[embedding]].
+
+```agda
+embedding-surjective→is-equiv
+  : {f : A → B}
+  → is-embedding f
+  → is-surjective f
+  → is-equiv f
+embedding-surjective→is-equiv f-emb f-surj .is-eqv x = ∥-∥-proj! do
+  pt ← f-surj x
+  pure $ is-prop∙→is-contr (f-emb x) pt
+```
+
+<!--
+```agda
+injective-surjective→is-equiv
+  : {f : A → B}
+  → is-set B
+  → injective f
+  → is-surjective f
+  → is-equiv f
+injective-surjective→is-equiv b-set f-inj =
+  embedding-surjective→is-equiv (injective→is-embedding b-set _ f-inj)
+
+injective-surjective→is-equiv!
+  : {f : A → B} {@(tactic hlevel-tactic-worker) b-set : is-set B}
+  → injective f
+  → is-surjective f
+  → is-equiv f
+injective-surjective→is-equiv! {b-set = b-set} =
+  injective-surjective→is-equiv b-set
+```
+-->

src/1Lab/HLevel/Retracts.lagda.md

@@ -134,7 +134,7 @@ equiv→is-hlevel : (n : Nat) (f : A → B) → is-equiv f → is-hlevel A n →
 equiv→is-hlevel n f eqv = iso→is-hlevel n f (is-equiv→is-iso eqv)
 
 is-hlevel≃ : (n : Nat) → (B ≃ A) → is-hlevel A n → is-hlevel B n
-is-hlevel≃ n f = iso→is-hlevel n (Equiv.from f) (iso (Equiv.to f) (Equiv.η f) (Equiv.ε f))
+is-hlevel≃ n f = iso→is-hlevel n (equiv→inverse (f .snd)) (iso (f .fst) (equiv→unit (f .snd)) (equiv→counit (f .snd)))
 
 Iso→is-hlevel : (n : Nat) → Iso B A → is-hlevel A n → is-hlevel B n
 Iso→is-hlevel n (f , isic) = iso→is-hlevel n (isic .is-iso.inv) $

src/1Lab/Path/IdentitySystem.lagda.md

@@ -1,6 +1,6 @@
 <!--
 ```agda
-open import 1Lab.Equiv.Embedding
+open import 1Lab.Function.Embedding
 open import 1Lab.Equiv.Fibrewise
 open import 1Lab.HLevel.Retracts
 open import 1Lab.Type.Sigma

src/1Lab/Prelude.agda

@@ -23,9 +23,11 @@ open import 1Lab.HLevel.Universe public
 open import 1Lab.Equiv public
 open import 1Lab.Equiv.FromPath public
 open import 1Lab.Equiv.Fibrewise public
-open import 1Lab.Equiv.Embedding public
+open import 1Lab.Function.Embedding public
 open import 1Lab.Equiv.HalfAdjoint public
 
+open import 1Lab.Function.Surjection public
+
 open import 1Lab.Univalence public
 open import 1Lab.Univalence.SIP public
 

src/1Lab/Reflection.lagda.md

@@ -27,9 +27,9 @@ open import Meta.Idiom public
 open import Meta.Bind public
 open import Meta.Alt public
 
-open Data.Vec.Base using (Vec ; [] ; _∷_ ; lookup ; tabulate) public
 open Data.Product.NAry using ([_]) public
-open Data.List.Base hiding (lookup) public
+open Data.List.Base hiding (lookup ; tabulate) public
+open Data.Vec.Base using (Vec ; [] ; _∷_ ; lookup ; tabulate) public
 open Data.Dec.Base public
 open Data.Bool public
 

src/1Lab/Reflection/HLevel.agda

@@ -1,6 +1,6 @@
 {-# OPTIONS -vtactic.hlevel:20 -vtc.def:10 #-}
 open import 1Lab.Reflection.Record
-open import 1Lab.Equiv.Embedding
+open import 1Lab.Function.Embedding
 open import 1Lab.HLevel.Retracts
 open import 1Lab.HLevel.Universe
 open import 1Lab.Reflection
@@ -10,8 +10,8 @@ open import 1Lab.Equiv
 open import 1Lab.Path
 open import 1Lab.Type
 
+open import Data.List.Base
 open import Data.Bool
-open import Data.List
 
 open import Meta.Foldable
 
@@ -214,7 +214,8 @@ private
     go (def d ds) = go* ds
     go t          = pure tt
 
-    go* (arg (arginfo visible _) t ∷ as) = go t
+    go* (arg (arginfo visible _) t ∷ as)   = go t
+    go* (arg (arginfo instance' _) t ∷ as) = go t
     go* (_ ∷ as)                         = go* as
     go* []                               = pure tt
 
@@ -745,9 +746,6 @@ instance
   decomp-ntype : ∀ {ℓ} {n} → hlevel-decomposition (n-Type ℓ n)
   decomp-ntype = decomp (quote n-Type-is-hlevel) (`level-minus 1 ∷ [])
 
-  decomp-list : ∀ {ℓ} {A : Type ℓ} → hlevel-decomposition (List A)
-  decomp-list = decomp (quote ListPath.List-is-hlevel) (`level-minus 2 ∷ `search ∷ [])
-
   hlevel-proj-n-type : hlevel-projection (quote n-Type.∣_∣)
   hlevel-proj-n-type .has-level = quote n-Type.is-tr
   hlevel-proj-n-type .get-level ty = do

src/1Lab/Reflection/Solver.agda

@@ -4,7 +4,7 @@ open import 1Lab.Prelude
 open import 1Lab.Reflection
 open import 1Lab.Reflection.Variables
 
-open import Data.List
+open import Data.List.Base
 
 private variable
   ℓ : Level

src/1Lab/Resizing.lagda.md

@@ -197,6 +197,14 @@ to-is-true
   → ∣ P ∣
   → P ≡ Q
 to-is-true prf = Ω-ua (λ _ → hlevel 0 .centre) (λ _ → prf)
+
+tr-□ : ∀ {ℓ} {A : Type ℓ} → ∥ A ∥ → □ A
+tr-□ (inc x) = inc x
+tr-□ (squash x y i) = squash (tr-□ x) (tr-□ y) i
+
+□-tr : ∀ {ℓ} {A : Type ℓ} → □ A → ∥ A ∥
+□-tr (inc x) = inc x
+□-tr (squash x y i) = squash (□-tr x) (□-tr y) i
 ```
 -->
 

src/1Lab/Underlying.agda

@@ -69,6 +69,12 @@ _∈_ : ∀ {ℓ ℓ'} {A : Type ℓ} {P : Type ℓ'} ⦃ u : Underlying P ⦄
     → A → (A → P) → Type (u .ℓ-underlying)
 x ∈ P = ⌞ P x ⌟
 
+-- Generalised "total space" notation.
+∫ₚ
+  : ∀ {ℓ ℓ'} {X : Type ℓ} {P : Type ℓ'} ⦃ u : Underlying P ⦄
+  → (X → P) → Type _
+∫ₚ P = Σ _ (_∈ P)
+
 -- Notation class for type families which are "function-like" (always
 -- nondependent). Slight generalisation of the homs of concrete
 -- categories.

src/1Lab/Univalence/SIP/Auto.agda

@@ -6,7 +6,7 @@ open import 1Lab.Equiv
 open import 1Lab.Path
 open import 1Lab.Type
 
-open import Data.List
+open import Data.List.Base
 
 module 1Lab.Univalence.SIP.Auto where
 

src/Algebra/Group/Subgroup.lagda.md

@@ -32,11 +32,9 @@ private module _ {ℓ} where open Cat.Displayed.Instances.Subobjects (Groups ℓ
 A **subgroup** $m$ of a group $G$ is a [[monomorphism]] $H \xto{m} G$,
 that is, an object of the [[poset of subobjects]] $\Sub(G)$. Since group
 homomorphisms are injective exactly when their underlying function is an
-[embedding], we can alternatively describe this as a condition on a
+[[embedding]], we can alternatively describe this as a condition on a
 predicate $G \to \prop$.
 
-[embedding]: 1Lab.Equiv.Embedding.html
-
 ```agda
 Subgroup : Group ℓ → Type (lsuc ℓ)
 Subgroup {ℓ = ℓ} G = Subobject G
@@ -548,7 +546,7 @@ that, if $\rm{inc}(x) = \rm{inc}(y)$, then $(x - y) \in H$.
   normal-subgroup→congruence .symᶜ = rel-sym
 
   /ᴳ-effective : ∀ {x y} → Path G/H (inc x) (inc y) → rel x y
-  /ᴳ-effective = equiv→inverse (effective normal-subgroup→congruence)
+  /ᴳ-effective = effective normal-subgroup→congruence
 ```
 
 <!--

src/Algebra/Ring/Commutative.lagda.md

@@ -1,6 +1,6 @@
 <!--
 ```agda
-open import 1Lab.Equiv.Embedding
+open import 1Lab.Function.Embedding
 
 open import Algebra.Prelude
 open import Algebra.Ring

src/Cat/Diagram/Congruence.lagda.md

@@ -5,7 +5,7 @@ open import Cat.Diagram.Limit.Finite
 open import Cat.Diagram.Coequaliser
 open import Cat.Diagram.Pullback
 open import Cat.Diagram.Product
-open import Cat.Prelude
+open import Cat.Prelude hiding (Kernel-pair)
 
 import Cat.Reasoning
 ```
@@ -23,13 +23,10 @@ _equivalence relation_. Recall that an equivalence relation on a [[set]]
 is a family of [[propositions]] $R : A \times A \to \prop$ satisfying
 _reflexivity_ ($R(x,x)$ for all $x$), _transitivity_ ($R(x,y) \land
 R(y,z) \to R(x,z)$), and _symmetry_ ($R(x,y) \to R(y,x)$). Knowing that
-$\prop$ classifies [embeddings], we can equivalently talk about an
+$\prop$ classifies [[embeddings]], we can equivalently talk about an
 equivalence relation $R$ as being _just some set_, equipped with a
 [[monomorphism]] $m : R \mono A \times A$.
 
-[embeddings]: 1Lab.Equiv.Embedding.html
-[mono]: Cat.Morphism.html#monos
-
 We must now identify what properties of the mono $m$ identify $R$ as
 being the total space of an equivalence relation. Let us work in the
 category of sets for the moment. Suppose $R$ is a relation on $A$, and

src/Cat/Diagram/Image.lagda.md

@@ -36,18 +36,16 @@ Let $f : A \to B$ be an ordinary function between sets (or, indeed,
 arbitrary types). Its **image** $\im f$ can be computed as the subset
 $\{ b \in B : (\exists a)\ b = f(a) \}$, but this description does not
 carry over to more general categories: More abstractly, we can say that
-the image [embeds into] $B$, and admits a map from $A$ (in material set
-theory, this is $f$ itself --- structurally, it is called the
+the image [[embeds into|embedding]] $B$, and admits a map from $A$ (in
+material set theory, this is $f$ itself --- structurally, it is called
+the
 **corestriction** of $f$). Furthermore, these two maps _factor_ $f$, in
 that:
 
 $$
 (A \xto{e} \im f \xmono{m} B) = (A \xto{f} B)
 $$
 
-
-[embeds into]: 1Lab.Equiv.Embedding.html
-
 While these are indeed two necessary properties of an _image_, they fail
 to accurately represent the set-theoretic construction: Observe that,
 e.g. for $f(x) = 2x$, we could take $\im f = \bb{N}$, taking $e = f$

src/Cat/Diagram/Sieve.lagda.md

@@ -1,5 +1,6 @@
 <!--
 ```agda
+{-# OPTIONS -vtactic.hlevel:30 #-}
 open import Cat.Instances.Functor
 open import Cat.Functor.Hom
 open import Cat.Prelude

src/Cat/Displayed/Univalence/Thin.lagda.md

@@ -1,7 +1,7 @@
 <!--
 ```agda
 {-# OPTIONS --lossy-unification #-}
-open import 1Lab.Equiv.Embedding
+open import 1Lab.Function.Embedding
 
 open import Cat.Displayed.Univalence
 open import Cat.Functor.Properties