Geb.Mathlib.CategoryTheory.DiscreteFibration.Basic

Imports

/-
Copyright (c) 2026 Terence Rokop. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Terence Rokop
-/
module

public import Mathlib.CategoryTheory.Comma.Arrow
public import Mathlib.CategoryTheory.FiberedCategory.Fiber
public import Mathlib.CategoryTheory.FiberedCategory.Fibered
public import Mathlib.CategoryTheory.FiberedCategory.HomLift
public import Mathlib.Tactic.Attr.Core

Discrete fibrations: lifting data

A functor p : C ⥤ B is a discrete fibration when every g : b ⟶ p.obj c has a unique lift with codomain c ([LoregianRiehl2018] § 2.1; [nLabDiscreteFibration]). This module carries that lifting data as a structure and relates it to mathlib's fibred-category API.

Main definitions

DiscreteFibration p, the lifting data: for each g : b ⟶ p.obj c a lift hom g : src g ⟶ c, together with the statement that it is the only lift.

Main statements

DiscreteFibration.map_injective and DiscreteFibration.faithful: a discrete fibration is faithful.

isHomLift_iff_arrow_mk_eq: mathlib's Functor.IsHomLift is equality of arrows.

DiscreteFibration.isCartesian, DiscreteFibration.isPreFibered and DiscreteFibration.isFibered: every morphism is cartesian, so a discrete fibration is a fibred category.

DiscreteFibration.fiber_eq_of_hom and DiscreteFibration.fiber_hom_ext: the fibres are discrete categories.

Implementation notes

Lifts are unique, so DiscreteFibration p is a Subsingleton: carrying it as data costs nothing, and it lets the fibre presheaf of Geb/Mathlib/CategoryTheory/DiscreteFibration/FiberPresheaf.lean be defined without Classical.choice.

eq_of_isHomLift_id and fiber_eq_of_hom route through Functor.Fiber.fiberInclusion rather than the subtype projections of Functor.Fiber, which is semireducible: a goal mentioning b.1 is not type-correct at implicit transparency and stops rw and simp.

References

[LoregianRiehl2018]

[nLabDiscreteFibration]

Tags

discrete fibration, fibred category, cartesian morphism, fibre

              @[expose] public sectionuniverse v₁ v₂ u₁ u₂namespace CategoryTheoryvariable {C : Type u₁} [Category.{v₁} C] {B : Type u₂} [Category.{v₂} B]

Lifting data for p: for every g : b ⟶ p.obj c a lift hom g : src g ⟶ c over g, unique among all lifts. The base-side eqToHom is forced by the bundle presentation (objects of C are only propositionally over b); it vanishes in the family presentation Functor.CoElements below.

Domain of the lift of g.

The lift of g.

The domain of the lift of g lies over the domain of g.

The lift of g lies over g.

