def: define biimplications

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 α))
 ```
 -->