Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+πŸ–±οΈto focus. On Mac, use Cmdinstead of Ctrl. 
/-
Copyright (c) 2018 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison, Johannes HΓΆlzl, Reid Barton, Sean Leather

! This file was ported from Lean 3 source module category_theory.concrete_category.bundled
! leanprover-community/mathlib commit a148d797a1094ab554ad4183a4ad6f130358ef64
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Std.Tactic.Lint.Frontend
import Std.Tactic.Lint.Misc
import Std.Tactic.CoeExt
import Mathlib.Mathport.Rename

/-!
# Bundled types

`Bundled c` provides a uniform structure for bundling a type equipped with a type class.

We provide `Category` instances for these in `CategoryTheory/UnbundledHom.lean`
(for categories with unbundled homs, e.g. topological spaces)
and in `CategoryTheory/BundledHom.lean` (for categories with bundled homs, e.g. monoids).
-/

universe u v

namespace CategoryTheory

variable {
c: Type u β†’ Type v
c 
d: Type u β†’ Type v
d : 
Type u: Type (u+1)
Type u β†’ 
Type v: Type (v+1)
Type v} {
Ξ±: Type u
Ξ± : 
Type u: Type (u+1)
Type u}

/-- `Bundled` is a type bundled with a type class instance for that type. Only
the type class is exposed as a parameter. -/
structure 
Bundled: (Type u β†’ Type v) β†’ Type (max(u+1)v)
Bundled (
c: Type u β†’ Type v
c : 
Type u: Type (u+1)
Type u β†’ 
Type v: Type (v+1)
Type v) : 
Type max (u + 1) v: Type ((max(u+1)v)+1)
Type max (u + 1) v where
  /-- The underlying type of the bundled type -/
  
Ξ±: {c : Type u β†’ Type v} β†’ Bundled c β†’ Type u
Ξ± : 
Type u: Type (u+1)
Type u
  /-- The corresponding instance of the bundled type class -/
  
str: {c : Type u β†’ Type v} β†’ (self : Bundled c) β†’ c self.Ξ±
str : 
c: Type u β†’ Type v
c 
Ξ±: Type u
Ξ± := by infer_instance
#align category_theory.bundled 
CategoryTheory.Bundled: (Type u β†’ Type v) β†’ Type (max(u+1)v)
CategoryTheory.Bundled

namespace Bundled

attribute [coe] 
Ξ±: {c : Type u β†’ Type v} β†’ Bundled c β†’ Type u
Ξ±

-- This is needed so that we can ask for an instance of `c Ξ±` below even though Lean doesn't know
-- that `c Ξ±` is a typeclass.
set_option checkBinderAnnotations false in

-- Usually explicit instances will provide their own version of this, e.g. `MonCat.of` and
-- `TopCat.of`.
/-- A generic function for lifting a type equipped with an instance to a bundled object. -/
def 
of: {c : Type u β†’ Type v} β†’ (Ξ± : Type u) β†’ [str : c Ξ±] β†’ Bundled c
of {
c: Type u β†’ Type v
c : 
Type u: Type (u+1)
Type u β†’ 
Type v: Type (v+1)
Type v} (
Ξ±: Type u
Ξ± : 
Type u: Type (u+1)
Type u) [
str: c Ξ±
str : 
c: Type u β†’ Type v
c 
Ξ±: Type u
Ξ±] : 
Bundled: (Type ?u.698 β†’ Type ?u.697) β†’ Type (max(?u.698+1)?u.697)
Bundled 
c: Type u β†’ Type v
c :=
  ⟨
Ξ±: Type u
Ξ±, 
str: c Ξ±
str⟩
#align category_theory.bundled.of 
CategoryTheory.Bundled.of: {c : Type u β†’ Type v} β†’ (Ξ± : Type u) β†’ [str : c Ξ±] β†’ Bundled c
CategoryTheory.Bundled.of

