[WIP] Groupoid interpretation #168

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft

Vtec234 wants to merge 36 commits into master from hott0-interp

HoTTLean/ForMathlib.lean

            
                      Original file line number
                      Diff line number
                      Diff line change
                  
    @@ -1,10 +1,11 @@
  
    import Mathlib.Tactic.DepRewrite

    import Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

    import Mathlib.CategoryTheory.Groupoid.Discrete

    import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq

    import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

    import Mathlib.CategoryTheory.Category.ULift

    import Mathlib.Logic.Function.ULift

    import Mathlib.CategoryTheory.Category.Cat

    import Mathlib.CategoryTheory.Category.Grpd

    import Mathlib.CategoryTheory.Groupoid.Grpd.Basic

    import Mathlib.Data.Part

    import Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

    import Mathlib.CategoryTheory.Core

    @@ -101,29 +102,29 @@ namespace CategoryTheory.Cat
  
    /-- This is the proof of equality used in the eqToHom in `Cat.eqToHom_hom` -/

    theorem eqToHom_hom_aux {C1 C2 : Cat.{v,u}} (x y: C1) (eq : C1 = C2) :

        (x ⟶ y) = ((eqToHom eq).obj x ⟶ (eqToHom eq).obj y) := by

        (x ⟶ y) = ((eqToHom eq).toFunctor.obj x ⟶ (eqToHom eq).toFunctor.obj y) := by

      cases eq

      simp[CategoryStruct.id]

    /-- This is the turns the hom part of eqToHom functors into a cast-/

    theorem eqToHom_hom {C1 C2 : Cat.{v,u}} {x y: C1} (f : x ⟶ y) (eq : C1 = C2) :

        (eqToHom eq).map f = (cast (Cat.eqToHom_hom_aux x y eq) f) := by

        (eqToHom eq).toFunctor.map f = (cast (Cat.eqToHom_hom_aux x y eq) f) := by

      cases eq

      simp[CategoryStruct.id]

    /-- This turns the object part of eqToHom functors into casts -/

    theorem eqToHom_obj {C1 C2 : Cat.{v,u}} (x : C1) (eq : C1 = C2) :

        (eqToHom eq).obj x = cast (congrArg Bundled.α eq) x := by

        (eqToHom eq).toFunctor.obj x = cast (congrArg Bundled.α eq) x := by

      cases eq

      simp[CategoryStruct.id]

    abbrev homOf {C D : Type u} [Category.{v} C] [Category.{v} D] (F : C ⥤ D) :

        Cat.of C ⟶ Cat.of D := F

        Cat.of C ⟶ Cat.of D := ⟨F⟩

    @[simps] def ULift_lte_iso_self {C : Type (max u u₁)} [Category.{v} C] :

        Cat.of (ULift.{u} C) ≅ Cat.of C where

      hom := ULift.downFunctor

      inv := ULift.upFunctor

      hom := homOf ULift.downFunctor

      inv := homOf ULift.upFunctor

    @[simp] def ULift_succ_iso_self {C : Type (u + 1)} [Category.{v} C] :

        of (ULift.{u, u + 1} C) ≅ of C := ULift_lte_iso_self.{v,u,u+1}

    @@ -135,8 +136,8 @@ def ofULift (C : Type u) [Category.{v} C] : Cat.{v, max u w} :=
  
      of $ ULift.{w} C

    def uLiftFunctor : Cat.{v,u} ⥤ Cat.{v, max u w} where

      obj X := Cat.ofULift.{w} X

      map F := Cat.homOf $ ULift.downFunctor ⋙ F ⋙ ULift.upFunctor

      obj X := ofULift.{w} X

      map F := homOf $ ULift.downFunctor ⋙ F.toFunctor ⋙ ULift.upFunctor

    end CategoryTheory.Cat

    @@ -401,16 +402,15 @@ variable {Γ : Type u₂} [Category.{v₂} Γ] {A : Γ ⥤ Grpd.{v₁,u₁}}
  
    @[simp] theorem Cat.map_id_obj {A : Γ ⥤ Cat.{v₁,u₁}}

        {x : Γ} {a : A.obj x} :

        (A.map (𝟙 x)).obj a = a := by

      have : A.map (𝟙 x) = 𝟙 (A.obj x) := by simp

      exact Functor.congr_obj this a

        (A.map (𝟙 x)).toFunctor.obj a = a := by

      simp

    theorem Cat.map_id_map {A : Γ ⥤ Cat.{v₁,u₁}}

        {x : Γ} {a b : A.obj x} {f : a ⟶ b} :

        (A.map (𝟙 x)).map f = eqToHom Cat.map_id_obj

        (A.map (𝟙 x)).toFunctor.map f = eqToHom Cat.map_id_obj

          ≫ f ≫ eqToHom Cat.map_id_obj.symm := by

      have : A.map (𝟙 x) = 𝟙 (A.obj x) := by simp

      exact Functor.congr_hom this f

      rw! [show A.map (𝟙 x) = 𝟙 (A.obj x) by simp]

      simp

    end

    @@ -624,14 +624,6 @@ lemma Discrete.functor_eq {X C : Type*} [Category C] {F : Discrete X ⥤ C} :
  
        cases h

        simp

    lemma Discrete.functor_ext {X C : Type*} [Category C] (F G : Discrete X ⥤ C)

        (h : ∀ x : X, F.obj ⟨x⟩ = G.obj ⟨x⟩) :

        F = G :=

      calc F

        _ = Discrete.functor (fun x => F.obj ⟨x⟩) := Discrete.functor_eq

        _ = Discrete.functor (fun x => G.obj ⟨x⟩) := Discrete.functor_ext' h

        _ = G := Discrete.functor_eq.symm

    lemma Discrete.hext {X Y : Type u} (a : Discrete X) (b : Discrete Y) (hXY : X ≍ Y)

        (hab : a.1 ≍ b.1) : a ≍ b := by

      aesop_cat

