get rid of biimp (#476)

Just gets rid of the biimplication type since it's now basically
needless verbosity

Author: plt-amy

src/1Lab/Biimp.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/Equiv.lagda.md

@@ -30,8 +30,6 @@ 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/Prelude.agda

@@ -11,7 +11,6 @@ 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
@@ -93,36 +92,25 @@ instance
 ```
 -->
 
-We can also prove a univalence principle for `Ω`{.Agda}: if
-$A, B : \Omega$ are [[logically equivalent|logical-equivalence]],
-then they are equal.
+We can also prove a univalence principle for `Ω`{.Agda}: if $A, B :
+\Omega$ are logically equivalent, then they are equal.
 
 ```agda
-Ω-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})
+Ω-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})
     (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 id↔)
+    (λ x → Ω-ua id 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.
@@ -222,7 +210,7 @@ to-is-true
   : ∀ {P Q : Ω} ⦃ _ : H-Level ∣ Q ∣ 0 ⦄
   → ∣ P ∣
   → P ≡ Q
-to-is-true prf = Ω-ua (biimp (λ _ → hlevel 0 .centre) λ _ → prf)
+to-is-true prf = Ω-ua (λ _ → hlevel 0 .centre) λ _ → prf
 
 tr-□ : ∀ {ℓ} {A : Type ℓ} → ∥ A ∥ → □ A
 tr-□ (inc x) = inc x
@@ -268,10 +256,6 @@ _→Ω_ : Ω → Ω → Ω
 ∣ P →Ω Q ∣ = ∣ P ∣ → ∣ Q ∣
 (P →Ω Q) .is-tr = hlevel 1
 
-_↔Ω_ : Ω → Ω → Ω
-∣ P ↔Ω Q ∣ = ∣ P ∣ ↔ ∣ Q ∣
-(P ↔Ω Q) .is-tr = hlevel 1
-
 ¬Ω_ : Ω → Ω
 ¬Ω P = P →Ω ⊥Ω
 ```

src/1Lab/Resizing.lagda.md

@@ -219,7 +219,7 @@ 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 → biimp
+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))
 ```
@@ -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 → biimp
+Rel ℓ .cat .idl R = ext λ x y → Ω-ua
   (rec! λ z x~z z=y → subst (λ e → ∣ R x e ∣) z=y x~z)
   (λ w → inc (y , w , inc refl))
 
-Rel ℓ .cat .assoc T S R = ext λ x y → biimp
+Rel ℓ .cat .assoc T S R = ext λ x y → Ω-ua
   (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 → biimp (p x y) (q x y)
+Rel ℓ .≤-antisym p q = ext λ x y → Ω-ua (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 → biimp
+Rel ℓ .dual-∘ = ext λ x y → Ω-ua
   (□-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/Allegory/Base.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 → biimp
+    pullback-id {s = s} = ext λ h → Ω-ua
       (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 → biimp
+    pullback-∘ {f = f} {g} {R = R} = ext λ h → Ω-ua
       (subst (_∈ R) (sym (C.assoc g f h)))
       (subst (_∈ R) (C.assoc g f h))
 ```

src/Cat/Diagram/Sieve.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 → biimp
+      rem₁ = ext λ {V} h → Ω-ua
         (λ (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 biimp (λ h∈S → cT h (rem₂' h∈S)) (λ h∈T → cS h (rem₃ h∈T))
+    in Ω-ua (λ 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 → biimp
+    restrict f hf = ext λ {V} h → Ω-ua
       (rec! λ α →
         let
           step₁ : id ∈ S .part (f ∘ h ∘ id) (⟦ R ⟧ .closed hf (h ∘ id)) .fst

src/Cat/Instances/Sheaves/Omega.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 → biimp (λ fhR → fhR , S .closed hf _) fst)) (pull f α))
+      (λ {V} f hf → subst (J ∋_) (ext (λ h → Ω-ua (λ fhR → fhR , S .closed hf _) fst)) (pull f α))
 ```
 -->
 

src/Cat/Site/Closure.lagda.md

@@ -360,7 +360,7 @@ proposition $P$ to the sieve which contains any $h$ iff $P$.
 
 <!--
 ```agda
-    m1 .is-natural x y f = ext λ S cl → biimp
+    m1 .is-natural x y f = ext λ S cl → Ω-ua
       (λ hf → cl id (inc (pullback id S , inc (y , f , subst (_∈ S) id-comm hf))))
       (λ hid → subst (_∈ S) id-comm-sym (S .closed hid f))
 
@@ -377,7 +377,7 @@ direction is definitional, and the other is not much more complicated.
   ΩJ-is-constant : ΩJ cov Sh.≅ ΩJ'
   ΩJ-is-constant =
     let
-      q = ext λ i X cl → Σ-prop-path! $ ext λ x → biimp
+      q = ext λ i X cl → Σ-prop-path! $ ext λ x → Ω-ua
         (λ p → subst (_∈ X) (idl _) (X .closed p _))
         (λ p → cl id (inc (_ , inc (_ , _ , subst (_∈ X) id-comm (X .closed p id)))))
     in Sh.make-iso m1 m2 trivial! q

src/Cat/Site/Instances/Atomic.lagda.md

@@ -83,7 +83,7 @@ computed *is* the pullback sieve.
   generate-∩
     : ∀ {U V} (h : V ≤ U) (S : Covering U)
     → generate (∩-covering h S) ≡ pullback h (generate S)
-  generate-∩ V≤U (I , f , p) = ext λ {W} W≤V → biimp
+  generate-∩ V≤U (I , f , p) = ext λ {W} W≤V → Ω-ua
     (rec! λ i W≤fi∩V → inc (i , ≤-trans W≤fi∩V ∩≤l))
     (rec! λ i W≤fi   → inc (i , ∩-universal _ W≤fi W≤V))
 

src/Cat/Site/Instances/Frame.lagda.md

@@ -90,7 +90,7 @@ part-ext
   → (∀ xd yd → x .elt xd ≡ y .elt yd)
   → x ≡ y
 part-ext to from p = Part-pathp refl
-  (Ω-ua (biimp to from)) (funext-dep λ _ → p _ _)
+  (Ω-ua to from) (funext-dep λ _ → p _ _)
 ```
 
 To close the initial definitions, if we have a partial element $x : \zap

src/Data/Partial/Base.lagda.md

@@ -60,8 +60,7 @@ propositions to each inhabitant of $X$.
 ```agda
 ℙ-ext : {A B : ℙ X}
       → A ⊆ B → B ⊆ A → A ≡ B
-ℙ-ext {A = A} {B = B} A⊆B B⊂A = funext λ x →
-  Ω-ua (biimp (A⊆B x) (B⊂A x))
+ℙ-ext {A = A} {B = B} A⊆B B⊂A = funext λ x → Ω-ua (A⊆B x) (B⊂A x)
 ```
 
 ## Lattice structure

src/Data/Power.lagda.md

@@ -303,7 +303,7 @@ Power-frame A .snd .has-top =
 Power-frame A .snd .⋃ k i = ∃Ω _ (λ j → k j i)
 Power-frame A .snd .⋃-lubs k = is-lub-pointwise _ _ λ _ →
   Props-has-lubs λ i → k i _
-Power-frame A .snd .⋃-distribl x f = ext λ i → biimp
+Power-frame A .snd .⋃-distribl x f = ext λ i → Ω-ua
   (rec! λ xi j j~i → inc (j , xi , j~i))
   (rec! λ j xi j~i → xi , inc (j , j~i))
 ```

src/Order/Frame.lagda.md

@@ -79,7 +79,7 @@ Lower-sets-frame (P , L) = Lower-sets P , L↓-frame where
   L↓-frame .is-frame.has-top = Lower-sets-top P
   L↓-frame .is-frame.⋃ k = Lower-sets-cocomplete P k .Lub.lub
   L↓-frame .is-frame.⋃-lubs k = Lower-sets-cocomplete P k .Lub.has-lub
-  L↓-frame .is-frame.⋃-distribl x f = ext λ arg → biimp
+  L↓-frame .is-frame.⋃-distribl x f = ext λ arg → Ω-ua
     (rec! λ x≤a i fi≤a → inc (i , x≤a , fi≤a))
     (rec! λ i x≤a fi≤a → x≤a , inc (i , fi≤a))
 ```

src/Order/Frame/Free.lagda.md

@@ -44,7 +44,7 @@ Props .Poset._≤_ P Q = ∣ P ∣ → ∣ Q ∣
 Props .Poset.≤-thin = hlevel 1
 Props .Poset.≤-refl x = x
 Props .Poset.≤-trans g f x = f (g x)
-Props .Poset.≤-antisym p q = ext (biimp p q)
+Props .Poset.≤-antisym p q = ext (Ω-ua p q)
 ```
 
 The poset of propositions a top and bottom element, as well as