Adjoint.Instance.0-Truncation: new function hierarchy

Didn't notice that I'd ended up in Functor.Instance in the previous commit

src/Categories/Adjoint/Instance/0-Truncation.agda

@@ -8,8 +8,9 @@ module Categories.Adjoint.Instance.0-Truncation where
 open import Level using (Lift)
 open import Data.Unit using (⊤)
 import Function
+open import Function.Bundles
+import Function.Construct.Identity as Id
 open import Relation.Binary using (Setoid)
-open import Function.Equality using (Π) renaming (id to idΠ)
 
 open import Categories.Adjoint using (_⊣_)
 open import Categories.Category.Construction.0-Groupoid using (0-Groupoid)
@@ -26,7 +27,7 @@ open import Categories.NaturalTransformation.NaturalIsomorphism using (refl)
 Inclusion : ∀ {c ℓ} e → Functor (Setoids c ℓ) (Groupoids c ℓ e)
 Inclusion {c} {ℓ} e = record
   { F₀           = 0-Groupoid e
-  ; F₁           = λ f → record { F₀ = f ⟨$⟩_ ; F₁ = cong f }
+  ; F₁           = λ f → record { F₀ = to f; F₁ = cong f }
   ; identity     = refl
   ; homomorphism = refl
   ; F-resp-≈     = λ {S T f g} f≗g →
@@ -37,7 +38,7 @@ Inclusion {c} {ℓ} e = record
     ; F⇐G = record { η = λ _ → T.sym (f≗g S.refl) }
     }
   }
-  where open Π
+  where open Func
 
 -- Trunc is left-adjoint to the inclusion functor from Setoids to Groupoids
 
@@ -49,7 +50,7 @@ TruncAdj {o} {ℓ} {e} = record
   ; zag    = refl
   }
   where
-    open Π
+    open Func
     open Groupoid using (category)
 
     unit : NaturalTransformation idF (Inclusion e ∘F Trunc)
@@ -60,4 +61,4 @@ TruncAdj {o} {ℓ} {e} = record
       }
 
     counit : NaturalTransformation (Trunc ∘F Inclusion e) idF
-    counit = ntHelper record { η = λ S → idΠ ; commute = λ f → cong f }
+    counit = ntHelper record { η = Id.function; commute = λ f → cong f }