HoTTLean/ForMathlib/CategoryTheory/Bicategory/Grothendieck.lean

-Original file line number
+Diff line change
@@ Expand Up / @@ -60,8 +60,6 @@ variable (F : Pseudofunctor B Cat) {a b : B} @@
         (X Y : LocallyDiscrete C) (e : X ≅ Y) : e.hom.toLoc ≫ e.inv.toLoc = 𝟙 _ :=
       LocallyDiscrete.eq_of_hom ⟨⟨by simp⟩⟩
-    attribute [reassoc] StrongTrans.naturality_comp_inv_app
     end
     lemma _root_.CategoryTheory.Functor.toPseudofunctor'_map₂ {C : Type u₁} [Category.{v₁} C] (F : C ⥤ Cat)
@@ Expand Down @@

HoTTLean/ForMathlib/CategoryTheory/FreeGroupoid.lean

            
                      Original file line number
                      Diff line number
                      Diff line change
                  
    @@ -4,14 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
  
    Authors: Joseph Hua

    -/

    import Mathlib.CategoryTheory.Groupoid.FreeGroupoid

    import Mathlib.CategoryTheory.Category.Grpd

    import Mathlib.CategoryTheory.Groupoid.Grpd.Basic

    import Mathlib.CategoryTheory.Adjunction.Reflective

    import Mathlib.CategoryTheory.Localization.Predicate

    import Mathlib.CategoryTheory.Monad.Limits

    import Mathlib.CategoryTheory.Category.Cat.Limit

    import HoTTLean.ForMathlib.CategoryTheory.Localization.Predicate

    /-!

    # Free groupoid on a category

    @@ -190,15 +188,15 @@ open Category.FreeGroupoid
  
    @[simps]

    def free : Cat.{u,u} ⥤ Grpd.{u,u} where

      obj C := Grpd.of <| Category.FreeGroupoid C

      map {C D} F := map F

      map_id C := by simp [Grpd.id_eq_id, ← map_id]; rfl

      map_comp F G := by simp [Grpd.comp_eq_comp, ← map_comp]; rfl

      map {C D} F := map F.toFunctor

      map_id C := by simp [Grpd.id_eq_id, ← map_id]

      map_comp F G := by simp [Grpd.comp_eq_comp, ← map_comp]

    /-- The unit of the free-forgetful adjunction between `Grpd` and `Cat`. -/

    @[simps]

    def freeForgetAdjunction.unit : 𝟭 Cat ⟶ free ⋙ forgetToCat where

      app C := Category.FreeGroupoid.of C

      naturality C D F := by simp [forgetToCat, Cat.comp_eq_comp, map, lift_spec]

      app C := ⟨Category.FreeGroupoid.of C⟩

      naturality C D F := by ext; simp [forgetToCat, map, lift_spec]

    /-- The counit of the free-forgetful adjunction between `Grpd` and `Cat`. -/

    @[simps]

    @@ -218,7 +216,7 @@ def freeForgetAdjunction : free ⊣ Grpd.forgetToCat where
  
        apply lift_unique

        simp [Functor.assoc, lift_spec, Grpd.id_eq_id]

      right_triangle_components G := by

        simp [forgetToCat, Cat.comp_eq_comp, lift_spec, Cat.id_eq_id]

        ext; simp [forgetToCat, lift_spec]

    instance : Reflective Grpd.forgetToCat where

      L := free

