def: define biimplications (#457)

# Description

This PR defines a type of biimplications, and proves some basic
properties.

## Checklist

Before submitting a merge request, please check the items below:

- [x] I've read [the contributing
guidelines](https://github.com/plt-amy/1lab/blob/main/CONTRIBUTING.md).
- [x] The imports of new modules have been sorted with
`support/sort-imports.hs` (or `nix run --experimental-features
nix-command -f . sort-imports`).
- [x] All new code blocks have "agda" as their language.

If your change affects many files without adding substantial content,
and
you don't want your name to appear on those pages (for example, treewide
refactorings or reformattings), start the commit message and PR title
with `chore:`.

src/1Lab/Biimp.lagda.md

@@ -0,0 +1,143 @@
+---
+description: |
+  Biimplications.
+---
+<!--
+```agda
+open import 1Lab.Reflection.Record
+open import 1Lab.Extensionality
+open import 1Lab.HLevel.Closure
+open import 1Lab.HLevel
+open import 1Lab.Equiv
+open import 1Lab.Type
+
+open import Meta.Invariant
+```
+-->
+```agda
+module 1Lab.Biimp where
+```
+
+# Biimplications
+
+:::{.definition #biimplication}
+A **biimplication** $A \leftrightarrow B$ between a pair of types $A, B$
+is a pair of functions $A \to B, B \to A$.
+:::
+
+```agda
+record _↔_ {ℓ} {ℓ'} (A : Type ℓ) (B : Type ℓ') : Type (ℓ ⊔ ℓ') where
+  no-eta-equality
+  constructor biimp
+  field
+    to : A → B
+    from : B → A
+
+open _↔_
+```
+
+<!--
+```agda
+private variable
+  ℓ ℓ' : Level
+  A B C : Type ℓ
+```
+-->
+
+<!--
+```agda
+module Biimp (f : A ↔ B) where
+  open _↔_ f public
+```
+-->
+
+If $A$ and $B$ [[n-types]], then the type of biimplications $A \leftrightarrow B$
+is also an n-type.
+
+<!--
+```agda
+private unquoteDecl eqv = declare-record-iso eqv (quote _↔_)
+```
+-->
+
+```agda
+↔-is-hlevel : ∀ n → is-hlevel A n → is-hlevel B n → is-hlevel (A ↔ B) n
+↔-is-hlevel n A-hl B-hl =
+  Iso→is-hlevel n eqv $
+  ×-is-hlevel n
+    (Π-is-hlevel n λ _ → B-hl)
+    (Π-is-hlevel n λ _ → A-hl)
+```
+
+<!--
+```agda
+instance
+  H-Level-↔
+    : ∀ {n}
+    → ⦃ _ : H-Level A n ⦄ ⦃ _ : H-Level B n ⦄
+    → H-Level (A ↔ B) n
+  H-Level-↔ {n = n} .H-Level.has-hlevel =
+    ↔-is-hlevel n (hlevel n) (hlevel n)
+
+instance
+  Extensional-↔
+    : ∀ {ℓr}
+    → ⦃ _ : Extensional ((A → B) × (B → A)) ℓr ⦄
+    → Extensional (A ↔ B) ℓr
+  Extensional-↔ ⦃ e ⦄ = iso→extensional eqv e
+```
+-->
+
+## Working with biimplications
+
+There is an identity biimplication, and biimplications compose.
+
+```agda
+id↔ : A ↔ A
+id↔ .to = id
+id↔ .from = id
+
+_∙↔_ : A ↔ B → B ↔ C → A ↔ C
+(f ∙↔ g) .to = g .to ∘ f .to
+(f ∙↔ g) .from = f .from ∘ g .from
+```
+
+Moreover, every biimplication $A \leftrightarrow B$ induces a biimplication
+$B \leftrightarrow A$.
+
+```agda
+_↔⁻¹ : A ↔ B → B ↔ A
+(f ↔⁻¹) .to = f .from
+(f ↔⁻¹) .from = f .to
+```
+
+## Biimplications and equivalences
+
+Every [[equivalence]] is a biimplication.
+
+```agda
+equiv→biimp : A ≃ B → A ↔ B
+equiv→biimp f .to = Equiv.to f
+equiv→biimp f .from = Equiv.from f
+```
+
+:::{.definition #logical-equivalence}
+
+Every biimplication between [[propositions]] is an [[equivalence]].
+In light of this, biimplications are often referred to as
+**logical equivalences**.
+
+```agda
+biimp→equiv : is-prop A → is-prop B → A ↔ B → A ≃ B
+biimp→equiv A-prop B-prop f =
+  prop-ext A-prop B-prop (f .to) (f .from)
+```
+:::
+
+<!--
+```agda
+infix 21 _↔_
+infixr 30 _∙↔_
+infix 31 _↔⁻¹
+```
+-->

src/1Lab/Equiv.lagda.md

@@ -846,7 +846,7 @@ for which constructing equivalences is easy are the [[propositions]]. If
 $P$ and $Q$ are propositions, then any map $P \to P$ (resp. $Q \to Q$)
 must be homotopic to the identity, and consequently any pair of
 functions $P \to Q$ and $Q \to P$ is a pair of inverses. Put another
-way, any *biimplication* between propositions is an equivalence.
+way, any [[biimplication]] between propositions is an equivalence.
 
 ```agda
   biimp-is-equiv : (f : P → Q) → (Q → P) → is-equiv f

src/1Lab/Extensionality.agda

@@ -7,7 +7,6 @@ open import 1Lab.HIT.Truncation
 open import 1Lab.HLevel.Closure
 open import 1Lab.Reflection
 open import 1Lab.Type.Sigma
-open import 1Lab.Resizing
 open import 1Lab.Type.Pi
 open import 1Lab.HLevel
 open import 1Lab.Equiv
@@ -341,11 +340,6 @@ instance
     → ⦃ ea : Extensional A ℓr ⦄ → Extensional (Σ A λ x → ∥ B x ∥) ℓr
   Extensional-Σ-trunc ⦃ ea ⦄ = Σ-prop-extensional (λ x → hlevel 1) ea
 
-  Extensional-Σ-□
-    : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : A → Type ℓ'}
-    → ⦃ ea : Extensional A ℓr ⦄ → Extensional (Σ A λ x → □ (B x)) ℓr
-  Extensional-Σ-□ ⦃ ea ⦄ = Σ-prop-extensional (λ x → hlevel 1) ea
-
   Extensional-equiv
     : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : Type ℓ'}
     → ⦃ ea : Extensional (A → B) ℓr ⦄ → Extensional (A ≃ B) ℓr

src/1Lab/Prelude.agda

@@ -30,6 +30,8 @@ open import 1Lab.Function.Embedding public
 open import 1Lab.Function.Reasoning public
 open import 1Lab.Equiv.HalfAdjoint public
 
+open import 1Lab.Biimp public
+
 open import 1Lab.Function.Surjection public
 
 open import 1Lab.Univalence public

src/1Lab/Resizing.lagda.md

@@ -4,12 +4,14 @@ open import 1Lab.Function.Surjection
 open import 1Lab.Path.IdentitySystem
 open import 1Lab.Reflection.HLevel
 open import 1Lab.HLevel.Universe
+open import 1Lab.Extensionality
 open import 1Lab.HIT.Truncation
 open import 1Lab.HLevel.Closure
 open import 1Lab.Reflection using (arg ; typeError)
 open import 1Lab.Univalence
 open import 1Lab.Inductive
 open import 1Lab.HLevel
+open import 1Lab.Biimp
 open import 1Lab.Equiv
 open import 1Lab.Path
 open import 1Lab.Type
@@ -91,24 +93,36 @@ instance
 ```
 -->
 
-We can also prove a univalence principle for `Ω`{.Agda}:
+We can also prove a univalence principle for `Ω`{.Agda}: if
+$A, B : \Omega$ are [[logically equivalent|logical-equivalence]],
+then they are equal.
 
 ```agda
-Ω-ua : {A B : Ω} → (∣ A ∣ → ∣ B ∣) → (∣ B ∣ → ∣ A ∣) → A ≡ B
-Ω-ua {A} {B} f g i .∣_∣ = ua (prop-ext! f g) i
-Ω-ua {A} {B} f g i .is-tr =
-  is-prop→pathp (λ i → is-prop-is-prop {A = ua (prop-ext! f g) i})
+Ω-ua : {A B : Ω} → ∣ A ∣ ↔ ∣ B ∣ → A ≡ B
+Ω-ua {A} {B} f i .∣_∣ = ua (prop-ext! (Biimp.to f) (Biimp.from f)) i
+Ω-ua {A} {B} f i .is-tr =
+  is-prop→pathp (λ i → is-prop-is-prop {A = ua (prop-ext! (Biimp.to f) (Biimp.from f)) i})
     (A .is-tr) (B .is-tr) i
 
 instance abstract
   H-Level-Ω : ∀ {n} → H-Level Ω (2 + n)
   H-Level-Ω = basic-instance 2 $ retract→is-hlevel 2
     (λ r → el ∣ r ∣ (r .is-tr))
     (λ r → el ∣ r ∣ (r .is-tr))
-    (λ x → Ω-ua (λ x → x) λ x → x)
+    (λ x → Ω-ua id↔)
     (n-Type-is-hlevel {lzero} 1)
 ```
 
+<!--
+```agda
+instance
+  Extensionality-Ω : Extensional Ω lzero
+  Extensionality-Ω .Pathᵉ A B = ∣ A ∣ ↔ ∣ B ∣
+  Extensionality-Ω .reflᵉ A = id↔
+  Extensionality-Ω .idsᵉ = set-identity-system (λ _ _ → hlevel 1) Ω-ua
+```
+-->
+
 The `□`{.Agda} type former is a functor (in the handwavy sense that it
 supports a "map" operation), and can be projected from into propositions
 of any universe. These functions compute on `inc`{.Agda}s, as usual.
@@ -208,7 +222,7 @@ to-is-true
   : ∀ {P Q : Ω} ⦃ _ : H-Level ∣ Q ∣ 0 ⦄
   → ∣ P ∣
   → P ≡ Q
-to-is-true prf = Ω-ua (λ _ → hlevel 0 .centre) (λ _ → prf)
+to-is-true prf = Ω-ua (biimp (λ _ → hlevel 0 .centre) λ _ → prf)
 
 tr-□ : ∀ {ℓ} {A : Type ℓ} → ∥ A ∥ → □ A
 tr-□ (inc x) = inc x
@@ -223,7 +237,7 @@ tr-□ (squash x y i) = squash (tr-□ x) (tr-□ y) i
 ## Connectives
 
 The universe of small propositions contains true, false, conjunctions,
-disjunctions, and implications.
+disjunctions, and (bi)implications.
 
 <!--
 ```agda
@@ -254,6 +268,10 @@ _→Ω_ : Ω → Ω → Ω
 ∣ P →Ω Q ∣ = ∣ P ∣ → ∣ Q ∣
 (P →Ω Q) .is-tr = hlevel 1
 
+_↔Ω_ : Ω → Ω → Ω
+∣ P ↔Ω Q ∣ = ∣ P ∣ ↔ ∣ Q ∣
+(P ↔Ω Q) .is-tr = hlevel 1
+
 ¬Ω_ : Ω → Ω
 ¬Ω P = P →Ω ⊥Ω
 ```
@@ -274,6 +292,16 @@ syntax ∃Ω A (λ x → B) = ∃Ω[ x ∈ A ] B
 syntax ∀Ω A (λ x → B) = ∀Ω[ x ∈ A ] B
 ```
 
+<!--
+```agda
+instance
+  Extensional-Σ-□
+    : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : A → Type ℓ'}
+    → ⦃ ea : Extensional A ℓr ⦄ → Extensional (Σ A λ x → □ (B x)) ℓr
+  Extensional-Σ-□ ⦃ ea ⦄ = Σ-prop-extensional (λ x → hlevel 1) ea
+```
+-->
+
 These connectives and quantifiers are only provided for completeness;
 if you find yourself building nested propositions, it is generally a good
 idea to construct the large proposition by hand, and then use truncation

src/Cat/Allegory/Base.lagda.md

@@ -219,9 +219,9 @@ to show $R(x, y)$! Fortunately if we we set $\Id(x, a)$, then $R(x,
 y) \simeq R(a, y)$, and we're done.
 
 ```agda
-Rel ℓ .cat .idr {A} {B} R = ext λ x y → Ω-ua
-  (rec! λ a b w → subst (λ e → ∣ R e y ∣) (sym b) w)
-  λ w → inc (x , inc refl , w)
+Rel ℓ .cat .idr {A} {B} R = ext λ x y → biimp
+  (rec! (λ a b w → subst (λ e → ∣ R e y ∣) (sym b) w))
+  (λ w → inc (x , inc refl , w))
 ```
 
 The other interesting bits of the construction are meets, the dual, and
@@ -251,24 +251,24 @@ automatic proof search: that speaks to how contentful it is.</summary>
 
 ```agda
 Rel ℓ .cat .Hom-set x y = hlevel 2
-Rel ℓ .cat .idl R = ext λ x y → Ω-ua
+Rel ℓ .cat .idl R = ext λ x y → biimp
   (rec! λ z x~z z=y → subst (λ e → ∣ R x e ∣) z=y x~z)
-  λ w → inc (y , w , inc refl)
+  (λ w → inc (y , w , inc refl))
 
-Rel ℓ .cat .assoc T S R = ext λ x y → Ω-ua
+Rel ℓ .cat .assoc T S R = ext λ x y → biimp
   (rec! λ a b r s t → inc (b , r , inc (a , s , t)))
   (rec! λ a r b s t → inc (b , inc (a , r , s) , t))
 
 Rel ℓ .≤-thin = hlevel 1
 Rel ℓ .≤-refl x y w = w
 Rel ℓ .≤-trans x y p q z = y p q (x p q z)
-Rel ℓ .≤-antisym p q = ext λ x y → Ω-ua (p x y) (q x y)
+Rel ℓ .≤-antisym p q = ext λ x y → biimp (p x y) (q x y)
 
 Rel ℓ ._◆_ f g a b = □-map (λ { (x , y , w) → x , g a x y , f x b w })
 
 -- This is nice:
 Rel ℓ .dual R = refl
-Rel ℓ .dual-∘ = ext λ x y → Ω-ua
+Rel ℓ .dual-∘ = ext λ x y → biimp
   (□-map λ { (a , b , c) → a , c , b })
   (□-map λ { (a , b , c) → a , c , b })
 Rel ℓ .dual-≤ f≤g x y w = f≤g y x w

src/Cat/CartesianClosed/Lambda.lagda.md

@@ -23,7 +23,7 @@ module Cat.CartesianClosed.Lambda
         (cc : Cartesian-closed C fp term)
         where
 
-open Binary-products C fp hiding (unique₂)
+open Binary-products C fp
 open Cartesian-closed cc
 open Cat.Reasoning C
 ```

src/Cat/Diagram/Sieve.lagda.md

@@ -163,14 +163,14 @@ contravariant, this means that the assignment $U \mapsto
 ```agda
   abstract
     pullback-id : ∀ {c} {s : Sieve C c} → pullback C.id s ≡ s
-    pullback-id {s = s} = ext λ h → Ω-ua
+    pullback-id {s = s} = ext λ h → biimp
       (subst (_∈ s) (C.idl h))
       (subst (_∈ s) (sym (C.idl h)))
 
     pullback-∘
       : ∀ {u v w} {f : C.Hom w v} {g : C.Hom v u} {R : Sieve C u}
       → pullback (g C.∘ f) R ≡ pullback f (pullback g R)
-    pullback-∘ {f = f} {g} {R = R} = ext λ h → Ω-ua
+    pullback-∘ {f = f} {g} {R = R} = ext λ h → biimp
       (subst (_∈ R) (sym (C.assoc g f h)))
       (subst (_∈ R) (C.assoc g f h))
 ```

src/Cat/Instances/Sheaves/Omega.lagda.md

@@ -82,7 +82,7 @@ actually agree on their intersection with $R$:
   sep {U} R {S , cS} {T , cT} α = ext λ {V} h →
     let
       rem₁ : S ∩S ⟦ R ⟧ ≡ T ∩S ⟦ R ⟧
-      rem₁ = ext λ {V} h → Ω-ua
+      rem₁ = ext λ {V} h → biimp
         (λ (h∈S , h∈R) → cT h (subst (J ∋_) (ap fst (α h h∈R)) (max (S .closed h∈S id))) , h∈R)
         (λ (h∈T , h∈R) → cS h (subst (J ∋_) (ap fst (sym (α h h∈R))) (max (T .closed h∈T id))) , h∈R)
 ```
@@ -115,7 +115,7 @@ We omit the symmetric converse for brevity.
 -->
 
 ```agda
-    in Ω-ua (λ h∈S → cT h (rem₂' h∈S)) (λ h∈T → cS h (rem₃ h∈T))
+    in biimp (λ h∈S → cT h (rem₂' h∈S)) (λ h∈T → cS h (rem₃ h∈T))
 ```
 
 Now we have to show that a family $S$ of compatible closed sieves over a
@@ -152,7 +152,7 @@ are painful --- and entirely mechanical --- calculations.
 
 ```agda
     restrict : ∀ {V} (f : Hom V U) (hf : f ∈ R) → pullback f S' ≡ S .part f hf .fst
-    restrict f hf = ext λ {V} h → Ω-ua
+    restrict f hf = ext λ {V} h → biimp
       (rec! λ α →
         let
           step₁ : id ∈ S .part (f ∘ h ∘ id) (⟦ R ⟧ .closed hf (h ∘ id)) .fst

src/Cat/Site/Closure.lagda.md

@@ -280,7 +280,7 @@ sieve belongs to the saturation in at most one way.
       : ∀ {J : Coverage C ℓs} {U} {R S : Sieve C U}
       → J ∋ R → J ∋ S → J ∋ (R ∩S S)
     ∋-intersect {J = J} {R = R} {S = S} α β = local β
-      (λ {V} f hf → subst (J ∋_) (ext (λ h → Ω-ua (λ fhR → fhR , S .closed hf _) fst)) (pull f α))
+      (λ {V} f hf → subst (J ∋_) (ext (λ h → biimp (λ fhR → fhR , S .closed hf _) fst)) (pull f α))
 ```
 -->