Loading theory "Category3.Category" (required by "Category3.Limit" via "Category3.FreeCategory")
locale partial_magma
  fixes C :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "\<cdot>" 55)
  assumes "partial_magma (\<cdot>)"
locale category
  fixes C :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "\<cdot>" 55)
  assumes "category (\<cdot>)"
locale classical_category
  fixes Obj :: "'obj \<Rightarrow> bool"
    and Arr :: "'arr \<Rightarrow> bool"
    and Dom :: "'arr \<Rightarrow> 'obj"
    and Cod :: "'arr \<Rightarrow> 'obj"
    and Id :: "'obj \<Rightarrow> 'arr"
    and Comp :: "'arr \<Rightarrow> 'arr \<Rightarrow> 'arr"
  assumes "classical_category Obj Arr Dom Cod Id Comp"
locale category
  fixes C :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "\<cdot>" 55)
  assumes "category (\<cdot>)"
### theory "Category3.Category"
### 0.837s elapsed time, 1.596s cpu time, 0.000s GC time
Loading theory "Category3.AbstractedCategory" (required by "Category3.Limit" via "Category3.FreeCategory")
locale abstracted_category
  fixes
    C :: "'c \<Rightarrow> 'c \<Rightarrow> 'c"
      (infixr "\<cdot>\<^sub>C" 55)
    and A :: "'c \<Rightarrow> 'a"
    and R :: "'a \<Rightarrow> 'c"
    and S :: "'c set"
  assumes "abstracted_category (\<cdot>\<^sub>C) A R S"
locale abstracted_category
  fixes
    C :: "'c \<Rightarrow> 'c \<Rightarrow> 'c"
      (infixr "\<cdot>\<^sub>C" 55)
    and A :: "'c \<Rightarrow> 'a"
    and R :: "'a \<Rightarrow> 'c"
    and S :: "'c set"
  assumes "abstracted_category (\<cdot>\<^sub>C) A R S"
### theory "Category3.AbstractedCategory"
### 0.294s elapsed time, 0.584s cpu time, 0.000s GC time
Loading theory "Category3.DiscreteCategory" (required by "Category3.Limit")
locale discrete_category
  fixes Obj :: "'a set"
  assumes "discrete_category Obj"
locale discrete_category
  fixes Obj :: "'a set"
  assumes "discrete_category Obj"
### theory "Category3.DiscreteCategory"
### 0.146s elapsed time, 0.292s cpu time, 0.000s GC time
Loading theory "Category3.DualCategory" (required by "Category3.Limit" via "Category3.Adjunction" via "Category3.Yoneda")
locale dual_category
  fixes C :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "\<cdot>" 55)
  assumes "dual_category (\<cdot>)"
locale dual_category
  fixes C :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "\<cdot>" 55)
  assumes "dual_category (\<cdot>)"
### theory "Category3.DualCategory"
### 0.387s elapsed time, 0.712s cpu time, 0.252s GC time
Loading theory "Category3.EpiMonoIso" (required by "Category3.Limit" via "Category3.Adjunction" via "Category3.Yoneda" via "Category3.SetCat" via "Category3.SetCategory" via "Category3.Functor" via "Category3.InitialTerminal")
locale category
  fixes C :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "\<cdot>" 55)
  assumes "category (\<cdot>)"
### theory "Category3.EpiMonoIso"
### 0.060s elapsed time, 0.116s cpu time, 0.000s GC time
Loading theory "Category3.FreeCategory" (required by "Category3.Limit")
locale graph
  fixes Obj :: "'obj set"
    and Arr :: "'arr set"
    and Dom :: "'arr \<Rightarrow> 'obj"
    and Cod :: "'arr \<Rightarrow> 'obj"
  assumes "graph Obj Arr Dom Cod"
locale free_category
  fixes Obj :: "'obj set"
    and Arr :: "'arr set"
    and D :: "'arr \<Rightarrow> 'obj"
    and C :: "'arr \<Rightarrow> 'obj"
  assumes "free_category Obj Arr D C"
locale free_category
  fixes Obj :: "'obj set"
    and Arr :: "'arr set"
    and D :: "'arr \<Rightarrow> 'obj"
    and C :: "'arr \<Rightarrow> 'obj"
  assumes "free_category Obj Arr D C"
locale discrete_category
  fixes Obj :: "'obj set"
  assumes "discrete_category Obj"
locale empty_category
  assumes "empty_category"
locale quiver
  fixes Arr :: "'arr set"
  assumes "quiver Arr"
locale parallel_pair
  assumes "parallel_pair"
### theory "Category3.FreeCategory"
### 1.862s elapsed time, 3.720s cpu time, 0.000s GC time
isabelle document -d /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Category3/document -o pdf -n document
isabelle document -d /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Category3/outline -o pdf -n outline -t /proof,/ML
*** Failed to load theory "Category3.InitialTerminal" (unresolved "Category3.EpiMonoIso")
*** Failed to load theory "Category3.Functor" (unresolved "Category3.InitialTerminal")
*** Failed to load theory "Category3.NaturalTransformation" (unresolved "Category3.Functor")
*** Failed to load theory "Category3.Subcategory" (unresolved "Category3.Functor")
*** Failed to load theory "Category3.ProductCategory" (unresolved "Category3.EpiMonoIso")
*** Failed to load theory "Category3.BinaryFunctor" (unresolved "Category3.NaturalTransformation", "Category3.ProductCategory")
*** Failed to load theory "Category3.FunctorCategory" (unresolved "Category3.BinaryFunctor")
*** Failed to load theory "Category3.SetCategory" (unresolved "Category3.Functor")
*** Failed to load theory "Category3.SetCat" (unresolved "Category3.SetCategory")
*** Failed to load theory "Category3.Yoneda" (unresolved "Category3.FunctorCategory", "Category3.SetCat")
*** Failed to load theory "Category3.Adjunction" (unresolved "Category3.Yoneda")
*** Failed to load theory "Category3.EquivalenceOfCategories" (unresolved "Category3.Adjunction")
*** Failed to load theory "Category3.Limit" (unresolved "Category3.Adjunction")
*** Type unification failed
*** 
*** Type error in application: incompatible operand type
*** 
*** Operator:  inj_on ::
***   (??'a \<Rightarrow> ??'b) \<Rightarrow> ??'a set \<Rightarrow> bool
*** Operand:   op \<cdot> f :: 'a
*** 
*** At command "definition" (line 23 of "~~/afp/thys/Category3/EpiMonoIso.thy")