HoTTLean/ForMathlib/CategoryTheory/Groupoid.lean

This file was deleted.

HoTTLean/ForMathlib/CategoryTheory/Localization/Predicate.lean

This file was deleted.

HoTTLean/ForMathlib/CategoryTheory/MorphismProperty/Basic.lean

This file was deleted.

HoTTLean/ForMathlib/CategoryTheory/NatTrans.lean

-Original file line number
+Diff line change
@@ -1,6 +1,5 @@
     import Mathlib.CategoryTheory.NatTrans
     import Mathlib.CategoryTheory.Functor.TwoSquare
-    import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq
     import HoTTLean.ForMathlib
     universe w v u v₁ u₁ v₂ u₂ v₃ u₃
@@ Expand Down @@

HoTTLean/ForMathlib/CategoryTheory/RepPullbackCone.lean

-Original file line number
+Diff line change
@@ -1,7 +1,7 @@
     import Mathlib.CategoryTheory.Limits.Yoneda
     import Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
     import Mathlib.CategoryTheory.Limits.Preserves.Finite
-    import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq
+    import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
     import HoTTLean.ForMathlib.CategoryTheory.WeakPullback
     /-!
@@ Expand Down @@

HoTTLean/ForMathlib/Tactic/CategoryTheory/FunctorMap.lean

            
                      Original file line number
                      Diff line number
                      Diff line change
                  
    @@ -56,24 +56,24 @@ def functorMapExpr (e : Expr) (lvl_params : Bool) : MetaM (Expr × List Level) :
  
        let some (hom, _, _) := eTp.eq? | throwError "expected an equality, got{indentD eTp}"

        if !hom.isAppOf ``Quiver.Hom then

          throwError "expected an equality of morphisms, got{indentD eTp}"

        let [.succ v₁, u₁] := hom.getAppFn.constLevels! |

        let [v₁, u₁] := hom.getAppFn.constLevels! |

          throwError "unexpected universe levels in{indentD hom.getAppFn}"

        let e' ← mkAppM' (.const ``eq_functor_map [v₁, u₁, v₂, u₂]) #[e]

        simpType categorySimp' e'

      return (e, [v₂, u₂])

    syntax (name := functor_map) "functor_map" (" (" &"attr" ":=" Parser.Term.attrInstance,* ")")? : attr

    syntax (name := functor_map) "functor_map" optAttrArg : attr

    initialize registerBuiltinAttribute {

      name := `functor_map

      descr := ""

      applicationTime := .afterCompilation

      add := fun src ref kind => match ref with

      | `(attr| functor_map $[(attr := $stx?,*)]?) => MetaM.run' do

      | `(attr| functor_map $stx?) => MetaM.run' do

        if (kind != AttributeKind.global) then

          throwError "`functor_map` can only be used as a global attribute"

        addRelatedDecl src "_functor_map" ref stx? fun type value levels => do

          let (e, levels') ← functorMapExpr (← mkExpectedTypeHint value type) true

        addRelatedDecl src (src.appendAfter "_functor_map") ref stx? fun value levels => do

          let (e, levels') ← functorMapExpr value true

          pure (e, levels ++ levels'.map fun | .param n => n | _ => panic! "")

      | _ => throwUnsupportedSyntax }

HoTTLean/ForPoly.lean

            
                      Original file line number
                      Diff line number
                      Diff line change
                  
    @@ -256,8 +256,8 @@ theorem fan_snd_map' {E B E' B' : C} {P : UvPoly E B} {P' : UvPoly E' B'}
  
      slice_lhs 1 2 => rw [← this]

      slice_lhs 2 3 => apply Category.comp_id

      simp [α, Over.starPullbackIsoStar]

      slice_lhs 5 6 => apply pullback.lift_fst

      simp [Over.mapForget]

      slice_lhs 4 5 => apply pullback.lift_fst

      simp

    open ExponentiableMorphism in

    theorem fan_snd_map {E B A E' B' A' : C} {P : UvPoly E B} {P' : UvPoly E' B'}

HoTTLean/Frontend/Checked.lean

This file was deleted.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[WIP] Groupoid interpretation #168

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

[WIP] Groupoid interpretation #168

Are you sure you want to change the base?

Uh oh!

[WIP] Groupoid interpretation #168

Uh oh!

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!