{-# OPTIONS --without-K #-}

module Iff where

open import lib.Base public
open import lib.types.Sigma public

{- Standard notation: if and only if. -}

_⇔_ :  {j₁ j₂}  Set j₁  Set j₂  Set (lmax j₁ j₂)
A  B = (A  B) × (B  A)