--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/subcat.agda	Sat May 02 04:21:05 2020 +0900
@@ -0,0 +1,23 @@
+open import Category
+open import Level
+module subcat {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁' c₂' ℓ') (B : Category c₁ c₂ ℓ) (F : Functor A B) where
+
+    open import cat-utility
+    open import Relation.Binary.PropositionalEquality
+    open Functor
+
+    FCat : Category c₁' c₂ ℓ
+    FCat = record {
+          Obj = Obj A
+          ; Hom = λ a b → Hom B (FObj F a) (FObj F b)
+          ; _o_ = Category._o_ B
+          ; _≈_ = Category._≈_ B
+          ; Id  = λ {a} → id1 B (FObj F a)
+          ; isCategory = record {
+                    isEquivalence =  IsCategory.isEquivalence (Category.isCategory B) ;
+                    identityL  = λ {a b f} → IsCategory.identityL (Category.isCategory B) ;
+                    identityR  = λ {a b f} → IsCategory.identityR (Category.isCategory B) ;
+                    o-resp-≈  = λ {a b c f g h i} → IsCategory.o-resp-≈ (Category.isCategory B);
+                    associative  = λ{a b c d f g h } → IsCategory.associative (Category.isCategory B) 
+             }
+      }