From ed32ce5454d257a3909213421c7be219e073ab58 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Wed, 26 Feb 2025 10:58:30 +0100
Subject: [PATCH] liftC C is equivalent to C

---
 src/Categories/Category/Lift/Properties.agda | 39 ++++++++++++++++++++
 1 file changed, 39 insertions(+)
 create mode 100644 src/Categories/Category/Lift/Properties.agda

diff --git a/src/Categories/Category/Lift/Properties.agda b/src/Categories/Category/Lift/Properties.agda
new file mode 100644
index 00000000..81a9368c
--- /dev/null
+++ b/src/Categories/Category/Lift/Properties.agda
@@ -0,0 +1,39 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Categories.Category.Lift.Properties where
+
+open import Level
+
+open import Categories.Category.Core
+open import Categories.Category.Equivalence
+open import Categories.Category.Lift
+open import Categories.NaturalTransformation.NaturalIsomorphism
+import Categories.Morphism.Reasoning.Core as MR
+
+unliftF-liftF-weakInverse : ∀ {o ℓ e} o′ ℓ′ e′ (C : Category o ℓ e) → WeakInverse (unliftF o′ ℓ′ e′ C) (liftF o′ ℓ′ e′ C)
+unliftF-liftF-weakInverse o′ ℓ′ e′ C = record
+  { F∘G≈id = niHelper record
+    { η = λ X → id
+    ; η⁻¹ = λ X → id
+    ; commute = λ f → id-comm-sym
+    ; iso = λ X → record
+      { isoˡ = identity²
+      ; isoʳ = identity²
+      }
+    }
+  ; G∘F≈id = niHelper record
+    { η = λ X → lift id
+    ; η⁻¹ = λ X → lift id
+    ; commute = λ f → lift id-comm-sym
+    ; iso = λ X → record
+      { isoˡ = lift identity²
+      ; isoʳ = lift identity²
+      }
+    }
+  }
+  where
+    open Category C
+    open MR C
+
+liftC-strongEquivalence : ∀ {o ℓ e} o′ ℓ′ e′ (C : Category o ℓ e) → StrongEquivalence (liftC o′ ℓ′ e′ C) C
+liftC-strongEquivalence o′ ℓ′ e′ C = record { weak-inverse = unliftF-liftF-weakInverse o′ ℓ′ e′ C }