From a321a9c8b2831001327ec37620d754dda26d3a08 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Fri, 23 Feb 2018 13:36:54 +0100
Subject: [PATCH] Use hLevels in Fam

---
 src/Cat/Categories/Fam.agda | 43 ++++++++++++++++++-------------------
 1 file changed, 21 insertions(+), 22 deletions(-)

diff --git a/src/Cat/Categories/Fam.agda b/src/Cat/Categories/Fam.agda
index 6150dd2..7727a6d 100644
--- a/src/Cat/Categories/Fam.agda
+++ b/src/Cat/Categories/Fam.agda
@@ -3,9 +3,11 @@ module Cat.Categories.Fam where
 
 open import Agda.Primitive
 open import Data.Product
-open import Cubical
 import Function
 
+open import Cubical
+open import Cubical.Universe
+
 open import Cat.Category
 open import Cat.Equality
 
@@ -13,38 +15,35 @@ open Equality.Data.Product
 
 module _ (ℓa ℓb : Level) where
   private
-    Obj' = Σ[ A ∈ Set ℓa ] (A → Set ℓb)
-    Arr : Obj' → Obj' → Set (ℓa ⊔ ℓb)
-    Arr (A , B) (A' , B') = Σ[ f ∈ (A → A') ] ({x : A} → B x → B' (f x))
-    one : {o : Obj'} → Arr o o
-    proj₁ one = λ x → x
-    proj₂ one = λ b → b
-    _∘_ : {a b c : Obj'} → Arr b c → Arr a b → Arr a c
+    Object = Σ[ hA ∈ hSet {ℓa} ] (proj₁ hA → hSet {ℓb})
+    Arr : Object → Object → Set (ℓa ⊔ ℓb)
+    Arr ((A , _) , B) ((A' , _) , B') = Σ[ f ∈ (A → A') ] ({x : A} → proj₁ (B x) → proj₁ (B' (f x)))
+    𝟙 : {A : Object} → Arr A A
+    proj₁ 𝟙 = λ x → x
+    proj₂ 𝟙 = λ b → b
+    _∘_ : {a b c : Object} → Arr b c → Arr a b → Arr a c
     (g , g') ∘ (f , f') = g Function.∘ f , g' Function.∘ f'
-    _⟨_∘_⟩ : {a b : Obj'} → (c : Obj') → Arr b c → Arr a b → Arr a c
-    c ⟨ g ∘ f ⟩ = _∘_ {c = c} g f
-
-    module _ {A B C D : Obj'} {f : Arr A B} {g : Arr B C} {h : Arr C D} where
-      isAssociative : (D ⟨ h ∘ C ⟨ g ∘ f ⟩ ⟩) ≡ D ⟨ D ⟨ h ∘ g ⟩ ∘ f ⟩
-      isAssociative = Σ≡ refl refl
-
-    module _ {A B : Obj'} {f : Arr A B} where
-      isIdentity : B ⟨ f ∘ one ⟩ ≡ f × B ⟨ one {B} ∘ f ⟩ ≡ f
-      isIdentity = (Σ≡ refl refl) , Σ≡ refl refl
-
 
     RawFam : RawCategory (lsuc (ℓa ⊔ ℓb)) (ℓa ⊔ ℓb)
     RawFam = record
-      { Object = Obj'
+      { Object = Object
       ; Arrow = Arr
-      ; 𝟙 = one
+      ; 𝟙 = λ { {A} → 𝟙 {A = A}}
       ; _∘_ = λ {a b c} → _∘_ {a} {b} {c}
       }
 
+    open RawCategory RawFam hiding (Object ; 𝟙)
+
+    isAssociative : IsAssociative
+    isAssociative = Σ≡ refl refl
+
+    isIdentity : IsIdentity λ { {A} → 𝟙 {A} }
+    isIdentity = (Σ≡ refl refl) , Σ≡ refl refl
+
     instance
       isCategory : IsCategory RawFam
       isCategory = record
-        { isAssociative = λ {A} {B} {C} {D} {f} {g} {h} → isAssociative {D = D} {f} {g} {h}
+        { isAssociative = λ {A} {B} {C} {D} {f} {g} {h} → isAssociative {A} {B} {C} {D} {f} {g} {h}
         ; isIdentity = λ {A} {B} {f} → isIdentity {A} {B} {f = f}
         ; arrowsAreSets = {!!}
         ; univalent = {!!}