From ff496aae09dd5379a21787a68be8ea277f1b6626 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Tue, 20 Feb 2018 17:33:02 +0100
Subject: [PATCH] Factor out a useful type-family

---
 src/Cat/Category.agda | 17 ++++++++++++-----
 1 file changed, 12 insertions(+), 5 deletions(-)

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 6d60a4e..7896d02 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -143,13 +143,20 @@ module _ {ℓa} {ℓb} {ℂ : RawCategory ℓa ℓb} where
       module IC = IsCategory
       module X = IsCategory x
       module Y = IsCategory y
+      -- ident : X.ident {?} ≡ Y.ident
+      ident : (λ _ → IsIdentity 𝟙) [ X.ident ≡ Y.ident ]
       ident = X.propIsIdentity X.ident Y.ident
-      done : x ≡ y
-      T : I → Set (ℓa ⊔ ℓb)
-      T i = {A B : Object} →
+      -- A version of univalence indexed by the identity proof.
+      -- Not of course that since it's defined where `RawCategory ℂ` has been opened
+      -- this is specialized to that category.
+      Univ : IsIdentity 𝟙 → Set _
+      Univ idnt = {A B : Y.Raw.Object} →
         isEquiv (A ≡ B) (A ≅ B)
-        (λ eq → transp (λ i₁ → A ≅ eq i₁) (𝟙 , 𝟙 , ident i))
-      eqUni : T [ X.univalent ≡ Y.univalent ]
+        (λ eq → transp (λ j → A ≅ eq j) (𝟙 , 𝟙 , idnt))
+      done : x ≡ y
+      U : ∀ {a : IsIdentity 𝟙} → (λ _ → IsIdentity 𝟙) [ X.ident ≡ a ] → (b : Univ a) → Set _
+      U eqwal bbb = (λ i → Univ (eqwal i)) [ X.univalent ≡ bbb ]
+      eqUni : U ident Y.univalent
       eqUni = {!!}
       IC.assoc      (done i) = X.propIsAssociative X.assoc Y.assoc i
       IC.ident      (done i) = ident i