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

module 1Lab.Biimp where

BiimplicationsπŸ”—

A biimplication between a pair of types is a pair of functions 

record _↔_ {β„“} {β„“'} (A : Type β„“) (B : Type β„“') : Type (β„“ βŠ” β„“') where
  no-eta-equality
  constructor biimp
  field
    to : A β†’ B
    from : B β†’ A

open _↔_

private variable
  β„“ β„“' : Level
  A B C : Type β„“

module Biimp (f : A ↔ B) where
  open _↔_ f public

If and n-types, then the type of biimplications is also an n-type.

private unquoteDecl eqv = declare-record-iso eqv (quote _↔_)

↔-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)

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.

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 induces a biimplication 

_↔⁻¹ : A ↔ B β†’ B ↔ A
(f ↔⁻¹) .to = f .from
(f ↔⁻¹) .from = f .to

Biimplications and equivalencesπŸ”—

Every equivalence is a biimplication.

equivβ†’biimp : A ≃ B β†’ A ↔ B
equiv→biimp f .to = Equiv.to f
equiv→biimp f .from = Equiv.from f

Every biimplication between propositions is an equivalence. In light of this, biimplications are often referred to as logical equivalences.

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)

infix 21 _↔_
infixr 30 _βˆ™β†”_
infix 31 _↔⁻¹