IMPAN demo: structures

structures.lean

import category_theory.category.basic

open category_theory

/-! # Structures

Define your own structure
(e.g. `prod` or `functor`)
and define examples (e.g. composition).

-/


namespace impan
/-! ## Products -/

structure prod (X Y : Type) :=
(fst : X)
(snd : Y)

-- type as `\boxtimes`
notation X `⊠` Y := impan.prod X Y

variables {X Y : Type}

example (x : X) (y : Y) : X ⊠ Y :=
_

example (p : X ⊠ Y) : X :=
_

@[ext]
lemma prod.ext (p q : X ⊠ Y)
  (h1 : p.fst = q.fst) (h2 : p.snd = q.snd) :
  p = q :=
begin
  sorry
end

end impan


namespace impan
/-! ## Functors -/

structure functor (C D : Type)
  [category C] [category D] :=
(obj : C → D)
-- (map : _)
-- (map_id : _)
-- (map_comp : _)


variables {C D E : Type}
variables [category C] [category D] [category E]

def functor.comp
  (F : functor C D) (G : functor D E) :
  functor C E :=
_


end impan