Rewrite theory

src/1Lab/HIT/Truncation.lagda.md

@@ -106,8 +106,11 @@ whenever it is a family of propositions, by providing a case for
   → (x : ∥ A ∥) → P
 ∥-∥-rec! {pprop = pprop} = ∥-∥-elim (λ _ → pprop)
 
-∥-∥-proj : ∀ {ℓ} {A : Type ℓ} → {@(tactic hlevel-tactic-worker) ap : is-prop A} → ∥ A ∥ → A
-∥-∥-proj {ap = ap} = ∥-∥-rec ap λ x → x
+∥-∥-proj : ∀ {ℓ} {A : Type ℓ} → is-prop A → ∥ A ∥ → A
+∥-∥-proj ap = ∥-∥-rec ap λ x → x
+
+∥-∥-proj! : ∀ {ℓ} {A : Type ℓ} → {@(tactic hlevel-tactic-worker) ap : is-prop A} → ∥ A ∥ → A
+∥-∥-proj! {ap = ap} = ∥-∥-proj ap
 ```
 -->
 

src/Cat/Univalent/Rezk/Universal.lagda.md

@@ -86,7 +86,7 @@ eso→pre-faithful
   → is-eso H → (γ δ : F => G)
   → (∀ b → γ .η (H .F₀ b) ≡ δ .η (H .F₀ b)) → γ ≡ δ
 eso→pre-faithful {A = A} {B = B} {C = C} H {F} {G} h-eso γ δ p =
-  Nat-path λ b → ∥-∥-proj {ap = C.Hom-set _ _ _ _} do
+  Nat-path λ b → ∥-∥-proj (C.Hom-set _ _ _ _) do
   (b′ , m) ← h-eso b
   ∥_∥.inc $
     γ .η b                                      ≡⟨ C.intror (F-map-iso F m .invl) ⟩
@@ -191,7 +191,7 @@ this file in Agda and poke around the proof.
 ```agda
       lemma : (a : A.Ob) (f : H.₀ a B.≅ b)
             → γ.η a ≡ G.₁ (f .from) C.∘ g C.∘ F.₁ (f .to)
-      lemma a f = ∥-∥-proj {ap = C.Hom-set _ _ _ _} do
+      lemma a f = ∥-∥-proj (C.Hom-set _ _ _ _) do
         (k , p)   ← H-full (h.from B.∘ B.to f)
         (k⁻¹ , q) ← H-full (B.from f B.∘ h.to)
         ∥_∥.inc $
@@ -216,7 +216,7 @@ over $b$ is a proposition.
     T-prop : ∀ b → is-prop (T b)
     T-prop b (g , coh) (g′ , coh′) =
       Σ-prop-path (λ x → Π-is-hlevel² 1 λ _ _ → C.Hom-set _ _ _ _) $
