cat.lean

import data.set.basic
import data.equiv.basic
import tactic.rcases
import tactic.interactive
import tactic.tidy

/-!
    This is land of oz.
    Living Scarecrow in munchkin at 2020-03-15 12:51:14
    -/
    namespace land.oz.munchkin
    ------------------------------------

#check nat

namespace category_def

    structure {u v} category :=
    ( obj : Type u)
    ( hom : Π A B : obj, Type v )
    ( id : Π {A}, hom A A )
    ( comp : Π {A B C} (g : hom B C) (f : hom A B), hom A C )
    ( comp_assoc : ∀ {A B C D} (h : hom C D) (g : hom B C) (f : hom A B),
                comp h (comp g f) = comp (comp h g) f )
    ( id_comp : ∀ {A B} (f : hom A B), comp id f = f )
    ( comp_id : ∀ {A B} (f : hom A B), comp f id = f )
    
    class {u v} category' (obj : Type u) :=
    ( hom : Π A B : obj, Type v )
    ( id : Π {A}, hom A A )
    ( comp : Π {A B C} (g : hom B C) (f : hom A B), hom A C )
    ( comp_assoc : ∀ {A B C D} (h : hom C D) (g : hom B C) (f : hom A B),
                comp h (comp g f) = comp (comp h g) f )
    ( id_comp : ∀ {A B} (f : hom A B), comp id f = f )
    ( comp_id : ∀ {A B} (f : hom A B), comp f id = f )

    class {u v} category'' (obj : Type u) (hom : Π A B : obj, Type v) :=
    ( id : Π {A}, hom A A )
    ( comp : Π {A B C} (g : hom B C) (f : hom A B), hom A C )
    ( comp_assoc : ∀ {A B C D} (h : hom C D) (g : hom B C) (f : hom A B),
                comp h (comp g f) = comp (comp h g) f )
    ( id_comp : ∀ {A B} (f : hom A B), comp id f = f )
    ( comp_id : ∀ {A B} (f : hom A B), comp f id = f )

    -- @[instance]
    def {} category_to_category' (C : category) : category' C.obj := { ..C }
    @[instance]
    def {u} category'_to_category'' {obj : Type u} (C : category' obj) : category'' obj C.hom := { ..C }
    def {u v} category''_to_category {obj : Type u} {hom : Π A B : obj, Type v} (C : category'' obj hom) : category := { obj := obj, hom := hom, ..C }

    lemma {u v} category_equiv_category' : category.{u v} ≃ Σ obj, category'.{u v} obj :=
        begin
            refine_struct {..},
            exact λ C, ⟨C.obj, category_to_category' C⟩,
            rintro ⟨obj, C⟩,
            apply category''_to_category,
            exact category'_to_category'' C,
            intro C, cases C, exact rfl,
            rintro ⟨obj, C'⟩, cases C', exact rfl,
        end
    lemma {u v} category'_equiv_category'' : (Σ obj, category'.{u v} obj) ≃ Σ obj hom, category''.{u v} obj hom :=
        begin
            refine_struct {..},
            rintro ⟨obj, C'⟩, exact ⟨obj, C'.hom, category'_to_category'' C'⟩,
            rintro ⟨obj, hom, C''⟩,
            use obj,
            -- refine category_to_category' _,
            exact category_to_category' (category''_to_category C''),
            -- exact category_to_category' this
            rintro ⟨obj, C'⟩, cases C', exact rfl,
            rintro ⟨obj, hom, C''⟩, cases C'', exact rfl,
        end 
    


    notation A `⟶` B       := category.hom (by assumption) A B
    notation `hom(`A`,`B`)` := category.hom (by assumption) A B
    notation A `⟶[`C`]` B      := category.hom C A B
    notation `hom-`C`(`A`,`B`)` := category.hom C A B

    notation A `⟶` B       := category'.hom A B
    notation `hom(`A`,`B`)` := category'.hom A B
    notation A `⟶[`C`]` B      := @category'.hom _ C A B
    notation `hom-`C`(`A`,`B`)` := @category'.hom _ C A B

    notation g `∘` f := category.comp (by assumption) g f
    notation g `∘` f := category'.comp g f

    -- notation `Mor(`C`)` := Σ A B : Ob(C), category.hom C A B

    def {} Ob (C : category) := C.obj
    def {u} Ob' {obj : Type u} (C : category' obj) := obj
    def {u v} Ob'' {obj : Type u} {hom : Π A B : obj, Type v} (C : category'' obj hom) := obj

    def {} Mor (C : category) := Σ A B : Ob(C), category.hom C A B
    def {u} Mor' {obj : Type u} (C : category' obj) := Σ A B : Ob'(C), @category'.hom obj C A B
    def {u v} Mor'' {obj : Type u} {hom : Π A B : obj, Type v} (C : category'' obj hom) := Σ A B : Ob''(C), hom A B
 
--  universes u v
    -- variables {obj : Type u} {A B : obj} [category'.{u v} obj]
    def {u v} dom {obj : Type u} {A B : obj} [category'.{u v} obj] (f : A ⟶ B) := A
    def {u v} cod {obj : Type u} {A B : obj} [category'.{u v} obj] (f : A ⟶ B) := B

end category_def


open category_def

lemma {u v} dom_unique {obj : Type u} {A B : obj} [category' obj] (f f' : A ⟶ B) : 
            (f = f') → dom(f) = dom(f') := congr_arg _

lemma {u v} cod_unique {obj : Type u} {A B : obj} [category' obj] (f f' : A ⟶ B)  : 
            (f = f') → cod(f) = cod(f') := congr_arg _
    
def dual (cat : category) : category :=
    begin
        refine_struct { obj := cat.obj },
        intros a b, exact (b ⟶ a),
        exact cat.id,
        intros a b c g f,
        exact f ∘ g,
        intros a b c d h g f,
        dsimp only,
        rw [←category.comp_assoc],
        intros a b f,
        dsimp only,
        rw [category.comp_id],
        intros a b f,
        dsimp only,
        rw [category.id_comp],
    end

theorem dual_dual (cat : category) : dual (dual cat) = cat :=
    begin
        cases cat,
        dunfold dual,
        dsimp only,
        simp,
    end

notation g `∘ᵒᵖ` f := category.comp (dual (by assumption)) g f
notation g `∘ᵒᵖ` f := @category'.comp _ (dual (by assumption)) _ _ _ g f



















------------------------------------
    end land.oz.munchkin