diff --git a/src/Cat/Categories/Cube.agda b/src/Cat/Categories/Cube.agda
index 2cef72e..ec1a145 100644
--- a/src/Cat/Categories/Cube.agda
+++ b/src/Cat/Categories/Cube.agda
@@ -12,7 +12,7 @@ open import Function
 open import Relation.Nullary
 open import Relation.Nullary.Decidable
 
-open import Cat.Category hiding (Hom)
+open import Cat.Category
 open import Cat.Functor
 open import Cat.Equality
 open Equality.Data.Product
@@ -66,12 +66,14 @@ module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where
     Hom = Σ Hom' rules
 
   -- The category of names and substitutions
-  ℂ : Category ℓ ℓ -- ℓo (lsuc lzero ⊔ ℓo)
-  ℂ = record
+  Rawℂ : RawCategory ℓ ℓ -- ℓo (lsuc lzero ⊔ ℓo)
+  Rawℂ = record
     { Object = FiniteDecidableSubset
     -- { Object = Ns → Bool
     ; Arrow = Hom
     ; 𝟙 = λ { {o} → inj₁ , λ { (i , ii) (j , jj) eq → Σ≡ eq {!refl!} } }
     ; _∘_ = {!!}
-    ; isCategory = {!!}
     }
+  postulate RawIsCategoryℂ : IsCategory Rawℂ
+  ℂ : Category ℓ ℓ
+  ℂ = Rawℂ , RawIsCategoryℂ
diff --git a/src/Cat/Categories/Fam.agda b/src/Cat/Categories/Fam.agda
index 8e82369..9fac2bf 100644
--- a/src/Cat/Categories/Fam.agda
+++ b/src/Cat/Categories/Fam.agda
@@ -13,36 +13,42 @@ open Equality.Data.Product
 
 module _ (ℓa ℓb : Level) where
   private
-    Obj = Σ[ A ∈ Set ℓa ] (A → Set ℓb)
-    Arr : Obj → Obj → Set (ℓa ⊔ ℓb)
+    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
+    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
+    _∘_ : {a b c : Obj'} → 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
+    _⟨_∘_⟩ : {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
+    module _ {A B C D : Obj'} {f : Arr A B} {g : Arr B C} {h : Arr C D} where
       assoc : (D ⟨ h ∘ C ⟨ g ∘ f ⟩ ⟩) ≡ D ⟨ D ⟨ h ∘ g ⟩ ∘ f ⟩
       assoc = Σ≡ refl refl
 
-    module _ {A B : Obj} {f : Arr A B} where
+    module _ {A B : Obj'} {f : Arr A B} where
       ident : B ⟨ f ∘ one ⟩ ≡ f × B ⟨ one {B} ∘ f ⟩ ≡ f
       ident = (Σ≡ refl refl) , Σ≡ refl refl
 
+
+    RawFam : RawCategory (lsuc (ℓa ⊔ ℓb)) (ℓa ⊔ ℓb)
+    RawFam = record
+      { Object = Obj'
+      ; Arrow = Arr
+      ; 𝟙 = one
+      ; _∘_ = λ {a b c} → _∘_ {a} {b} {c}
+      }
+
     instance
-      isCategory : IsCategory Obj Arr one (λ {a b c} → _∘_ {a} {b} {c})
+      isCategory : IsCategory RawFam
       isCategory = record
         { assoc = λ {A} {B} {C} {D} {f} {g} {h} → assoc {D = D} {f} {g} {h}
         ; ident = λ {A} {B} {f} → ident {A} {B} {f = f}
+        ; arrow-is-set = ?
+        ; univalent = ?
         }
 
   Fam : Category (lsuc (ℓa ⊔ ℓb)) (ℓa ⊔ ℓb)
-  Fam = record
-    { Object = Obj
-    ; Arrow = Arr
-    ; 𝟙 = one
-    ; _∘_ = λ {a b c} → _∘_ {a} {b} {c}
-    }
+  Fam = RawFam , isCategory
diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda
index 8eb7918..3778cdb 100644
--- a/src/Cat/Categories/Fun.agda
+++ b/src/Cat/Categories/Fun.agda
@@ -53,7 +53,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
     𝔻 [ F→ f ∘ identityTrans F A ]  ∎
     where
       F→ = F .func→
-      module 𝔻 = IsCategory (𝔻 .isCategory)
+      module 𝔻 = IsCategory (isCategory 𝔻)
 
   identityNat : (F : Functor ℂ 𝔻) → NaturalTransformation F F
   identityNat F = identityTrans F , identityNatural F
@@ -75,7 +75,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
       𝔻 [ H .func→ f ∘ 𝔻 [ θ A ∘ η A ] ] ≡⟨⟩
       𝔻 [ H .func→ f ∘ (θ ∘nt η) A ]     ∎
       where
-        open IsCategory (𝔻 .isCategory)
+        open IsCategory (isCategory 𝔻)
 
     NatComp = _:⊕:_
 
@@ -96,29 +96,33 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
         × (_:⊕:_ {A} {B} {B} (identityNat B) f) ≡ f
       :ident: = ident-r , ident-l
 
-  instance
-    :isCategory: : IsCategory (Functor ℂ 𝔻) NaturalTransformation
-      (λ {F} → identityNat F) (λ {a} {b} {c} → _:⊕:_ {a} {b} {c})
-    :isCategory: = record
-      { assoc = λ {A B C D} → :assoc: {A} {B} {C} {D}
-      ; ident = λ {A B} → :ident: {A} {B}
-      }
-
   -- Functor categories. Objects are functors, arrows are natural transformations.
-  Fun : Category (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') (ℓc ⊔ ℓc' ⊔ ℓd')
-  Fun = record
+  RawFun : RawCategory (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') (ℓc ⊔ ℓc' ⊔ ℓd')
+  RawFun = record
     { Object = Functor ℂ 𝔻
     ; Arrow = NaturalTransformation
     ; 𝟙 = λ {F} → identityNat F
     ; _∘_ = λ {F G H} → _:⊕:_ {F} {G} {H}
     }
 
+  instance
+    :isCategory: : IsCategory RawFun
+    :isCategory: = record
+      { assoc = λ {A B C D} → :assoc: {A} {B} {C} {D}
+      ; ident = λ {A B} → :ident: {A} {B}
+      ; arrow-is-set = ?
+      ; univalent = ?
+      }
+
+  Fun : Category (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') (ℓc ⊔ ℓc' ⊔ ℓd')
+  Fun = RawFun , :isCategory:
+
 module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
   open import Cat.Categories.Sets
 
   -- Restrict the functors to Presheafs.
-  Presh : Category (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
-  Presh = record
+  RawPresh : RawCategory (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
+  RawPresh = record
     { Object = Presheaf ℂ
     ; Arrow = NaturalTransformation
     ; 𝟙 = λ {F} → identityNat F
diff --git a/src/Cat/Categories/Rel.agda b/src/Cat/Categories/Rel.agda
index 7d7eeb8..d58b35c 100644
--- a/src/Cat/Categories/Rel.agda
+++ b/src/Cat/Categories/Rel.agda
@@ -154,16 +154,18 @@ module _ {A B C D : Set} {S : Subset (A × B)} {R : Subset (B × C)} {Q : Subset
          ≡ (Σ[ b ∈ B ] (a , b) ∈ S × (Σ[ c ∈ C ] (b , c) ∈ R × (c , d) ∈ Q))
   is-assoc = equivToPath equi
 
-Rel : Category (lsuc lzero) (lsuc lzero)
-Rel = record
+RawRel : RawCategory (lsuc lzero) (lsuc lzero)
+RawRel = record
   { Object = Set
   ; Arrow = λ S R → Subset (S × R)
   ; 𝟙 = λ {S} → Diag S
   ; _∘_ = λ {A B C} S R → λ {( a , c ) → Σ[ b ∈ B ] ( (a , b) ∈ R × (b , c) ∈ S )}
-  ; isCategory = record
-    { assoc = funExt is-assoc
-    ; ident = funExt ident-l , funExt ident-r
-    ; arrow-is-set = {!!}
-    ; univalent = {!!}
-    }
+  }
+
+RawIsCategoryRel : IsCategory RawRel
+RawIsCategoryRel = record
+  { assoc = funExt is-assoc
+  ; ident = funExt ident-l , funExt ident-r
+  ; arrow-is-set = {!!}
+  ; univalent = {!!}
   }
diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index bf5744b..e9c93bd 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -4,22 +4,31 @@ module Cat.Categories.Sets where
 open import Cubical
 open import Agda.Primitive
 open import Data.Product
+import Function
 
 open import Cat.Category
 open import Cat.Functor
 open Category
 
 module _ {ℓ : Level} where
-  Sets : Category (lsuc ℓ) ℓ
-  Sets = record
-    { Object = Set ℓ
-    ; Arrow = λ T U → T → U
-    ; 𝟙 = id
-    ; _∘_ = _∘′_
-    ; isCategory = record { assoc = refl ; ident = funExt (λ _ → refl) , funExt (λ _ → refl) }
+  SetsRaw : RawCategory (lsuc ℓ) ℓ
+  SetsRaw = record
+       { Object = Set ℓ
+       ; Arrow = λ T U → T → U
+       ; 𝟙 = Function.id
+       ; _∘_ = Function._∘′_
+       }
+
+  SetsIsCategory : IsCategory SetsRaw
+  SetsIsCategory = record
+    { assoc = refl
+    ; ident = funExt (λ _ → refl) , funExt (λ _ → refl)
+    ; arrow-is-set = {!!}
+    ; univalent = {!!}
     }
-    where
-      open import Function
+
+  Sets : Category (lsuc ℓ) ℓ
+  Sets = SetsRaw , SetsIsCategory
 
   private
     module _ {X A B : Set ℓ} (f : X → A) (g : X → B) where
@@ -55,7 +64,7 @@ representable {ℂ = ℂ} A = record
     }
   }
   where
-    open IsCategory (ℂ .isCategory)
+    open IsCategory (isCategory ℂ)
 
 -- Contravariant Presheaf
 Presheaf : ∀ {ℓ ℓ'} (ℂ : Category ℓ ℓ') → Set (ℓ ⊔ lsuc ℓ')
@@ -72,4 +81,4 @@ presheaf {ℂ = ℂ} B = record
     }
   }
   where
-    open IsCategory (ℂ .isCategory)
+    open IsCategory (isCategory ℂ)
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index c4c0cdd..4154dce 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -23,18 +23,37 @@ open import Cubical.GradLemma using ( propIsEquiv )
 
 syntax ∃!-syntax (λ x → B) = ∃![ x ] B
 
+record RawCategory (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where
+  -- adding no-eta-equality can speed up type-checking.
+  -- ONLY IF you define your categories with copatterns though.
+  no-eta-equality
+  field
+    -- Need something like:
+    -- Object : Σ (Set ℓ) isGroupoid
+    Object : Set ℓ
+    -- And:
+    -- Arrow  : Object → Object → Σ (Set ℓ') isSet
+    Arrow  : Object → Object → Set ℓ'
+    𝟙      : {o : Object} → Arrow o o
+    _∘_    : {A B C : Object} → Arrow B C → Arrow A B → Arrow A C
+  infixl 10 _∘_
+  domain : { a b : Object } → Arrow a b → Object
+  domain {a = a} _ = a
+  codomain : { a b : Object } → Arrow a b → Object
+  codomain {b = b} _ = b
+
 -- Thierry: All projections must be `isProp`'s
 
 -- According to definitions 9.1.1 and 9.1.6 in the HoTT book the
 -- arrows of a category form a set (arrow-is-set), and there is an
 -- equivalence between the equality of objects and isomorphisms
 -- (univalent).
-record IsCategory {ℓ ℓ' : Level}
-  (Object : Set ℓ)
-  (Arrow  : Object → Object → Set ℓ')
-  (𝟙      : {o : Object} → Arrow o o)
-  (_∘_    : { a b c : Object } → Arrow b c → Arrow a b → Arrow a c)
-  : Set (lsuc (ℓ' ⊔ ℓ)) where
+record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where
+  open RawCategory ℂ
+  -- (Object : Set ℓ)
+  -- (Arrow  : Object → Object → Set ℓ')
+  -- (𝟙      : {o : Object} → Arrow o o)
+  -- (_∘_    : { a b c : Object } → Arrow b c → Arrow a b → Arrow a c)
   field
     assoc : {A B C D : Object} { f : Arrow A B } { g : Arrow B C } { h : Arrow C D }
       → h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f
@@ -42,10 +61,10 @@ record IsCategory {ℓ ℓ' : Level}
       → f ∘ 𝟙 ≡ f × 𝟙 ∘ f ≡ f
     arrow-is-set : ∀ {A B : Object} → isSet (Arrow A B)
 
-  Isomorphism : ∀ {A B} → (f : Arrow A B) → Set ℓ'
+  Isomorphism : ∀ {A B} → (f : Arrow A B) → Set ℓb
   Isomorphism {A} {B} f = Σ[ g ∈ Arrow B A ] g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙
 
-  _≅_ : (A B : Object) → Set ℓ'
+  _≅_ : (A B : Object) → Set ℓb
   _≅_ A B = Σ[ f ∈ Arrow A B ] (Isomorphism f)
 
   idIso : (A : Object) → A ≅ A
@@ -61,20 +80,16 @@ record IsCategory {ℓ ℓ' : Level}
     univalent : {A B : Object} → isEquiv (A ≡ B) (A ≅ B) (id-to-iso A B)
 
   module _ {A B : Object} where
-    Epimorphism : {X : Object } → (f : Arrow A B) → Set ℓ'
+    Epimorphism : {X : Object } → (f : Arrow A B) → Set ℓb
     Epimorphism {X} f = ( g₀ g₁ : Arrow B X ) → g₀ ∘ f ≡ g₁ ∘ f → g₀ ≡ g₁
 
-    Monomorphism : {X : Object} → (f : Arrow A B) → Set ℓ'
+    Monomorphism : {X : Object} → (f : Arrow A B) → Set ℓb
     Monomorphism {X} f = ( g₀ g₁ : Arrow X A ) → f ∘ g₀ ≡ f ∘ g₁ → g₀ ≡ g₁
 
-module _ {ℓ} {ℓ'} {Object : Set ℓ}
-   {Arrow  : Object → Object → Set ℓ'}
-   {𝟙      : {o : Object} → Arrow o o}
-   {_⊕_ : { a b c : Object } → Arrow b c → Arrow a b → Arrow a c}
-    where
+module _ {ℓa} {ℓb} {ℂ : RawCategory ℓa ℓb} where
   -- TODO, provable by using  arrow-is-set and that isProp (isEquiv _ _ _)
   -- This lemma will be useful to prove the equality of two categories.
-  IsCategory-is-prop : isProp (IsCategory Object Arrow 𝟙 _⊕_)
+  IsCategory-is-prop : isProp (IsCategory ℂ)
   IsCategory-is-prop x y i = record
     { assoc = x.arrow-is-set _ _ x.assoc y.assoc i
     ; ident =
@@ -94,38 +109,32 @@ module _ {ℓ} {ℓ'} {Object : Set ℓ}
       module x = IsCategory x
       module y = IsCategory y
 
-record Category (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where
-  -- adding no-eta-equality can speed up type-checking.
-  -- ONLY IF you define your categories with copatterns though.
-  no-eta-equality
-  field
-    -- Need something like:
-    -- Object : Σ (Set ℓ) isGroupoid
-    Object : Set ℓ
-    -- And:
-    -- Arrow  : Object → Object → Σ (Set ℓ') isSet
-    Arrow  : Object → Object → Set ℓ'
-    𝟙      : {o : Object} → Arrow o o
-    _∘_    : {A B C : Object} → Arrow B C → Arrow A B → Arrow A C
-    {{isCategory}} : IsCategory Object Arrow 𝟙 _∘_
-  infixl 10 _∘_
-  domain : { a b : Object } → Arrow a b → Object
-  domain {a = a} _ = a
-  codomain : { a b : Object } → Arrow a b → Object
-  codomain {b = b} _ = b
+Category : (ℓa ℓb : Level) → Set (lsuc (ℓa ⊔ ℓb))
+Category ℓa ℓb = Σ (RawCategory ℓa ℓb) IsCategory
 
-open Category
+module Category {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
+  raw = fst ℂ
+  open RawCategory raw public
+  isCategory = snd ℂ
 
-_[_,_] : ∀ {ℓ ℓ'} → (ℂ : Category ℓ ℓ') → (A : ℂ .Object) → (B : ℂ .Object) → Set ℓ'
-_[_,_] = Arrow
+open RawCategory
 
-_[_∘_] : ∀ {ℓ ℓ'} → (ℂ : Category ℓ ℓ') → {A B C : ℂ .Object} → (g : ℂ [ B , C ]) → (f : ℂ [ A , B ]) → ℂ [ A , C ]
-_[_∘_] = _∘_
+-- _∈_ : ∀ {ℓa ℓb} (ℂ : Category ℓa ℓb) → (ℂ .fst .Object → Set ℓb) → Set (ℓa ⊔ ℓb)
+-- A ∈ ℂ =
 
-module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {A B obj : Object ℂ} where
-  IsProduct : (π₁ : Arrow ℂ obj A) (π₂ : Arrow ℂ obj B) → Set (ℓ ⊔ ℓ')
+Obj : ∀ {ℓa ℓb} → Category ℓa ℓb → Set ℓa
+Obj ℂ = ℂ .fst .Object
+
+_[_,_] : ∀ {ℓ ℓ'} → (ℂ : Category ℓ ℓ') → (A : Obj ℂ) → (B : Obj ℂ) → Set ℓ'
+ℂ [ A , B ] = ℂ .fst .Arrow A B
+
+_[_∘_] : ∀ {ℓ ℓ'} → (ℂ : Category ℓ ℓ') → {A B C : Obj ℂ} → (g : ℂ [ B , C ]) → (f : ℂ [ A , B ]) → ℂ [ A , C ]
+ℂ [ g ∘ f ] = ℂ .fst ._∘_ g f
+
+module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {A B obj : Obj ℂ} where
+  IsProduct : (π₁ : ℂ [ obj , A ]) (π₂ : ℂ [ obj , B ]) → Set (ℓ ⊔ ℓ')
   IsProduct π₁ π₂
-    = ∀ {X : ℂ .Object} (x₁ : ℂ .Arrow X A) (x₂ : ℂ .Arrow X B)
+    = ∀ {X : Obj ℂ} (x₁ : ℂ [ X , A ]) (x₂ : ℂ [ X , B ])
     → ∃![ x ] (ℂ [ π₁ ∘ x ] ≡ x₁ × ℂ [ π₂ ∘ x ] ≡ x₂)
 
 -- Tip from Andrea; Consider this style for efficiency:
@@ -135,48 +144,55 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {A B obj : Object ℂ} whe
 --      isProduct : ∀ {X : ℂ .Object} (x₁ : ℂ .Arrow X A) (x₂ : ℂ .Arrow X B)
 --        → ∃![ x ] (ℂ ._⊕_ π₁ x ≡ x₁ × ℂ. _⊕_ π₂ x ≡ x₂)
 
-record Product {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} (A B : ℂ .Object) : Set (ℓ ⊔ ℓ') where
+record Product {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} (A B : Obj ℂ) : Set (ℓ ⊔ ℓ') where
   no-eta-equality
   field
-    obj : ℂ .Object
-    proj₁ : ℂ .Arrow obj A
-    proj₂ : ℂ .Arrow obj B
+    obj : Obj ℂ
+    proj₁ : ℂ [ obj , A ]
+    proj₂ : ℂ [ obj , B ]
     {{isProduct}} : IsProduct ℂ proj₁ proj₂
 
-  arrowProduct : ∀ {X} → (π₁ : Arrow ℂ X A) (π₂ : Arrow ℂ X B)
-    → Arrow ℂ X obj
+  arrowProduct : ∀ {X} → (π₁ : ℂ [ X , A ]) (π₂ : ℂ [ X , B ])
+    → ℂ [ X , obj ]
   arrowProduct π₁ π₂ = fst (isProduct π₁ π₂)
 
 record HasProducts {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') : Set (ℓ ⊔ ℓ') where
   field
-    product : ∀ (A B : ℂ .Object) → Product {ℂ = ℂ} A B
+    product : ∀ (A B : Obj ℂ) → Product {ℂ = ℂ} A B
 
   open Product
 
-  objectProduct : (A B : ℂ .Object) → ℂ .Object
+  objectProduct : (A B : Obj ℂ) → Obj ℂ
   objectProduct A B = Product.obj (product A B)
   -- The product mentioned in awodey in Def 6.1 is not the regular product of arrows.
   -- It's a "parallel" product
-  parallelProduct : {A A' B B' : ℂ .Object} → ℂ .Arrow A A' → ℂ .Arrow B B'
-    → ℂ .Arrow (objectProduct A B) (objectProduct A' B')
+  parallelProduct : {A A' B B' : Obj ℂ} → ℂ [ A , A' ] → ℂ [ B , B' ]
+    → ℂ [ objectProduct A B , objectProduct A' B' ]
   parallelProduct {A = A} {A' = A'} {B = B} {B' = B'} a b = arrowProduct (product A' B')
     (ℂ [ a ∘ (product A B) .proj₁ ])
     (ℂ [ b ∘ (product A B) .proj₂ ])
 
-module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
-  Opposite : Category ℓ ℓ'
-  Opposite =
-    record
-      { Object = ℂ .Object
-      ; Arrow = Function.flip (ℂ .Arrow)
-      ; 𝟙 = ℂ .𝟙
-      ; _∘_ = Function.flip (ℂ ._∘_)
-      ; isCategory = record { assoc = sym assoc ; ident = swap ident
-                            ; arrow-is-set = {!!}
-                            ; univalent = {!!} }
+module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
+  private
+    open Category ℂ
+    module ℂ = RawCategory (ℂ .fst)
+    OpRaw : RawCategory ℓa ℓb
+    OpRaw = record
+      { Object = ℂ.Object
+      ; Arrow = Function.flip ℂ.Arrow
+      ; 𝟙 = ℂ.𝟙
+      ; _∘_ = Function.flip (ℂ._∘_)
       }
-      where
-        open IsCategory (ℂ .isCategory)
+    open IsCategory isCategory
+    OpIsCategory : IsCategory OpRaw
+    OpIsCategory = record
+      { assoc = sym assoc
+      ; ident = swap ident
+      ; arrow-is-set = {!!}
+      ; univalent = {!!}
+      }
+  Opposite : Category ℓa ℓb
+  Opposite = OpRaw , OpIsCategory
 
 -- A consequence of no-eta-equality; `Opposite-is-involution` is no longer
 -- definitional - i.e.; you must match on the fields:
@@ -189,42 +205,34 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
 -- assoc (Opposite-is-involution i) = {!!}
 -- ident (Opposite-is-involution i) = {!!}
 
-Hom : {ℓ ℓ' : Level} → (ℂ : Category ℓ ℓ') → (A B : Object ℂ) → Set ℓ'
-Hom ℂ A B = Arrow ℂ A B
-
-module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} where
-  HomFromArrow : (A : ℂ .Object) → {B B' : ℂ .Object} → (g : ℂ .Arrow B B')
-    → Hom ℂ A B → Hom ℂ A B'
-  HomFromArrow _A = ℂ ._∘_
-
 module _ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {{hasProducts : HasProducts ℂ}} where
   open HasProducts hasProducts
   open Product hiding (obj)
   private
-    _×p_ : (A B : ℂ .Object) → ℂ .Object
+    _×p_ : (A B : Obj ℂ) → Obj ℂ
     _×p_ A B = Product.obj (product A B)
 
-  module _ (B C : ℂ .Category.Object) where
-    IsExponential : (Cᴮ : ℂ .Object) → ℂ .Arrow (Cᴮ ×p B) C → Set (ℓ ⊔ ℓ')
-    IsExponential Cᴮ eval = ∀ (A : ℂ .Object) (f : ℂ .Arrow (A ×p B) C)
-      → ∃![ f~ ] (ℂ [ eval ∘ parallelProduct f~ (ℂ .𝟙)] ≡ f)
+  module _ (B C : Obj ℂ) where
+    IsExponential : (Cᴮ : Obj ℂ) → ℂ [ Cᴮ ×p B , C ] → Set (ℓ ⊔ ℓ')
+    IsExponential Cᴮ eval = ∀ (A : Obj ℂ) (f : ℂ [ A ×p B , C ])
+      → ∃![ f~ ] (ℂ [ eval ∘ parallelProduct f~ (Category.raw ℂ .𝟙)] ≡ f)
 
     record Exponential : Set (ℓ ⊔ ℓ') where
       field
         -- obj ≡ Cᴮ
-        obj : ℂ .Object
-        eval : ℂ .Arrow ( obj ×p B ) C
+        obj : Obj ℂ
+        eval : ℂ [ obj ×p B , C ]
         {{isExponential}} : IsExponential obj eval
       -- If I make this an instance-argument then the instance resolution
       -- algorithm goes into an infinite loop. Why?
       exponentialsHaveProducts : HasProducts ℂ
       exponentialsHaveProducts = hasProducts
-      transpose : (A : ℂ .Object) → ℂ .Arrow (A ×p B) C → ℂ .Arrow A obj
+      transpose : (A : Obj ℂ) → ℂ [ A ×p B , C ] → ℂ [ A , obj ]
       transpose A f = fst (isExponential A f)
 
 record HasExponentials {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {{_ : HasProducts ℂ}} : Set (ℓ ⊔ ℓ') where
   field
-    exponent : (A B : ℂ .Object) → Exponential ℂ A B
+    exponent : (A B : Obj ℂ) → Exponential ℂ A B
 
 record CartesianClosed {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') : Set (ℓ ⊔ ℓ') where
   field
@@ -234,15 +242,15 @@ record CartesianClosed {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') : Set (ℓ 
 module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
   unique = isContr
 
-  IsInitial : ℂ .Object → Set (ℓa ⊔ ℓb)
-  IsInitial I = {X : ℂ .Object} → unique (ℂ .Arrow I X)
+  IsInitial : Obj ℂ → Set (ℓa ⊔ ℓb)
+  IsInitial I = {X : Obj ℂ} → unique (ℂ [ I , X ])
 
-  IsTerminal : ℂ .Object → Set (ℓa ⊔ ℓb)
+  IsTerminal : Obj ℂ → Set (ℓa ⊔ ℓb)
   -- ∃![ ? ] ?
-  IsTerminal T = {X : ℂ .Object} → unique (ℂ .Arrow X T)
+  IsTerminal T = {X : Obj ℂ} → unique (ℂ [ X , T ])
 
   Initial : Set (ℓa ⊔ ℓb)
-  Initial = Σ (ℂ .Object) IsInitial
+  Initial = Σ (Obj ℂ) IsInitial
 
   Terminal : Set (ℓa ⊔ ℓb)
-  Terminal = Σ (ℂ .Object) IsTerminal
+  Terminal = Σ (Obj ℂ) IsTerminal
diff --git a/src/Cat/Category/Free.agda b/src/Cat/Category/Free.agda
index 4d5db54..1225aa3 100644
--- a/src/Cat/Category/Free.agda
+++ b/src/Cat/Category/Free.agda
@@ -10,33 +10,33 @@ open import Cat.Category as C
 module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
   private
     open module ℂ = Category ℂ
-    Obj = ℂ.Object
 
   postulate
-    Path : ( a b : Obj ) → Set ℓ'
-    emptyPath : (o : Obj) → Path o o
-    concatenate : {a b c : Obj} → Path b c → Path a b → Path a c
+    Path : ( a b : Obj ℂ ) → Set ℓ'
+    emptyPath : (o : Obj ℂ) → Path o o
+    concatenate : {a b c : Obj ℂ} → Path b c → Path a b → Path a c
 
   private
-    module _ {A B C D : Obj} {r : Path A B} {q : Path B C} {p : Path C D} where
+    module _ {A B C D : Obj ℂ} {r : Path A B} {q : Path B C} {p : Path C D} where
       postulate
         p-assoc : concatenate {A} {C} {D} p (concatenate {A} {B} {C} q r)
           ≡ concatenate {A} {B} {D} (concatenate {B} {C} {D} p q) r
-    module _ {A B : Obj} {p : Path A B} where
+    module _ {A B : Obj ℂ} {p : Path A B} where
       postulate
         ident-r : concatenate {A} {A} {B} p (emptyPath A) ≡ p
         ident-l : concatenate {A} {B} {B} (emptyPath B) p ≡ p
 
-  Free : Category ℓ ℓ'
-  Free = record
-    { Object = Obj
+  RawFree : RawCategory ℓ ℓ'
+  RawFree = record
+    { Object = Obj ℂ
     ; Arrow = Path
     ; 𝟙 = λ {o} → emptyPath o
     ; _∘_ = λ {a b c} → concatenate {a} {b} {c}
-    ; isCategory = record
-      { assoc = p-assoc
-      ; ident = ident-r , ident-l
-      ; arrow-is-set = {!!}
-      ; univalent = {!!}
-      }
+    }
+  RawIsCategoryFree : IsCategory RawFree
+  RawIsCategoryFree = record
+    { assoc = p-assoc
+    ; ident = ident-r , ident-l
+    ; arrow-is-set = {!!}
+    ; univalent = {!!}
     }
diff --git a/src/Cat/Functor.agda b/src/Cat/Functor.agda
index 873ea43..e88238d 100644
--- a/src/Cat/Functor.agda
+++ b/src/Cat/Functor.agda
@@ -10,11 +10,11 @@ open Category hiding (_∘_)
 
 module _ {ℓc ℓc' ℓd ℓd'} (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where
   record IsFunctor
-    (func* : ℂ .Object → 𝔻 .Object)
-    (func→ : {A B : ℂ .Object} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ])
+    (func* : Obj ℂ → Obj 𝔻)
+    (func→ : {A B : Obj ℂ} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ])
       : Set (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') where
     field
-      ident   : { c : ℂ .Object } → func→ (ℂ .𝟙 {c}) ≡ 𝔻 .𝟙 {func* c}
+      ident   : {c : Obj ℂ} → func→ (ℂ .𝟙 {c}) ≡ 𝔻 .𝟙 {func* c}
       -- TODO: Avoid use of ugly explicit arguments somehow.
       -- This guy managed to do it:
       --    https://github.com/copumpkin/categories/blob/master/Categories/Functor/Core.agda