category.lean

category.lean

namespace category
  universes u v

  structure category :=
    (object : Type u)
    (arrow : object → object → Type v)
    (identity : Π {α}, arrow α α)
    (compose : Π {α β φ}, arrow β φ → arrow α β → arrow α φ)
    (infixr ∘ := compose)
    (compose_left_identity_unit : ∀ α β (f : arrow α β), identity ∘ f = f)
    (compose_right_identity_unit : ∀ α β (f : arrow α β), f ∘ identity = f)
    (compose_associative : ∀ α β φ δ (f : arrow φ δ) g (h : arrow α β), f ∘ (g ∘ h) = (f ∘ g) ∘ h)

  infixr ∘ := category.compose _

  def sort_coercible_type_category (s) [has_coe_to_sort s] : category :=
    { object := s
    , arrow := λ α β, α → β
    , identity := λ _, id
    , compose := λ _ _ _, function.comp
    , compose_left_identity_unit := begin intros; reflexivity end
    , compose_right_identity_unit := begin intros; reflexivity end
    , compose_associative := begin intros; reflexivity end
    }

  def Types := @sort_coercible_type_category (Sort _) ⟨id⟩

  def finite_type := { α //  ∃ {n} (f : α → fin n), function.bijective f }

  instance finite_type_to_sort : has_coe_to_sort finite_type :=
    ⟨subtype.val⟩

  def FiniteTypes := @sort_coercible_type_category finite_type ⟨subtype.val⟩

  #print group

  structure group' :=
    (carrier : Type u)
    (is_group : group carrier)

  instance group'_to_sort : has_coe_to_sort group' :=
    ⟨group'.carrier⟩

  instance group'_group (g : group') : group g := g.is_group

  structure group_morphism (g₁ : group') (g₂ : group') :=
    (map : g₁ → g₂)
    (preserves_one : map 1 = 1)
    (preserves_mul : ∀ x y, map (x * y) = map x * map y)

  def Group : category :=
    { object := group'
    , arrow := group_morphism
    , identity := λ _, { map := id
                       , preserves_one := rfl
                       , preserves_mul := begin intros; reflexivity end
                       }
    , compose := λ _ _ _ f g, { map := f.map ∘ g.map
                              , preserves_one := begin intros; simp [function.comp, f.preserves_one, g.preserves_one] end
                              , preserves_mul := begin intros; simp [function.comp, f.preserves_mul, g.preserves_mul] end
                              }
    , compose_left_identity_unit := begin intros; induction f; reflexivity end
    , compose_right_identity_unit := begin intros; induction f; reflexivity end
    , compose_associative := begin intros; induction f; reflexivity end
    }

  universes u2 v2

  structure functor (A : category.{u v}) (B : category.{u2 v2}) :=
    (object_map : A.object → B.object)
    (arrow_map : Π {α β}, A.arrow α β → B.arrow (object_map α) (object_map β))
    (preserves_identity : ∀ α, arrow_map (@category.identity A α) = category.identity B)
    (preserves_composition : ∀ α β φ (f : A.arrow α β) (g : A.arrow β φ), arrow_map (g ∘ f) = (arrow_map g) ∘ (arrow_map f))

  def Cat : category :=
    { object := category.{u v}
    , arrow := functor
    , identity := λ _, { object_map := id
                       , arrow_map := λ _ _, id
                       , preserves_identity := begin intros; reflexivity end
                       , preserves_composition := begin intros; reflexivity end
                       }
    , compose := λ _ _ _ g f, { object_map := λ x, g.object_map (f.object_map x)
                              , arrow_map := λ _ _ x, g.arrow_map (f.arrow_map x)
                              , preserves_identity := begin intros; simp [f.preserves_identity, g.preserves_identity] end
                              , preserves_composition := begin intros; simp [f.preserves_composition, g.preserves_composition] end
                              }
    , compose_left_identity_unit :=
      begin intros; induction f; reflexivity end
    , compose_right_identity_unit :=
      begin intros; induction f; reflexivity end
    , compose_associative :=
      begin intros; induction f; reflexivity end
    }
end category