Adjust Felix.Instances.Function.Lift to new instance resolution

src/Felix/Instances/Function/Lift.agda

@@ -5,26 +5,32 @@ open import Level
 module Felix.Instances.Function.Lift (a b : Level) where
 
 open Lift
-open import Data.Product using (_,_)
+open import Data.Product using (_,_; uncurry)
+open import Function using (_∘_)
 
-open import Felix.Homomorphism hiding (refl)
+open import Felix.Homomorphism
 open import Felix.Object
-
-private module F {ℓ} where open import Felix.Instances.Function ℓ public
-open F
+import Felix.Instances.Function
+open module F {ℓ} = Felix.Instances.Function ℓ
 
 private
   variable
     A : Set a
 
-lift₀ : ⦃ _ : Products (Set (a ⊔ b)) ⦄ → A → (⊤ F.⇾ Lift b A)
+lift₀′ : A → Lift b A
+lift₀′ = lift
+
+lift₀ : A → (⊤ ⇾ Lift b A)
 lift₀ n tt = lift n
 
-lift₁ : (A F.⇾ A) → (Lift b A F.⇾ Lift b A)
+lift₁ : (A ⇾ A) → (Lift b A ⇾ Lift b A)
 lift₁ f (lift a) = lift (f a)
 
-lift₂ : (A F.⇾ A F.⇾ A) → (Lift b A × Lift b A F.⇾ Lift b A)
-lift₂ f (lift a , lift b) = lift (f a b)
+lift₂′ : (A ⇾ A ⇾ A) → (Lift b A ⇾ Lift b A ⇾ Lift b A)
+lift₂′ f (lift a) (lift b) = lift (f a b)
+
+lift₂ : (A ⇾ A ⇾ A) → (Lift b A × Lift b A ⇾ Lift b A)
+lift₂ = uncurry ∘ lift₂′
 
 module function-lift-instances where instance