instance 
coeSort: CoeSort (Bundled c) (Type u)
coeSort : 
CoeSort: Sort ?u.764 β†’ outParam (Sort ?u.763) β†’ Sort (max(max1?u.764)?u.763)
CoeSort (
Bundled: (Type ?u.766 β†’ Type ?u.765) β†’ Type (max(?u.766+1)?u.765)
Bundled 
c: Type u β†’ Type v
c) (
Type u: Type (u+1)
Type u) :=
  ⟨
Bundled.Ξ±: {c : Type ?u.781 β†’ Type ?u.780} β†’ Bundled c β†’ Type ?u.781
Bundled.α⟩

theorem 
coe_mk: βˆ€ (Ξ± : Type u) (str : c Ξ±), ↑(mk Ξ±) = Ξ±
coe_mk (
Ξ±: ?m.855
Ξ±) (
str: c Ξ±
str) : (@
Bundled.mk: {c : Type ?u.864 β†’ Type ?u.863} β†’ (Ξ± : Type ?u.864) β†’ autoParam (c Ξ±) _auto✝ β†’ Bundled c
Bundled.mk 
c: Type u β†’ Type v
c 
Ξ±: ?m.855
Ξ± 
str: ?m.858
str : 
Type u: Type (u+1)
Type u) = 
Ξ±: ?m.855
Ξ± :=
  
rfl: βˆ€ {Ξ± : Sort ?u.1000} {a : Ξ±}, a = a
rfl
#align category_theory.bundled.coe_mk 
CategoryTheory.Bundled.coe_mk: βˆ€ {c : Type u β†’ Type v} (Ξ± : Type u) (str : c Ξ±), ↑(mk Ξ±) = Ξ±
CategoryTheory.Bundled.coe_mk

/-
`Bundled.map` is reducible so that, if we define a category

  def Ring : Type (u+1) := induced_category SemiRing (bundled.map @ring.to_semiring)

instance search is able to "see" that a morphism R ⟢ S in Ring is really
a (semi)ring homomorphism from R.Ξ± to S.Ξ±, and not merely from
`(Bundled.map @Ring.toSemiring R).Ξ±` to `(Bundled.map @Ring.toSemiring S).Ξ±`.

TODO: Once at least one use of this has been ported, check if this still needs to be reducible in
Lean 4.
-/
/-- Map over the bundled structure -/
def 
map: ({Ξ± : Type u} β†’ c Ξ± β†’ d Ξ±) β†’ Bundled c β†’ Bundled d
map (
f: {Ξ± : Type u} β†’ c Ξ± β†’ d Ξ±
f : βˆ€ {
Ξ±: ?m.1022
Ξ±}, 
c: Type u β†’ Type v
c 
Ξ±: ?m.1022
Ξ± β†’ 
d: Type u β†’ Type v
d 
Ξ±: ?m.1022
Ξ±) (
b: Bundled c
b : 
Bundled: (Type ?u.1030 β†’ Type ?u.1029) β†’ Type (max(?u.1030+1)?u.1029)
Bundled 
c: Type u β†’ Type v
c) : 
Bundled: (Type ?u.1037 β†’ Type ?u.1036) β†’ Type (max(?u.1037+1)?u.1036)
Bundled 
d: Type u β†’ Type v
d :=
  ⟨
b: Bundled c
b, 
f: {Ξ± : Type u} β†’ c Ξ± β†’ d Ξ±
f 
b: Bundled c
b.
str: {c : Type ?u.1184 β†’ Type ?u.1183} β†’ (self : Bundled c) β†’ c ↑self
str⟩
#align category_theory.bundled.map 
CategoryTheory.Bundled.map: {c d : Type u β†’ Type v} β†’ ({Ξ± : Type u} β†’ c Ξ± β†’ d Ξ±) β†’ Bundled c β†’ Bundled d
CategoryTheory.Bundled.map

end Bundled

end CategoryTheory