-        ∥-∥-proj {ap = C.Hom-set _ _ _ _} do
+        ∥-∥-proj (C.Hom-set _ _ _ _) do
         (a₀ , h) ← H-eso b
         pure $ C.iso→epic (F-map-iso F h) _ _
           (C.iso→monic (F-map-iso G (h B.Iso⁻¹)) _ _
@@ -236,7 +236,7 @@ $(a,h)$ pair.
       ∥_∥.inc (Mk.g b a₀ h , Mk.lemma b a₀ h)
 
     mkT : ∀ b → T b
-    mkT b = ∥-∥-proj {ap = T-prop b} (mkT′ b (H-eso b))
+    mkT b = ∥-∥-proj (T-prop b) (mkT′ b (H-eso b))
 ```
 
 Another calculation shows that, since $H$ is full, given any pair of
@@ -260,7 +260,7 @@ the transformation we're defining, too.
         module h = B._≅_ h
 
       naturality : _
-      naturality = ∥-∥-proj {ap = C.Hom-set _ _ _ _} do
+      naturality = ∥-∥-proj (C.Hom-set _ _ _ _) do
         (k , p) ← H-full (h′.from B.∘ f B.∘ h.to)
         pure $ C.pullr (C.pullr (F.weave (sym
                   (B.pushl p ∙ ap₂ B._∘_ refl (B.cancelr h.invl)))))
@@ -281,16 +281,16 @@ $- \circ H$ is faithful, and now we've shown it is full, it is fully faithful.
     δ : F => G
     δ .η b = mkT b .fst
     δ .is-natural b b′ f = ∥-∥-elim₂
-      {P = λ α β → ∥-∥-proj {ap = T-prop b′} (mkT′ b′ α) .fst C.∘ F.₁ f
-                 ≡ G.₁ f C.∘ ∥-∥-proj {ap = T-prop b} (mkT′ b β) .fst}
+      {P = λ α β → ∥-∥-proj (T-prop b′) (mkT′ b′ α) .fst C.∘ F.₁ f
+                 ≡ G.₁ f C.∘ ∥-∥-proj (T-prop b) (mkT′ b β) .fst}
       (λ _ _ → C.Hom-set _ _ _ _)
       (λ (a′ , h′) (a , h) → naturality f a a′ h h′) (H-eso b′) (H-eso b)
 
   full : is-full (precompose H)
   full {x = x} {y = y} γ = pure (δ _ _ γ , Nat-path p) where
     p : ∀ b → δ _ _ γ .η (H.₀ b) ≡ γ .η b
     p b = subst
-      (λ e → ∥-∥-proj {ap = T-prop _ _ γ (H.₀ b)} (mkT′ _ _ γ (H.₀ b) e) .fst
+      (λ e → ∥-∥-proj (T-prop _ _ γ (H.₀ b)) (mkT′ _ _ γ (H.₀ b) e) .fst
            ≡ γ .η b)
       (squash (inc (b , B.id-iso)) (H-eso (H.₀ b)))
       (C.eliml (y .F-id) ∙ C.elimr (x .F-id))
@@ -377,7 +377,7 @@ candidate over it.
 <!--
 ```agda
     summon : ∀ {b} → ∥ Essential-fibre H b ∥ → is-contr (Obs b)
-    summon f = ∥-∥-proj {ap = is-contr-is-prop} do
+    summon f = ∥-∥-proj is-contr-is-prop do
       f ← f
       pure $ contr (obj′ f) (Obs-is-prop f)
 
@@ -488,7 +488,7 @@ This proof _really_ isn't commented. I'm sorry.
         (λ _ → compat-prop f) (sym (Homs-prop′ f _ _ _ _ h′)))
 
     Homs-contr : ∀ {b b′} (f : B.Hom b b′) → is-contr (Homs f)
-    Homs-contr f = ∥-∥-proj (Homs-contr′ f)
+    Homs-contr f = ∥-∥-proj! (Homs-contr′ f)
 
     G₁ : ∀ {b b′} → B.Hom b b′ → C.Hom (G₀ b) (G₀ b′)
     G₁ f = Homs-contr f .centre .fst
