Special shapes for limits in Type
. #
The general shape (co)limits defined in CategoryTheory.Limits.Types
are intended for use through the limits API,
and the actual implementation should mostly be considered "sealed".
In this file, we provide definitions of the "standard" special shapes of limits in Type
,
giving the expected definitional implementation:
- the terminal object is
PUnit
- the binary product of
X
andY
isX × Y
- the product of a family
f : J → Type
isΠ j, f j
- the coproduct of a family
f : J → Type
isΣ j, f j
- the binary coproduct of
X
andY
is the sum typeX ⊕ Y
- the equalizer of a pair of maps
(g, h)
is the subtype{x : Y // g x = h x}
- the coequalizer of a pair of maps
(f, g)
is the quotient ofY
by∀ x : Y, f x ~ g x
- the pullback of
f : X ⟶ Z
andg : Y ⟶ Z
is the subtype{ p : X × Y // f p.1 = g p.2 }
of the product - multiequalizers
We first construct terms of IsLimit
and LimitCone
, and then provide isomorphisms with the
types generated by the HasLimit
API.
As an example, when setting up the monoidal category structure on Type
we use the Types.terminalLimitCone
and Types.binaryProductLimitCone
definitions.
A restatement of Types.Limit.lift_π_apply
that uses Pi.π
and Pi.lift
.
A restatement of Types.Limit.lift_π_apply
that uses Pi.π
and Pi.lift
,
with specialized universes.
A restatement of Types.Limit.map_π_apply
that uses Pi.π
and Pi.map
.
A restatement of Types.Limit.map_π_apply
that uses Pi.π
and Pi.map
,
with specialized universes.
The category of types has PUnit
as a terminal object.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The terminal object in Type u
is PUnit
.
Equations
- CategoryTheory.Limits.Types.isTerminalPunit = CategoryTheory.Limits.terminalIsTerminal.ofIso CategoryTheory.Limits.Types.terminalIso
Instances For
Equations
- CategoryTheory.Limits.Types.instInhabitedTerminalType = { default := CategoryTheory.Limits.terminal.from (ULift.{?u.9, 0} (Fin 1)) { down := 0 } }
Equations
A type is terminal if and only if it contains exactly one element.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A type is terminal if and only if it is isomorphic to PUnit
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The category of types has PEmpty
as an initial object.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The initial object in Type u
is PEmpty
.
Equations
- CategoryTheory.Limits.Types.isInitialPunit = CategoryTheory.Limits.initialIsInitial.ofIso CategoryTheory.Limits.Types.initialIso
Instances For
An object in Type u
is initial if and only if it is empty.
The product type X × Y
forms a cone for the binary product of X
and Y
.
Equations
- CategoryTheory.Limits.Types.binaryProductCone X Y = CategoryTheory.Limits.BinaryFan.mk Prod.fst Prod.snd
Instances For
The product type X × Y
is a binary product for X
and Y
.
Equations
- CategoryTheory.Limits.Types.binaryProductLimit X Y = { lift := fun (s : CategoryTheory.Limits.BinaryFan X Y) (x : s.pt) => (s.fst x, s.snd x), fac := ⋯, uniq := ⋯ }
Instances For
The category of types has X × Y
, the usual cartesian product,
as the binary product of X
and Y
.
Equations
- CategoryTheory.Limits.Types.binaryProductLimitCone X Y = { cone := CategoryTheory.Limits.Types.binaryProductCone X Y, isLimit := CategoryTheory.Limits.Types.binaryProductLimit X Y }
Instances For
The categorical binary product in Type u
is cartesian product.
Equations
Instances For
The functor which sends X, Y
to the product type X × Y
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The product functor given by the instance HasBinaryProducts (Type u)
is isomorphic to the
explicit binary product functor given by the product type.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The sum type X ⊕ Y
forms a cocone for the binary coproduct of X
and Y
.
Equations
- CategoryTheory.Limits.Types.binaryCoproductCocone X Y = CategoryTheory.Limits.BinaryCofan.mk Sum.inl Sum.inr
Instances For
The sum type X ⊕ Y
is a binary coproduct for X
and Y
.
Equations
- CategoryTheory.Limits.Types.binaryCoproductColimit X Y = { desc := fun (s : CategoryTheory.Limits.BinaryCofan X Y) => Sum.elim s.inl s.inr, fac := ⋯, uniq := ⋯ }
Instances For
The category of types has X ⊕ Y
,
as the binary coproduct of X
and Y
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The categorical binary coproduct in Type u
is the sum X ⊕ Y
.
Equations
Instances For
Any monomorphism in Type
is a coproduct injection.
Equations
Instances For
The category of types has Π j, f j
as the product of a type family f : J → TypeMax.{v, u}
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The categorical product in TypeMax.{v, u}
is the type theoretic product Π j, F j
.
Equations
Instances For
A variant of productLimitCone
using a Small
hypothesis rather than a function to TypeMax
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The categorical product in Type u
indexed in Type v
is the type theoretic product Π j, F j
, after shrinking back to Type u
.
Equations
Instances For
The category of types has Σ j, f j
as the coproduct of a type family f : J → Type
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The categorical coproduct in Type u
is the type theoretic coproduct Σ j, F j
.
Equations
Instances For
Show the given fork in Type u
is an equalizer given that any element in the "difference kernel"
comes from X
.
The converse of unique_of_type_equalizer
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The converse of type_equalizer_of_unique
.
Show that the subtype {x : Y // g x = h x}
is an equalizer for the pair (g,h)
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The categorical equalizer in Type u
is {x : Y // g x = h x}
.
Equations
- CategoryTheory.Limits.Types.equalizerIso g h = CategoryTheory.Limits.limit.isoLimitCone CategoryTheory.Limits.Types.equalizerLimit
Instances For
(Implementation) The relation to be quotiented to obtain the coequalizer.
- Rel: ∀ {X Y : Type u} {f g : X ⟶ Y} (x : X), CategoryTheory.Limits.Types.CoequalizerRel f g (f x) (g x)
Instances For
Show that the quotient by the relation generated by f(x) ~ g(x)
is a coequalizer for the pair (f, g)
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If π : Y ⟶ Z
is an equalizer for (f, g)
, and U ⊆ Y
such that f ⁻¹' U = g ⁻¹' U
,
then π ⁻¹' (π '' U) = U
.
The categorical coequalizer in Type u
is the quotient by f g ~ g x
.
Equations
Instances For
The usual explicit pullback in the category of types, as a subtype of the product.
The full LimitCone
data is bundled as pullbackLimitCone f g
.
Equations
- CategoryTheory.Limits.Types.PullbackObj f g = { p : X × Y // f p.1 = g p.2 }
Instances For
The explicit pullback cone on PullbackObj f g
.
This is bundled with the IsLimit
data as pullbackLimitCone f g
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A limit pullback cone in the category of types identifies to the explicit pullback.
Equations
- CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj hc = (hc.conePointUniqueUpToIso (CategoryTheory.Limits.Types.pullbackLimitCone f g).isLimit).toEquiv
Instances For
Given c : PullbackCone f g
in the category of types, this is
the canonical map c.pt → Types.PullbackObj f g
.
Equations
- c.toPullbackObj x = ⟨(c.fst x, c.snd x), ⋯⟩
Instances For
A pullback cone c
in the category of types is limit iff the
map c.toPullbackObj : c.pt → Types.PullbackObj f g
is a bijection.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The pullback given by the instance HasPullbacks (Type u)
is isomorphic to the
explicit pullback object given by PullbackObj
.
Equations
Instances For
The pushout of two maps f : S ⟶ X₁
and g : S ⟶ X₂
is the quotient
by the equivalence relation on X₁ ⊕ X₂
generated by this relation.
- inl_inr: ∀ {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} (s : S), CategoryTheory.Limits.Types.Pushout.Rel f g (Sum.inl (f s)) (Sum.inr (g s))
Instances For
In case f : S ⟶ X₁
is a monomorphism, this relation is the equivalence relation
generated by Pushout.Rel f g
.
- refl: ∀ {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} (x : X₁ ⊕ X₂), CategoryTheory.Limits.Types.Pushout.Rel' f g x x
- inl_inl: ∀ {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} (x₀ y₀ : S), g x₀ = g y₀ → CategoryTheory.Limits.Types.Pushout.Rel' f g (Sum.inl (f x₀)) (Sum.inl (f y₀))
- inl_inr: ∀ {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} (s : S), CategoryTheory.Limits.Types.Pushout.Rel' f g (Sum.inl (f s)) (Sum.inr (g s))
- inr_inl: ∀ {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} (s : S), CategoryTheory.Limits.Types.Pushout.Rel' f g (Sum.inr (g s)) (Sum.inl (f s))
Instances For
Given I : MulticospanIndex (Type u)
, this is a type which identifies
to the sections of the functor I.multicospan
.
- val : (i : I.L) → I.left i
The data of an element in
I.left i
for eachi : I.L
. - property : ∀ (r : I.R), I.fst r (self.val (I.fstTo r)) = I.snd r (self.val (I.sndTo r))
Instances For
The bijection I.sections ≃ I.multicospan.sections
when I : MulticospanIndex (Type u)
is a multiequalizer diagram in the category of types.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given a multiequalizer diagram I : MulticospanIndex (Type u)
in the category of
types and c
a multifork for I
, this is the canonical map c.pt → I.sections
.
Equations
- c.toSections x = { val := fun (i : I.L) => c.ι i x, property := ⋯ }
Instances For
A multifork c : Multifork I
in the category of types is limit iff the
map c.toSections : c.pt → I.sections
is a bijection.
The bijection I.sections ≃ c.pt
when c : Multifork I
is a limit multifork
in the category of types.
Equations
- CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv hc = (Equiv.ofBijective c.toSections ⋯).symm