Kim Morrison kim-em

kim-em / Functors_pointwise_equal.lean

Created January 28, 2017 15:54 — forked from leodemoura/Functors_pointwise_equal.lean

	meta def blast : tactic unit := using_smt $ return ()

	structure Category :=
	(Obj : Type)
	(Hom : Obj → Obj → Type)

	structure Functor (C : Category) (D : Category) :=
	(onObjects : C^.Obj → D^.Obj)
	(onMorphisms : Π { X Y : C^.Obj },
	C^.Hom X Y → D^.Hom (onObjects X) (onObjects Y))

kim-em / casting.lean

Created January 27, 2017 12:10 — forked from leodemoura/casting.lean

	meta def blast : tactic unit := using_smt $ return ()

	structure Category :=
	(Obj : Type)
	(Hom : Obj → Obj → Type)

	structure Functor (C : Category) (D : Category) :=
	(onObjects : C^.Obj → D^.Obj)
	(onMorphisms : Π { X Y : C^.Obj },
	C^.Hom X Y → D^.Hom (onObjects X) (onObjects Y))