From a7214fcc66e6ca1a8ad95fcd9ff43cdac0acc16e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Mon, 12 Mar 2018 13:51:29 +0100
Subject: [PATCH] Finish equality principle for categories

---
 src/Cat/Category.agda | 23 ++++++++---------------
 1 file changed, 8 insertions(+), 15 deletions(-)

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 5a13f41..5b2f025 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -38,7 +38,7 @@ open import Data.Product renaming
 open import Data.Empty
 import Function
 open import Cubical
-open import Cubical.NType.Properties using ( propIsEquiv )
+open import Cubical.NType.Properties using ( propIsEquiv ; lemPropF )
 
 open import Cat.Wishlist
 
@@ -195,9 +195,9 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
 --
 -- Proves that all projections of `IsCategory` are mere propositions as well as
 -- `IsCategory` itself being a mere proposition.
-module Propositionality {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
-  open RawCategory C
-  module _ (ℂ : IsCategory C) where
+module Propositionality {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
+  open RawCategory ℂ
+  module _ (ℂ : IsCategory ℂ) where
     open IsCategory ℂ using (isAssociative ; arrowsAreSets ; isIdentity ; Univalent)
     open import Cubical.NType
     open import Cubical.NType.Properties
@@ -241,11 +241,11 @@ module Propositionality {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
     propUnivalent a b i = propPi (λ iso → propHasLevel ⟨-2⟩) a b i
 
   private
-    module _ (x y : IsCategory C) where
+    module _ (x y : IsCategory ℂ) where
       module IC = IsCategory
       module X = IsCategory x
       module Y = IsCategory y
-      open Univalence C
+      open Univalence ℂ
       -- In a few places I use the result of propositionality of the various
       -- projections of `IsCategory` - I've arbitrarily chosed to use this
       -- result from `x : IsCategory C`. I don't know which (if any) possibly
@@ -275,7 +275,7 @@ module Propositionality {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
       IC.arrowsAreSets (done i) = propArrowIsSet x X.arrowsAreSets Y.arrowsAreSets i
       IC.univalent     (done i) = eqUni i
 
-  propIsCategory : isProp (IsCategory C)
+  propIsCategory : isProp (IsCategory ℂ)
   propIsCategory = done
 
 -- | Univalent categories
@@ -297,15 +297,8 @@ module _ {ℓa ℓb : Level} {ℂ 𝔻 : Category ℓa ℓb} where
 
   module _ (rawEq : ℂ.raw ≡ 𝔻.raw) where
     private
-      P : (target : RawCategory ℓa ℓb) → ({!!} ≡ target) → Set _
-      P _ eq = ∀ isCategory' → (λ i → IsCategory (eq i)) [ ℂ.isCategory ≡ isCategory' ]
-
-      p : P ℂ.raw refl
-      p isCategory' = Propositionality.propIsCategory {!!} {!!}
-
-      -- TODO Make and use heterogeneous version of Category≡
       isCategoryEq : (λ i → IsCategory (rawEq i)) [ ℂ.isCategory ≡ 𝔻.isCategory ]
-      isCategoryEq = {!!}
+      isCategoryEq = lemPropF Propositionality.propIsCategory rawEq
 
     Category≡ : ℂ ≡ 𝔻
     Category≡ i = record