Uniqueness of lifts, as an equality in Σ c', c' ⟶ c.

              structure DiscreteFibration (p : C ⥤ B) where  src : ∀ {b : B} {c : C}, (b ⟶ p.obj c) → C  hom : ∀ {b : B} {c : C} (g : b ⟶ p.obj c), src g ⟶ c  obj_src : ∀ {b : B} {c : C} (g : b ⟶ p.obj c), p.obj (src g) = b  map_hom : ∀ {b : B} {c : C} (g : b ⟶ p.obj c),
    p.map (hom g) = eqToHom (obj_src g) ≫ g  unique : ∀ {b : B} {c : C} (g : b ⟶ p.obj c) {c' : C} (h : c' ⟶ c)
    (e : p.obj c' = b), p.map h = eqToHom e ≫ g →
      (⟨c', h⟩ : Σ c', c' ⟶ c) = ⟨src g, hom g⟩

              namespace DiscreteFibrationvariable {p : C ⥤ B} (D : DiscreteFibration p)include D

The uniqueness clause with the source fixed: p reflects equality of parallel arrows, i.e. p is faithful.

theorem map_injective {c c' : C} {h₁ h₂ : c' ⟶ c}
    (H : p.map h₁ = p.map h₂) : h₁ = h₂ := byC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pc:Cc':Ch₁:c' ⟶ ch₂:c' ⟶ cH:p.map h₁ = p.map h₂⊢ h₁ = h₂
  have h := (D.unique (p.map h₂) h₁ rfl (byC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pc:Cc':Ch₁:c' ⟶ ch₂:c' ⟶ cH:p.map h₁ = p.map h₂⊢ p.map h₁ = eqToHom ⋯ ≫ p.map h₂ simpa using HAll goals completed! 🐙)).trans
    (D.unique (p.map h₂) h₂ rfl (byC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pc:Cc':Ch₁:c' ⟶ ch₂:c' ⟶ cH:p.map h₁ = p.map h₂⊢ p.map h₂ = eqToHom ⋯ ≫ p.map h₂ simpAll goals completed! 🐙)).symmC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pc:Cc':Ch₁:c' ⟶ ch₂:c' ⟶ cH:p.map h₁ = p.map h₂h:⟨c', h₁⟩ = ⟨c', h₂⟩⊢ h₁ = h₂
  exact eq_of_heq (Sigma.mk.inj_iff.1 h).2All goals completed! 🐙

A discrete fibration is faithful.

theorem faithful : p.Faithful := ⟨fun H => D.map_injective H⟩

Uniqueness of the source of a lift.

theorem src_eq {b : B} {c c' : C} (g : b ⟶ p.obj c) (h : c' ⟶ c)
    (e : p.obj c' = b) (H : p.map h = eqToHom e ≫ g) : D.src g = c' :=
  (congrArg Sigma.fst (D.unique g h e H)).symm

The lift of an identity is an identity.

theorem src_id (c : C) : D.src (𝟙 (p.obj c)) = c :=
  D.src_eq _ (𝟙 c) rfl (byC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pc:C⊢ p.map (𝟙 c) = eqToHom ⋯ ≫ 𝟙 (p.obj c) simpAll goals completed! 🐙)

Lifting data is unique: DiscreteFibration p is a mere proposition.

instance : Subsingleton (DiscreteFibration p) := byC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration p⊢ Subsingleton (DiscreteFibration p)
  constructorC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration p⊢ ∀ (a b : DiscreteFibration p), a = b
  intro D₁ D₂C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pD₁:DiscreteFibration pD₂:DiscreteFibration p⊢ D₁ = D₂
  have h : ∀ {b : B} {c : C} (g : b ⟶ p.obj c),
      (⟨D₁.src g, D₁.hom g⟩ : Σ c', c' ⟶ c) =
        ⟨D₂.src g, D₂.hom g⟩ :=
    fun g => D₂.unique g (D₁.hom g) (D₁.obj_src g) (D₁.map_hom g)C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pD₁:DiscreteFibration pD₂:DiscreteFibration ph:∀ {b : B} {c : C} (g : b ⟶ p.obj c), ⟨D₁.src g, D₁.hom g⟩ = ⟨D₂.src g, D₂.hom g⟩⊢ D₁ = D₂
  obtain ⟨src₁, hom₁, _, _, _⟩ := D₁C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pD₂:DiscreteFibration psrc₁:{b : B} → {c : C} → (b ⟶ p.obj c) → Chom₁:{b : B} → {c : C} → (g : b ⟶ p.obj c) → src₁ g ⟶ cobj_src✝:∀ {b : B} {c : C} (g : b ⟶ p.obj c), p.obj (src₁ g) = bmap_hom✝:∀ {b : B} {c : C} (g : b ⟶ p.obj c), p.map (hom₁ g) = eqToHom ⋯ ≫ gunique✝:∀ {b : B} {c : C} (g : b ⟶ p.obj c) {c' : C} (h : c' ⟶ c) (e : p.obj c' = b),
  p.map h = eqToHom e ≫ g → ⟨c', h⟩ = ⟨src₁ g, hom₁ g⟩h:∀ {b : B} {c : C} (g : b ⟶ p.obj c),
  ⟨{ src := src₁, hom := hom₁, obj_src := obj_src✝, map_hom := map_hom✝, unique := unique✝ }.src g,
      { src := src₁, hom := hom₁, obj_src := obj_src✝, map_hom := map_hom✝, unique := unique✝ }.hom g⟩ =
    ⟨D₂.src g, D₂.hom g⟩⊢ { src := src₁, hom := hom₁, obj_src := obj_src✝, map_hom := map_hom✝, unique := unique✝ } = D₂
  obtain ⟨src₂, hom₂, _, _, _⟩ := D₂C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration psrc₁:{b : B} → {c : C} → (b ⟶ p.obj c) → Chom₁:{b : B} → {c : C} → (g : b ⟶ p.obj c) → src₁ g ⟶ cobj_src✝¹:∀ {b : B} {c : C} (g : b ⟶ p.obj c), p.obj (src₁ g) = bmap_hom✝¹:∀ {b : B} {c : C} (g : b ⟶ p.obj c), p.map (hom₁ g) = eqToHom ⋯ ≫ gunique✝¹:∀ {b : B} {c : C} (g : b ⟶ p.obj c) {c' : C} (h : c' ⟶ c) (e : p.obj c' = b),
  p.map h = eqToHom e ≫ g → ⟨c', h⟩ = ⟨src₁ g, hom₁ g⟩src₂:{b : B} → {c : C} → (b ⟶ p.obj c) → Chom₂:{b : B} → {c : C} → (g : b ⟶ p.obj c) → src₂ g ⟶ cobj_src✝:∀ {b : B} {c : C} (g : b ⟶ p.obj c), p.obj (src₂ g) = bmap_hom✝:∀ {b : B} {c : C} (g : b ⟶ p.obj c), p.map (hom₂ g) = eqToHom ⋯ ≫ gunique✝:∀ {b : B} {c : C} (g : b ⟶ p.obj c) {c' : C} (h : c' ⟶ c) (e : p.obj c' = b),
  p.map h = eqToHom e ≫ g → ⟨c', h⟩ = ⟨src₂ g, hom₂ g⟩h:∀ {b : B} {c : C} (g : b ⟶ p.obj c),
  ⟨{ src := src₁, hom := hom₁, obj_src := obj_src✝¹, map_hom := map_hom✝¹, unique := unique✝¹ }.src g,
      { src := src₁, hom := hom₁, obj_src := obj_src✝¹, map_hom := map_hom✝¹, unique := unique✝¹ }.hom g⟩ =
    ⟨{ src := src₂, hom := hom₂, obj_src := obj_src✝, map_hom := map_hom✝, unique := unique✝ }.src g,
      { src := src₂, hom := hom₂, obj_src := obj_src✝, map_hom := map_hom✝, unique := unique✝ }.hom g⟩⊢ { src := src₁, hom := hom₁, obj_src := obj_src✝¹, map_hom := map_hom✝¹, unique := unique✝¹ } =
  { src := src₂, hom := hom₂, obj_src := obj_src✝, map_hom := map_hom✝, unique := unique✝ }
  have hs : @src₁ = @src₂ := byC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration p⊢ Subsingleton (DiscreteFibration p)
    funext b c gC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration psrc₁:{b : B} → {c : C} → (b ⟶ p.obj c) → Chom₁:{b : B} → {c : C} → (g : b ⟶ p.obj c) → src₁ g ⟶ cobj_src✝¹:∀ {b : B} {c : C} (g : b ⟶ p.obj c), p.obj (src₁ g) = bmap_hom✝¹:∀ {b : B} {c : C} (g : b ⟶ p.obj c), p.map (hom₁ g) = eqToHom ⋯ ≫ gunique✝¹:∀ {b : B} {c : C} (g : b ⟶ p.obj c) {c' : C} (h : c' ⟶ c) (e : p.obj c' = b),
  p.map h = eqToHom e ≫ g → ⟨c', h⟩ = ⟨src₁ g, hom₁ g⟩src₂:{b : B} → {c : C} → (b ⟶ p.obj c) → Chom₂:{b : B} → {c : C} → (g : b ⟶ p.obj c) → src₂ g ⟶ cobj_src✝:∀ {b : B} {c : C} (g : b ⟶ p.obj c), p.obj (src₂ g) = bmap_hom✝:∀ {b : B} {c : C} (g : b ⟶ p.obj c), p.map (hom₂ g) = eqToHom ⋯ ≫ gunique✝:∀ {b : B} {c : C} (g : b ⟶ p.obj c) {c' : C} (h : c' ⟶ c) (e : p.obj c' = b),
  p.map h = eqToHom e ≫ g → ⟨c', h⟩ = ⟨src₂ g, hom₂ g⟩h:∀ {b : B} {c : C} (g : b ⟶ p.obj c),
  ⟨{ src := src₁, hom := hom₁, obj_src := obj_src✝¹, map_hom := map_hom✝¹, unique := unique✝¹ }.src g,
      { src := src₁, hom := hom₁, obj_src := obj_src✝¹, map_hom := map_hom✝¹, unique := unique✝¹ }.hom g⟩ =
    ⟨{ src := src₂, hom := hom₂, obj_src := obj_src✝, map_hom := map_hom✝, unique := unique✝ }.src g,
      { src := src₂, hom := hom₂, obj_src := obj_src✝, map_hom := map_hom✝, unique := unique✝ }.hom g⟩b:Bc:Cg:b ⟶ p.obj c⊢ src₁ g = src₂ g
    exact congrArg Sigma.fst (h g)C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration psrc₁:{b : B} → {c : C} → (b ⟶ p.obj c) → Chom₁:{b : B} → {c : C} → (g : b ⟶ p.obj c) → src₁ g ⟶ cobj_src✝¹:∀ {b : B} {c : C} (g : b ⟶ p.obj c), p.obj (src₁ g) = bmap_hom✝¹:∀ {b : B} {c : C} (g : b ⟶ p.obj c), p.map (hom₁ g) = eqToHom ⋯ ≫ gunique✝¹:∀ {b : B} {c : C} (g : b ⟶ p.obj c) {c' : C} (h : c' ⟶ c) (e : p.obj c' = b),
  p.map h = eqToHom e ≫ g → ⟨c', h⟩ = ⟨src₁ g, hom₁ g⟩src₂:{b : B} → {c : C} → (b ⟶ p.obj c) → Chom₂:{b : B} → {c : C} → (g : b ⟶ p.obj c) → src₂ g ⟶ cobj_src✝:∀ {b : B} {c : C} (g : b ⟶ p.obj c), p.obj (src₂ g) = bmap_hom✝:∀ {b : B} {c : C} (g : b ⟶ p.obj c), p.map (hom₂ g) = eqToHom ⋯ ≫ gunique✝:∀ {b : B} {c : C} (g : b ⟶ p.obj c) {c' : C} (h : c' ⟶ c) (e : p.obj c' = b),
  p.map h = eqToHom e ≫ g → ⟨c', h⟩ = ⟨src₂ g, hom₂ g⟩h:∀ {b : B} {c : C} (g : b ⟶ p.obj c),
  ⟨{ src := src₁, hom := hom₁, obj_src := obj_src✝¹, map_hom := map_hom✝¹, unique := unique✝¹ }.src g,
      { src := src₁, hom := hom₁, obj_src := obj_src✝¹, map_hom := map_hom✝¹, unique := unique✝¹ }.hom g⟩ =
    ⟨{ src := src₂, hom := hom₂, obj_src := obj_src✝, map_hom := map_hom✝, unique := unique✝ }.src g,
      { src := src₂, hom := hom₂, obj_src := obj_src✝, map_hom := map_hom✝, unique := unique✝ }.hom g⟩hs:src₁ = src₂⊢ { src := src₁, hom := hom₁, obj_src := obj_src✝¹, map_hom := map_hom✝¹, unique := unique✝¹ } =
  { src := src₂, hom := hom₂, obj_src := obj_src✝, map_hom := map_hom✝, unique := unique✝ }
  subst hsC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration psrc₁:{b : B} → {c : C} → (b ⟶ p.obj c) → Chom₁:{b : B} → {c : C} → (g : b ⟶ p.obj c) → src₁ g ⟶ cobj_src✝¹:∀ {b : B} {c : C} (g : b ⟶ p.obj c), p.obj (src₁ g) = bmap_hom✝¹:∀ {b : B} {c : C} (g : b ⟶ p.obj c), p.map (hom₁ g) = eqToHom ⋯ ≫ gunique✝¹:∀ {b : B} {c : C} (g : b ⟶ p.obj c) {c' : C} (h : c' ⟶ c) (e : p.obj c' = b),
  p.map h = eqToHom e ≫ g → ⟨c', h⟩ = ⟨src₁ g, hom₁ g⟩hom₂:{b : B} → {c : C} → (g : b ⟶ p.obj c) → src₁ g ⟶ cobj_src✝:∀ {b : B} {c : C} (g : b ⟶ p.obj c), p.obj (src₁ g) = bmap_hom✝:∀ {b : B} {c : C} (g : b ⟶ p.obj c), p.map (hom₂ g) = eqToHom ⋯ ≫ gunique✝:∀ {b : B} {c : C} (g : b ⟶ p.obj c) {c' : C} (h : c' ⟶ c) (e : p.obj c' = b),
  p.map h = eqToHom e ≫ g → ⟨c', h⟩ = ⟨src₁ g, hom₂ g⟩h:∀ {b : B} {c : C} (g : b ⟶ p.obj c),
  ⟨{ src := src₁, hom := hom₁, obj_src := obj_src✝¹, map_hom := map_hom✝¹, unique := unique✝¹ }.src g,
      { src := src₁, hom := hom₁, obj_src := obj_src✝¹, map_hom := map_hom✝¹, unique := unique✝¹ }.hom g⟩ =
    ⟨{ src := src₁, hom := hom₂, obj_src := obj_src✝, map_hom := map_hom✝, unique := unique✝ }.src g,
      { src := src₁, hom := hom₂, obj_src := obj_src✝, map_hom := map_hom✝, unique := unique✝ }.hom g⟩⊢ { src := src₁, hom := hom₁, obj_src := obj_src✝¹, map_hom := map_hom✝¹, unique := unique✝¹ } =
  { src := src₁, hom := hom₂, obj_src := obj_src✝, map_hom := map_hom✝, unique := unique✝ }
  have hh : @hom₁ = @hom₂ := byC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration p⊢ Subsingleton (DiscreteFibration p)
    funext b c gC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration psrc₁:{b : B} → {c : C} → (b ⟶ p.obj c) → Chom₁:{b : B} → {c : C} → (g : b ⟶ p.obj c) → src₁ g ⟶ cobj_src✝¹:∀ {b : B} {c : C} (g : b ⟶ p.obj c), p.obj (src₁ g) = bmap_hom✝¹:∀ {b : B} {c : C} (g : b ⟶ p.obj c), p.map (hom₁ g) = eqToHom ⋯ ≫ gunique✝¹:∀ {b : B} {c : C} (g : b ⟶ p.obj c) {c' : C} (h : c' ⟶ c) (e : p.obj c' = b),
  p.map h = eqToHom e ≫ g → ⟨c', h⟩ = ⟨src₁ g, hom₁ g⟩hom₂:{b : B} → {c : C} → (g : b ⟶ p.obj c) → src₁ g ⟶ cobj_src✝:∀ {b : B} {c : C} (g : b ⟶ p.obj c), p.obj (src₁ g) = bmap_hom✝:∀ {b : B} {c : C} (g : b ⟶ p.obj c), p.map (hom₂ g) = eqToHom ⋯ ≫ gunique✝:∀ {b : B} {c : C} (g : b ⟶ p.obj c) {c' : C} (h : c' ⟶ c) (e : p.obj c' = b),
  p.map h = eqToHom e ≫ g → ⟨c', h⟩ = ⟨src₁ g, hom₂ g⟩h:∀ {b : B} {c : C} (g : b ⟶ p.obj c),
  ⟨{ src := src₁, hom := hom₁, obj_src := obj_src✝¹, map_hom := map_hom✝¹, unique := unique✝¹ }.src g,
      { src := src₁, hom := hom₁, obj_src := obj_src✝¹, map_hom := map_hom✝¹, unique := unique✝¹ }.hom g⟩ =
    ⟨{ src := src₁, hom := hom₂, obj_src := obj_src✝, map_hom := map_hom✝, unique := unique✝ }.src g,
      { src := src₁, hom := hom₂, obj_src := obj_src✝, map_hom := map_hom✝, unique := unique✝ }.hom g⟩b:Bc:Cg:b ⟶ p.obj c⊢ hom₁ g = hom₂ g
    exact eq_of_heq (Sigma.mk.inj_iff.1 (h g)).2C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration psrc₁:{b : B} → {c : C} → (b ⟶ p.obj c) → Chom₁:{b : B} → {c : C} → (g : b ⟶ p.obj c) → src₁ g ⟶ cobj_src✝¹:∀ {b : B} {c : C} (g : b ⟶ p.obj c), p.obj (src₁ g) = bmap_hom✝¹:∀ {b : B} {c : C} (g : b ⟶ p.obj c), p.map (hom₁ g) = eqToHom ⋯ ≫ gunique✝¹:∀ {b : B} {c : C} (g : b ⟶ p.obj c) {c' : C} (h : c' ⟶ c) (e : p.obj c' = b),
  p.map h = eqToHom e ≫ g → ⟨c', h⟩ = ⟨src₁ g, hom₁ g⟩hom₂:{b : B} → {c : C} → (g : b ⟶ p.obj c) → src₁ g ⟶ cobj_src✝:∀ {b : B} {c : C} (g : b ⟶ p.obj c), p.obj (src₁ g) = bmap_hom✝:∀ {b : B} {c : C} (g : b ⟶ p.obj c), p.map (hom₂ g) = eqToHom ⋯ ≫ gunique✝:∀ {b : B} {c : C} (g : b ⟶ p.obj c) {c' : C} (h : c' ⟶ c) (e : p.obj c' = b),
  p.map h = eqToHom e ≫ g → ⟨c', h⟩ = ⟨src₁ g, hom₂ g⟩h:∀ {b : B} {c : C} (g : b ⟶ p.obj c),
  ⟨{ src := src₁, hom := hom₁, obj_src := obj_src✝¹, map_hom := map_hom✝¹, unique := unique✝¹ }.src g,
      { src := src₁, hom := hom₁, obj_src := obj_src✝¹, map_hom := map_hom✝¹, unique := unique✝¹ }.hom g⟩ =
    ⟨{ src := src₁, hom := hom₂, obj_src := obj_src✝, map_hom := map_hom✝, unique := unique✝ }.src g,
      { src := src₁, hom := hom₂, obj_src := obj_src✝, map_hom := map_hom✝, unique := unique✝ }.hom g⟩hh:hom₁ = hom₂⊢ { src := src₁, hom := hom₁, obj_src := obj_src✝¹, map_hom := map_hom✝¹, unique := unique✝¹ } =
  { src := src₁, hom := hom₂, obj_src := obj_src✝, map_hom := map_hom✝, unique := unique✝ }
  subst hhC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration psrc₁:{b : B} → {c : C} → (b ⟶ p.obj c) → Chom₁:{b : B} → {c : C} → (g : b ⟶ p.obj c) → src₁ g ⟶ cobj_src✝¹:∀ {b : B} {c : C} (g : b ⟶ p.obj c), p.obj (src₁ g) = bmap_hom✝¹:∀ {b : B} {c : C} (g : b ⟶ p.obj c), p.map (hom₁ g) = eqToHom ⋯ ≫ gunique✝¹:∀ {b : B} {c : C} (g : b ⟶ p.obj c) {c' : C} (h : c' ⟶ c) (e : p.obj c' = b),
  p.map h = eqToHom e ≫ g → ⟨c', h⟩ = ⟨src₁ g, hom₁ g⟩obj_src✝:∀ {b : B} {c : C} (g : b ⟶ p.obj c), p.obj (src₁ g) = bmap_hom✝:∀ {b : B} {c : C} (g : b ⟶ p.obj c), p.map (hom₁ g) = eqToHom ⋯ ≫ gunique✝:∀ {b : B} {c : C} (g : b ⟶ p.obj c) {c' : C} (h : c' ⟶ c) (e : p.obj c' = b),
  p.map h = eqToHom e ≫ g → ⟨c', h⟩ = ⟨src₁ g, hom₁ g⟩h:∀ {b : B} {c : C} (g : b ⟶ p.obj c),
  ⟨{ src := src₁, hom := hom₁, obj_src := obj_src✝¹, map_hom := map_hom✝¹, unique := unique✝¹ }.src g,
      { src := src₁, hom := hom₁, obj_src := obj_src✝¹, map_hom := map_hom✝¹, unique := unique✝¹ }.hom g⟩ =
    ⟨{ src := src₁, hom := hom₁, obj_src := obj_src✝, map_hom := map_hom✝, unique := unique✝ }.src g,
      { src := src₁, hom := hom₁, obj_src := obj_src✝, map_hom := map_hom✝, unique := unique✝ }.hom g⟩⊢ { src := src₁, hom := hom₁, obj_src := obj_src✝¹, map_hom := map_hom✝¹, unique := unique✝¹ } =
  { src := src₁, hom := hom₁, obj_src := obj_src✝, map_hom := map_hom✝, unique := unique✝ }
  rflAll goals completed! 🐙

end DiscreteFibration

Mathlib's `IsHomLift`

Mathlib's IsHomLift is the proposition Arrow.mk (p.map φ) = Arrow.mk f.

theorem isHomLift_iff_arrow_mk_eq (p : C ⥤ B) {R S : B} {a b : C}
    (f : R ⟶ S) (φ : a ⟶ b) :
    p.IsHomLift f φ ↔ Arrow.mk (p.map φ) = Arrow.mk f := byC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BR:BS:Ba:Cb:Cf:R ⟶ Sφ:a ⟶ b⊢ p.IsHomLift f φ ↔ Arrow.mk (p.map φ) = Arrow.mk f
  constructormpC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BR:BS:Ba:Cb:Cf:R ⟶ Sφ:a ⟶ b⊢ p.IsHomLift f φ → Arrow.mk (p.map φ) = Arrow.mk fmprC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BR:BS:Ba:Cb:Cf:R ⟶ Sφ:a ⟶ b⊢ Arrow.mk (p.map φ) = Arrow.mk f → p.IsHomLift f φ
  ·mpC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BR:BS:Ba:Cb:Cf:R ⟶ Sφ:a ⟶ b⊢ p.IsHomLift f φ → Arrow.mk (p.map φ) = Arrow.mk f intro hmpC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BR:BS:Ba:Cb:Cf:R ⟶ Sφ:a ⟶ bh:p.IsHomLift f φ⊢ Arrow.mk (p.map φ) = Arrow.mk f
    exact (Arrow.mk_eq_mk_iff _ _).2
      ⟨IsHomLift.domain_eq p f φ, IsHomLift.codomain_eq p f φ,
        IsHomLift.fac' p f φ⟩All goals completed! 🐙
  ·mprC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BR:BS:Ba:Cb:Cf:R ⟶ Sφ:a ⟶ b⊢ Arrow.mk (p.map φ) = Arrow.mk f → p.IsHomLift f φ intro hmprC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BR:BS:Ba:Cb:Cf:R ⟶ Sφ:a ⟶ bh:Arrow.mk (p.map φ) = Arrow.mk f⊢ p.IsHomLift f φ
    obtain ⟨hR, hS, hf⟩ := (Arrow.mk_eq_mk_iff _ _).1 hmprC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BR:BS:Ba:Cb:Cf:R ⟶ Sφ:a ⟶ bh:Arrow.mk (p.map φ) = Arrow.mk fhR:p.obj a = RhS:p.obj b = Shf:p.map φ = eqToHom hR ≫ f ≫ eqToHom ⋯⊢ p.IsHomLift f φ
    exact IsHomLift.of_fac' p f φ hR hS hfAll goals completed! 🐙

              namespace DiscreteFibrationvariable {p : C ⥤ B} (D : DiscreteFibration p)include D

The lift of g as an arrow of C.

def liftArrow {b : B} {c : C} (g : b ⟶ p.obj c) : Arrow C :=
  Arrow.mk (D.hom g)

The image of the lift of g is g, as an equality of arrows.

theorem arrow_mk_map_hom {b : B} {c : C} (g : b ⟶ p.obj c) :
    Arrow.mk (p.map (D.hom g)) = Arrow.mk g :=
  (Arrow.mk_eq_mk_iff _ _).2 ⟨D.obj_src g, rfl, byC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pb:Bc:Cg:b ⟶ p.obj c⊢ p.map (D.hom g) = eqToHom ⋯ ≫ g ≫ eqToHom ⋯ simp [D.map_hom]All goals completed! 🐙⟩

The lift of g lies over g in mathlib's sense.

theorem isHomLift_hom {b : B} {c : C} (g : b ⟶ p.obj c) :
    p.IsHomLift g (D.hom g) :=
  (isHomLift_iff_arrow_mk_eq p g (D.hom g)).2 (D.arrow_mk_map_hom g)

Uniqueness of lifts, Arrow-style.

theorem eq_liftArrow {b : B} {c : C} (g : b ⟶ p.obj c) {c' : C}
    (h : c' ⟶ c) (hh : Arrow.mk (p.map h) = Arrow.mk g) :
    Arrow.mk h = D.liftArrow g := byC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pb:Bc:Cg:b ⟶ p.obj cc':Ch:c' ⟶ chh:Arrow.mk (p.map h) = Arrow.mk g⊢ Arrow.mk h = D.liftArrow g
  obtain ⟨e, hY, hf⟩ := (Arrow.mk_eq_mk_iff _ _).1 hhC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pb:Bc:Cg:b ⟶ p.obj cc':Ch:c' ⟶ chh:Arrow.mk (p.map h) = Arrow.mk ge:p.obj c' = bhY:p.obj c = p.obj chf:p.map h = eqToHom e ≫ g ≫ eqToHom ⋯⊢ Arrow.mk h = D.liftArrow g
  have hu := D.unique g h e (byC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pb:Bc:Cg:b ⟶ p.obj cc':Ch:c' ⟶ chh:Arrow.mk (p.map h) = Arrow.mk ge:p.obj c' = bhY:p.obj c = p.obj chf:p.map h = eqToHom e ≫ g ≫ eqToHom ⋯⊢ p.map h = eqToHom e ≫ g simpa using hfAll goals completed! 🐙)C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pb:Bc:Cg:b ⟶ p.obj cc':Ch:c' ⟶ chh:Arrow.mk (p.map h) = Arrow.mk ge:p.obj c' = bhY:p.obj c = p.obj chf:p.map h = eqToHom e ≫ g ≫ eqToHom ⋯hu:⟨c', h⟩ = ⟨D.src g, D.hom g⟩⊢ Arrow.mk h = D.liftArrow g
  obtain ⟨h1, h2⟩ := Sigma.mk.inj_iff.1 huC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pb:Bc:Cg:b ⟶ p.obj cc':Ch:c' ⟶ chh:Arrow.mk (p.map h) = Arrow.mk ge:p.obj c' = bhY:p.obj c = p.obj chf:p.map h = eqToHom e ≫ g ≫ eqToHom ⋯hu:⟨c', h⟩ = ⟨D.src g, D.hom g⟩h1:c' = D.src gh2:h ≍ D.hom g⊢ Arrow.mk h = D.liftArrow g
  simp only [liftArrow]C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pb:Bc:Cg:b ⟶ p.obj cc':Ch:c' ⟶ chh:Arrow.mk (p.map h) = Arrow.mk ge:p.obj c' = bhY:p.obj c = p.obj chf:p.map h = eqToHom e ≫ g ≫ eqToHom ⋯hu:⟨c', h⟩ = ⟨D.src g, D.hom g⟩h1:c' = D.src gh2:h ≍ D.hom g⊢ Arrow.mk h = Arrow.mk (D.hom g)
  subst h1C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pb:Bc:Cg:b ⟶ p.obj chY:p.obj c = p.obj ch:D.src g ⟶ chh:Arrow.mk (p.map h) = Arrow.mk ge:p.obj (D.src g) = bhf:p.map h = eqToHom e ≫ g ≫ eqToHom ⋯hu:⟨D.src g, h⟩ = ⟨D.src g, D.hom g⟩h2:h ≍ D.hom g⊢ Arrow.mk h = Arrow.mk (D.hom g)
  rw [eq_of_heq h2C:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pb:Bc:Cg:b ⟶ p.obj chY:p.obj c = p.obj ch:D.src g ⟶ chh:Arrow.mk (p.map h) = Arrow.mk ge:p.obj (D.src g) = bhf:p.map h = eqToHom e ≫ g ≫ eqToHom ⋯hu:⟨D.src g, h⟩ = ⟨D.src g, D.hom g⟩h2:h ≍ D.hom g⊢ Arrow.mk (D.hom g) = Arrow.mk (D.hom g)]All goals completed! 🐙

A morphism lying over an identity has equal endpoints.

theorem eq_of_isHomLift_id {S : B} {a b : C} (ψ : a ⟶ b)
    [p.IsHomLift (𝟙 S) ψ] : a = b :=
  (D.src_eq (eqToHom (IsHomLift.codomain_eq p (𝟙 S) ψ).symm) ψ
      (IsHomLift.domain_eq p (𝟙 S) ψ)
      (byC:Type u₁inst✝²:Category.{v₁, u₁} CB:Type u₂inst✝¹:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pS:Ba:Cb:Cψ:a ⟶ binst✝:p.IsHomLift (𝟙 S) ψ⊢ p.map ψ = eqToHom ⋯ ≫ eqToHom ⋯ simpa using IsHomLift.fac' p (𝟙 S) ψAll goals completed! 🐙)).symm.trans
    (D.src_eq (eqToHom (IsHomLift.codomain_eq p (𝟙 S) ψ).symm) (𝟙 b)
      (IsHomLift.codomain_eq p (𝟙 S) ψ) (byC:Type u₁inst✝²:Category.{v₁, u₁} CB:Type u₂inst✝¹:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pS:Ba:Cb:Cψ:a ⟶ binst✝:p.IsHomLift (𝟙 S) ψ⊢ p.map (𝟙 b) = eqToHom ⋯ ≫ eqToHom ⋯ simpAll goals completed! 🐙))

The endpoints of a morphism of a fibre agree. With fiber_hom_ext below, the fibres of a discrete fibration are discrete categories.

theorem fiber_eq_of_hom {S : B} {a b : p.Fiber S} (φ : a ⟶ b) : a = b :=
  Functor.Fiber.fiberInclusion_obj_inj
    (D.eq_of_isHomLift_id (S := S) (Functor.Fiber.fiberInclusion.map φ))

Parallel morphisms of a fibre agree, since p is faithful.

theorem fiber_hom_ext {S : B} {a b : p.Fiber S} (φ ψ : a ⟶ b) : φ = ψ :=
  Functor.Fiber.hom_ext (D.map_injective
    ((IsHomLift.fac' p (𝟙 S) (Functor.Fiber.fiberInclusion.map φ)).trans
      (IsHomLift.fac' p (𝟙 S) (Functor.Fiber.fiberInclusion.map ψ)).symm))

Every morphism over f is cartesian in mathlib's sense: uniqueness of lifts supplies the universal property outright.

theorem isCartesian {R S : B} {a b : C} (f : R ⟶ S) (φ : a ⟶ b)
    [p.IsHomLift f φ] : p.IsCartesian f φ where
  universal_property {a'} φ' _ := byC:Type u₁inst✝²:Category.{v₁, u₁} CB:Type u₂inst✝¹:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pR:BS:Ba:Cb:Cf:R ⟶ Sφ:a ⟶ binst✝:p.IsHomLift f φa':Cφ':a' ⟶ bx✝:p.IsHomLift f φ'⊢ ∃! χ, p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ = φ'
    have key : (⟨a', φ'⟩ : Σ c, c ⟶ b) = ⟨a, φ⟩ :=
      (D.unique (f ≫ eqToHom (IsHomLift.codomain_eq p f φ).symm) φ'
          (IsHomLift.domain_eq p f φ')
          (byC:Type u₁inst✝²:Category.{v₁, u₁} CB:Type u₂inst✝¹:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pR:BS:Ba:Cb:Cf:R ⟶ Sφ:a ⟶ binst✝:p.IsHomLift f φa':Cφ':a' ⟶ bx✝:p.IsHomLift f φ'⊢ p.map φ' = eqToHom ⋯ ≫ f ≫ eqToHom ⋯ simpa using IsHomLift.fac' p f φ'All goals completed! 🐙)).trans
        (D.unique (f ≫ eqToHom (IsHomLift.codomain_eq p f φ).symm) φ
          (IsHomLift.domain_eq p f φ)
          (byC:Type u₁inst✝²:Category.{v₁, u₁} CB:Type u₂inst✝¹:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pR:BS:Ba:Cb:Cf:R ⟶ Sφ:a ⟶ binst✝:p.IsHomLift f φa':Cφ':a' ⟶ bx✝:p.IsHomLift f φ'⊢ p.map φ = eqToHom ⋯ ≫ f ≫ eqToHom ⋯ simpa using IsHomLift.fac' p f φAll goals completed! 🐙)).symmC:Type u₁inst✝²:Category.{v₁, u₁} CB:Type u₂inst✝¹:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pR:BS:Ba:Cb:Cf:R ⟶ Sφ:a ⟶ binst✝:p.IsHomLift f φa':Cφ':a' ⟶ bx✝:p.IsHomLift f φ'key:⟨a', φ'⟩ = ⟨a, φ⟩⊢ ∃! χ, p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ = φ'
    obtain ⟨ha, hφ⟩ := Sigma.mk.inj_iff.1 keyC:Type u₁inst✝²:Category.{v₁, u₁} CB:Type u₂inst✝¹:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pR:BS:Ba:Cb:Cf:R ⟶ Sφ:a ⟶ binst✝:p.IsHomLift f φa':Cφ':a' ⟶ bx✝:p.IsHomLift f φ'key:⟨a', φ'⟩ = ⟨a, φ⟩ha:a' = ahφ:φ' ≍ φ⊢ ∃! χ, p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ = φ'
    subst haC:Type u₁inst✝²:Category.{v₁, u₁} CB:Type u₂inst✝¹:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pR:BS:Bb:Cf:R ⟶ Sa':Cφ':a' ⟶ bx✝:p.IsHomLift f φ'φ:a' ⟶ binst✝:p.IsHomLift f φkey:⟨a', φ'⟩ = ⟨a', φ⟩hφ:φ' ≍ φ⊢ ∃! χ, p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ = φ'
    obtain rfl := eq_of_heq hφC:Type u₁inst✝²:Category.{v₁, u₁} CB:Type u₂inst✝¹:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pR:BS:Bb:Cf:R ⟶ Sa':Cφ':a' ⟶ bx✝:p.IsHomLift f φ'inst✝:p.IsHomLift f φ'key:⟨a', φ'⟩ = ⟨a', φ'⟩hφ:φ' ≍ φ'⊢ ∃! χ, p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ' = φ'
    refine ⟨𝟙 _, ⟨IsHomLift.id (IsHomLift.domain_eq p f φ'),
      Category.id_comp _⟩, fun χ hχ => D.map_injective ?_⟩C:Type u₁inst✝²:Category.{v₁, u₁} CB:Type u₂inst✝¹:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pR:BS:Bb:Cf:R ⟶ Sa':Cφ':a' ⟶ bx✝:p.IsHomLift f φ'inst✝:p.IsHomLift f φ'key:⟨a', φ'⟩ = ⟨a', φ'⟩hφ:φ' ≍ φ'χ:a' ⟶ a'hχ:(fun χ ↦ p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ' = φ') χ⊢ p.map χ = p.map (𝟙 a')
    have := hχ.1C:Type u₁inst✝²:Category.{v₁, u₁} CB:Type u₂inst✝¹:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pR:BS:Bb:Cf:R ⟶ Sa':Cφ':a' ⟶ bx✝:p.IsHomLift f φ'inst✝:p.IsHomLift f φ'key:⟨a', φ'⟩ = ⟨a', φ'⟩hφ:φ' ≍ φ'χ:a' ⟶ a'hχ:(fun χ ↦ p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ' = φ') χthis:p.IsHomLift (𝟙 R) χ⊢ p.map χ = p.map (𝟙 a')
    rw [p.map_idC:Type u₁inst✝²:Category.{v₁, u₁} CB:Type u₂inst✝¹:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pR:BS:Bb:Cf:R ⟶ Sa':Cφ':a' ⟶ bx✝:p.IsHomLift f φ'inst✝:p.IsHomLift f φ'key:⟨a', φ'⟩ = ⟨a', φ'⟩hφ:φ' ≍ φ'χ:a' ⟶ a'hχ:(fun χ ↦ p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ' = φ') χthis:p.IsHomLift (𝟙 R) χ⊢ p.map χ = 𝟙 (p.obj a')]C:Type u₁inst✝²:Category.{v₁, u₁} CB:Type u₂inst✝¹:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pR:BS:Bb:Cf:R ⟶ Sa':Cφ':a' ⟶ bx✝:p.IsHomLift f φ'inst✝:p.IsHomLift f φ'key:⟨a', φ'⟩ = ⟨a', φ'⟩hφ:φ' ≍ φ'χ:a' ⟶ a'hχ:(fun χ ↦ p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ' = φ') χthis:p.IsHomLift (𝟙 R) χ⊢ p.map χ = 𝟙 (p.obj a')
    simpa using IsHomLift.fac' p (𝟙 R) χAll goals completed! 🐙

Every object of C admits a cartesian lift of every morphism into its image.

theorem isPreFibered : p.IsPreFibered where
  exists_isCartesian' f :=
    ⟨D.src f, D.hom f, have := D.isHomLift_hom f; D.isCartesian _ _⟩

A discrete fibration is a fibred category.

theorem isFibered : p.IsFibered where
  toIsPreFibered := D.isPreFibered
  comp := byC:Type u₁inst✝¹:Category.{v₁, u₁} CB:Type u₂inst✝:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration p⊢ ∀ {R S T : B} (f : R ⟶ S) (g : S ⟶ T) {a b c : C} (φ : a ⟶ b) (ψ : b ⟶ c) [p.IsCartesian f φ] [p.IsCartesian g ψ],
  p.IsCartesian (f ≫ g) (φ ≫ ψ)
    intro _ _ _ f g _ _ _ φ ψ _ _C:Type u₁inst✝³:Category.{v₁, u₁} CB:Type u₂inst✝²:Category.{v₂, u₂} Bp:C ⥤ BD:DiscreteFibration pR✝:BS✝:BT✝:Bf:R✝ ⟶ S✝g:S✝ ⟶ T✝a✝:Cb✝:Cc✝:Cφ:a✝ ⟶ b✝ψ:b✝ ⟶ c✝inst✝¹:p.IsCartesian f φinst✝:p.IsCartesian g ψ⊢ p.IsCartesian (f ≫ g) (φ ≫ ψ)
    exact D.isCartesian (f ≫ g) (φ ≫ ψ)All goals completed! 🐙

end DiscreteFibrationend CategoryTheory