Move just a few more things over to new Function hierarchy. (#2044)

Author: JacquesCarette

src/Data/List/Relation/Binary/Pointwise.agda

@@ -10,7 +10,7 @@ module Data.List.Relation.Binary.Pointwise where
 
 open import Algebra.Core using (Op₂)
 open import Function.Base
-open import Function.Inverse using (Inverse)
+open import Function.Bundles using (Inverse)
 open import Data.Bool.Base using (true; false)
 open import Data.Product.Base hiding (map)
 open import Data.List.Base as List hiding (map; head; tail; uncons)
@@ -269,10 +269,9 @@ Pointwise-≡⇒≡ (P.refl ∷ xs∼ys) with Pointwise-≡⇒≡ xs∼ys
 
 Pointwise-≡↔≡ : Inverse (setoid (P.setoid A)) (P.setoid (List A))
 Pointwise-≡↔≡ = record
-  { to         = record { _⟨$⟩_ = id; cong = Pointwise-≡⇒≡ }
-  ; from       = record { _⟨$⟩_ = id; cong = ≡⇒Pointwise-≡ }
-  ; inverse-of = record
-    { left-inverse-of  = λ _ → refl P.refl
-    ; right-inverse-of = λ _ → P.refl
-    }
+  { to = id
+  ; from = id
+  ; to-cong = Pointwise-≡⇒≡
+  ; from-cong = ≡⇒Pointwise-≡
+  ; inverse = Pointwise-≡⇒≡ , ≡⇒Pointwise-≡
   }

src/Data/List/Relation/Unary/All/Properties.agda

@@ -33,9 +33,9 @@ open import Data.Nat.Base using (zero; suc; s≤s; _<_; z<s; s<s)
 open import Data.Nat.Properties using (≤-refl; m≤n⇒m≤1+n)
 open import Data.Product.Base as Prod using (_×_; _,_; uncurry; uncurry′)
 open import Function.Base
+import Function.Bundles as B
 open import Function.Equality using (_⟨$⟩_)
 open import Function.Equivalence using (_⇔_; equivalence; Equivalence)
-open import Function.Inverse using (_↔_; inverse)
 open import Function.Surjection using (_↠_; surjection)
 open import Level using (Level)
 open import Relation.Binary as B using (REL; Setoid; _Respects_)
@@ -405,8 +405,8 @@ mapMaybe⁺ {xs = x ∷ xs} {f = f} (px ∷ pxs) with f x
 ++⁻ []       p          = [] , p
 ++⁻ (x ∷ xs) (px ∷ pxs) = Prod.map (px ∷_) id (++⁻ _ pxs)
 
-++↔ : (All P xs × All P ys) ↔ All P (xs ++ ys)
-++↔ {xs = zs} = inverse (uncurry ++⁺) (++⁻ zs) ++⁻∘++⁺ (++⁺∘++⁻ zs)
+++↔ : (All P xs × All P ys) B.↔ All P (xs ++ ys)
+++↔ {xs = zs} = B.mk↔′ (uncurry ++⁺) (++⁻ zs) (++⁺∘++⁻ zs) ++⁻∘++⁺
   where
   ++⁺∘++⁻ : ∀ xs (p : All P (xs ++ ys)) → uncurry′ ++⁺ (++⁻ xs p) ≡ p
   ++⁺∘++⁻ []       p          = refl

src/Data/Vec/Properties.agda

@@ -21,7 +21,8 @@ open import Data.Sum.Base using ([_,_]′)
 open import Data.Sum.Properties using ([,]-map)
 open import Data.Vec.Base
 open import Function.Base
-open import Function.Inverse using (_↔_; inverse)
+-- open import Function.Inverse using (_↔_; inverse)
+open import Function.Bundles using (_↔_; mk↔′)
 open import Level using (Level)
 open import Relation.Binary hiding (Decidable)
 open import Relation.Binary.PropositionalEquality
@@ -199,9 +200,8 @@ lookup⇒[]= zero    (_ ∷ _)  refl = here
 lookup⇒[]= (suc i) (_ ∷ xs) p    = there (lookup⇒[]= i xs p)
 
 []=↔lookup : ∀ {i} → xs [ i ]= x ↔ lookup xs i ≡ x
-[]=↔lookup {i = i} =
-  inverse []=⇒lookup (lookup⇒[]= _ _)
-          lookup⇒[]=∘[]=⇒lookup ([]=⇒lookup∘lookup⇒[]= _ i)
+[]=↔lookup {xs = ys} {i = i} =
+  mk↔′ []=⇒lookup (lookup⇒[]= i ys) ([]=⇒lookup∘lookup⇒[]= _ i) lookup⇒[]=∘[]=⇒lookup
   where
   lookup⇒[]=∘[]=⇒lookup : ∀ {i} (p : xs [ i ]= x) →
                           lookup⇒[]= i xs ([]=⇒lookup p) ≡ p
@@ -706,7 +706,7 @@ zip∘unzip []         = refl
 zip∘unzip (xy ∷ xys) = cong (xy ∷_) (zip∘unzip xys)
 
 ×v↔v× : (Vec A n × Vec B n) ↔ Vec (A × B) n
-×v↔v× = inverse (uncurry zip) unzip (uncurry unzip∘zip) zip∘unzip
+×v↔v× = mk↔′ (uncurry zip) unzip zip∘unzip (uncurry unzip∘zip)
 
 ------------------------------------------------------------------------
 -- _⊛_

src/Data/Vec/Recursive/Properties.agda

@@ -13,7 +13,7 @@ open import Data.Nat.Base hiding (_^_)
 open import Data.Product
 open import Data.Vec.Recursive
 open import Data.Vec.Base using (Vec; _∷_)
-open import Function.Inverse using (_↔_; inverse)
+open import Function.Bundles using (_↔_; mk↔′)
 open import Relation.Binary.PropositionalEquality.Core as P
 open ≡-Reasoning
 
@@ -82,7 +82,7 @@ toVec∘fromVec {n = suc n} (x Vec.∷ xs) = begin
   tl-prf = tail-cons-identity _ x (fromVec xs)
 
 ↔Vec : ∀ n → A ^ n ↔ Vec A n
-↔Vec n = inverse (toVec n) fromVec (fromVec∘toVec n) toVec∘fromVec
+↔Vec n = mk↔′ (toVec n) fromVec toVec∘fromVec (fromVec∘toVec n)
 
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES