From e5aff0a8ddf8a32a61d2b4bfcaf3859ec52af5b6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jakub=20Kopa=C5=84ski?= <jakub@famisoft.pl>
Date: Mon, 8 Apr 2024 12:47:49 +0200
Subject: [PATCH 1/2] Make sure `Felix.Instances.Function.Lift` is typechecked

This module was omitted in `Felix.All` so it wasn't typechecked in the
CI.  This has led to it being broken with new instance resolution
algorithm.  Now it shouldn't get out of sync.
---
 src/Felix/All.agda | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Felix/All.agda b/src/Felix/All.agda
index 8837fe1..bfabf06 100644
--- a/src/Felix/All.agda
+++ b/src/Felix/All.agda
@@ -20,4 +20,5 @@ import Felix.Construct.Comma
 import Felix.Construct.Arrow
 
 import Felix.Instances.Function
+import Felix.Instances.Function.Lift
 import Felix.Instances.Identity

From 220753e069193f6324ba7ccc7764c5e0264d48d9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jakub=20Kopa=C5=84ski?= <jakub@famisoft.pl>
Date: Mon, 8 Apr 2024 12:50:31 +0200
Subject: [PATCH 2/2] Adjust `Felix.Instances.Function.Lift` to new instance
 resolution

---
 src/Felix/Instances/Function/Lift.agda | 24 +++++++++++++++---------
 1 file changed, 15 insertions(+), 9 deletions(-)

diff --git a/src/Felix/Instances/Function/Lift.agda b/src/Felix/Instances/Function/Lift.agda
index 1b89acc..c9fbcbe 100644
--- a/src/Felix/Instances/Function/Lift.agda
+++ b/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