@@ -552,7 +552,7 @@ a set --- a proposition --- these choices don't matter, so we can use
 essential surjectivity of $H$.
 
 ```agda
-    G .F-∘ {x} {y} {z} f g = ∥-∥-proj do
+    G .F-∘ {x} {y} {z} f g = ∥-∥-proj! do
       (ax , hx) ← H-eso x
       (ay , hy) ← H-eso y
       (az , hz) ← H-eso z

src/Data/Fin/Finite.lagda.md

@@ -93,11 +93,11 @@ open Finite ⦃ ... ⦄ public
 instance
   H-Level-Finite : ∀ {ℓ} {A : Type ℓ} {n : Nat} → H-Level (Finite A) (suc n)
   H-Level-Finite = prop-instance {T = Finite _} λ where
-    x y i .Finite.cardinality → ∥-∥-proj
+    x y i .Finite.cardinality → ∥-∥-proj!
       ⦇ Fin-injective (⦇ ⦇ x .enumeration e⁻¹ ⦈ ∙e y .enumeration ⦈) ⦈
       i
     x y i .Finite.enumeration → is-prop→pathp
-      {B = λ i → ∥ _ ≃ Fin (∥-∥-proj ⦇ Fin-injective (⦇ ⦇ x .enumeration e⁻¹ ⦈ ∙e y .enumeration ⦈) ⦈ i) ∥}
+      {B = λ i → ∥ _ ≃ Fin (∥-∥-proj! ⦇ Fin-injective (⦇ ⦇ x .enumeration e⁻¹ ⦈ ∙e y .enumeration ⦈) ⦈ i) ∥}
       (λ _ → squash)
       (x .enumeration) (y .enumeration) i
 
@@ -146,7 +146,7 @@ private
     .snd .is-iso.rinv fzero → refl
     .snd .is-iso.linv x → funext λ { () }
 
-  finite-pi-fin (suc sz) {B} fam = ∥-∥-proj $ do
+  finite-pi-fin (suc sz) {B} fam = ∥-∥-proj! $ do
     e ← finite-choice (suc sz) λ x → fam x .enumeration
     let rest = finite-pi-fin sz (λ x → fam (fsuc x))
     cont ← rest .Finite.enumeration
@@ -167,13 +167,13 @@ Finite-⊎ {A = A} {B = B} = fin $ do
   beq ← enumeration {T = B}
   pure (⊎-ap aeq beq ∙e Finite-coproduct)
 
-Finite-Π {A = A} {P = P} ⦃ fin {sz} en ⦄ ⦃ fam ⦄ = ∥-∥-proj $ do
+Finite-Π {A = A} {P = P} ⦃ fin {sz} en ⦄ ⦃ fam ⦄ = ∥-∥-proj! $ do
   eqv ← en
   let count = finite-pi-fin sz λ x → fam $ equiv→inverse (eqv .snd) x
   eqv′ ← count .Finite.enumeration
   pure $ fin $ pure $ Π-dom≃ (eqv e⁻¹) ∙e eqv′
 
-Finite-Σ {A = A} {P = P} ⦃ afin ⦄ ⦃ fam ⦄ = ∥-∥-proj $ do
+Finite-Σ {A = A} {P = P} ⦃ afin ⦄ ⦃ fam ⦄ = ∥-∥-proj! $ do
   aeq ← afin .Finite.enumeration
   let
     module aeq = Equiv aeq

src/Data/Rel/Base.lagda.md

@@ -0,0 +1,126 @@
+<!--
+```agda
+open import 1Lab.Prelude
+open import Data.Sum
+```
+-->
+
+```agda
+module Data.Rel.Base where
+```
+
+# Relations
+
+A **relation** between types $A$ and $B$ consists of a family of types
+indexed by $A$ and $B$.
+
+```agda
+Rel : ∀ {a b} → Type a → Type b → (ℓ : Level) → Type _
+Rel A B ℓ = A → B → Type ℓ
+```
+
+<!--
+```agda
+private variable
+  ℓ ℓ' : Level
+  A B C : Type ℓ
+  R S T : Rel A B ℓ
+```
+-->
+
+We say that a relation is **propositional** if $R(x,y)$ is a proposition
+for every $x$ and $y$.
+
+```agda
+is-prop-rel : Rel A B ℓ → Type _
+is-prop-rel R = ∀ {x y} → is-prop (R x y)
+```
+
+## Operations on Propositional Relations
+
+We can take the union of two propositional relations by taking the
+pointwise truncated
+coproduct.
+
+```agda
+_∪r_ : Rel A B ℓ → Rel A B ℓ' → Rel A B _
+R ∪r S = λ x y → ∥ R x y ⊎ S x y ∥
+```
+
+Likewise, intersection can be defined by taking the pointwise product
+of the two relations.
+
+```agda
+_∩r_ : Rel A B ℓ → Rel A B ℓ' → Rel A B _
+R ∩r S = λ x y → R x y × S x y
+```
+
+We can compose two propositional relations by requiring the (mere)
+existence of a common endpoint.
+
+```agda
+_∘r_ : Rel B C ℓ → Rel A B ℓ' → Rel A C _
+R ∘r S = λ x y → ∃[ z ∈ _ ] (S x z × R z y)
+```
+
+Every relation between $A$ and $B$ can be flipped to get a relation
+between $B$ and $A$.
+
+```agda
+flipr : Rel A B ℓ → Rel B A ℓ
+flipr R = λ x y → R y x
+```
+
+## Relationships between Relations
+
+We say that a relation $R$ is contained in another relation $S$
+if $R(x,y)$ implies $S(x,y)$ for every $x$ and $y$.
+
+```agda
+_⊆r_ : Rel A B ℓ → Rel A B ℓ' → Type _
+R ⊆r S = ∀ {x y} → R x y → S x y
+
+_≃r_ : Rel A B ℓ → Rel A B ℓ' → Type _
+R ≃r S = ∀ {x y} → R x y ≃ S x y
+```
+
+```agda
+⊆r-trans : R ⊆r S → S ⊆r T → R ⊆r T 
+⊆r-trans p q Rxy = q (p Rxy)
+```
+
+
+Equality of propositional relations can be characterised in terms
+of containment.
+
+```agda
+prop-rel-ext
+  : is-prop-rel R → is-prop-rel S
+  → R ⊆r S → S ⊆r R → R ≡ S
+prop-rel-ext R-prop S-prop R⊆S S⊆R =
+  funext λ x → funext λ y → ua (prop-ext R-prop S-prop R⊆S S⊆R)
+```
+
+## Properties of Relations
+
+A relation is **reflexive** if every element is related to itself.
+
+```agda
+is-reflexive : Rel A A ℓ → Type _
+is-reflexive R = ∀ x → R x x
+```
+
+A relation is **symmetric** if every $R(x,y)$ implies that $R(y,x)$.
+
+```agda
+is-symmetric : Rel A A ℓ → Type _
+is-symmetric R = ∀ {x y} → R x y → R y x
+```
+
+A relation is **transitive** if $R(x,y)$ and $R(y,z)$ implies that
+$R(x,z)$.
+
+```agda
+is-transitive : Rel A A ℓ → Type _
+is-transitive R = ∀ {x y z} → R x y → R y z → R x z
+```

src/Data/Rel/Closure.agda

@@ -0,0 +1,12 @@
+-- This module doesn't have any text! That's because it's simply a bunch
+-- of convenient re-exports for working with closures of relations
+
+module Data.Rel.Closure where
+
+open import Data.Rel.Base public
+open import Data.Rel.Closure.Base public
+open import Data.Rel.Closure.Reflexive public
+open import Data.Rel.Closure.Symmetric public
+open import Data.Rel.Closure.Transitive public
+open import Data.Rel.Closure.ReflexiveTransitive public
+open import Data.Rel.Closure.ReflexiveSymmetricTransitive public

src/Data/Rel/Closure/Base.lagda.md

@@ -0,0 +1,80 @@
+<!--
+```agda
+open import 1Lab.Prelude
+open import Data.Sum
+
+open import Data.Rel.Base
+
+import Data.Nat as Nat
+import Data.Nat.Order as Nat
+```
+-->
+
+```agda
+module Data.Rel.Closure.Base where
+```
+
+<!--
+```agda
+private variable
+  ℓ ℓ' ℓ'' : Level
+  A B X : Type ℓ
+  R R' S : A → A → Type ℓ
+```
+-->
+
+# Closures of relations
+
+A **closure operator** $-^{+}$ on relations takes a relation $R$ on a type
+$A$ to a new relation $R^{+}$ on $A$, where $R^{+}$ is the smallest
+relation containing $R$ that satisfies some property.
+
+Intuitively, the closure of a relation should enjoy the following properties:
+- If $R \subseteq S$, then $R^{+} \subseteq S^{+}$.
+- $R \subseteq R^{+}$
+- $(R^{+})^{+} \subseteq R^{+}$, as closing $R$ under a property twice shouldn't
+  add any more elements.
+
+This ends up forming a [monad], though we do not define a closure operator as
+such due to annoying size restrictions.
+
+[monad]: Cat.Diagram.Monad.html
+
+```agda
+record is-rel-closure
+  (K : ∀ {ℓ ℓ'} {A : Type ℓ} → Rel A A ℓ' → Rel A A (ℓ ⊔ ℓ'))
+  : Typeω where
+  field
+    monotone : R ⊆r S → K R ⊆r K S
+    extensive : R ⊆r K R
+    closed : K (K R) ⊆r K R
+    has-prop : is-prop-rel (K R)
+```
+
+Closure, monotonicity, and extensivity combine to give idempotence
+of the closure operator.
+
+```agda
+  idempotent : K (K R) ≡ K R
+  idempotent =
+    prop-rel-ext has-prop has-prop
+      closed
+      (monotone extensive)
+```
+
+We can also derive an extension operator using the normal formulation
+for monads.
+
+```agda
+  extend : S ⊆r K R → K S ⊆r K R
+  extend p kr = closed (monotone p kr)
+```
+
+We can leverage this to see that if $R \subseteq S \subseteq K R$, then
+$K R = K S$.
+
+```agda
+  ⊆+⊆-clo→≃ : S ⊆r R → R ⊆r K S → K R ≃r K S
+  ⊆+⊆-clo→≃ p q =
+    prop-ext has-prop has-prop  (extend q) (monotone p)
+```