chore(category_theory/*): provide aliases quiver.hom.le and has_le.le…

….hom (#7677)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/category/Module/limits.lean

@@ -147,7 +147,7 @@ variables (f : Π i j, i ≤ j → G i →ₗ[R] G j) [module.directed_system G
 @[simps]
 def direct_limit_diagram : ι ⥤ Module R :=
 { obj := λ i, Module.of R (G i),
-  map := λ i j hij, f i j (le_of_hom hij),
+  map := λ i j hij, f i j hij.le,
   map_id' := λ i, by { ext x, apply module.directed_system.map_self },
   map_comp' := λ i j k hij hjk,
   begin

src/category_theory/category/default.lean

@@ -260,6 +260,7 @@ Because we do not allow the morphisms of a category to live in `Prop`,
 unfortunately we need to use `plift` and `ulift` when defining the morphisms.
 
 As convenience functions, we provide `hom_of_le` and `le_of_hom` to wrap and unwrap inequalities.
+We also provide aliases `has_le.le.hom` and `quiver.hom.le` to use with dot notation.
 -/
 namespace preorder
 
@@ -291,19 +292,21 @@ Express an inequality as a morphism in the corresponding preorder category.
 -/
 def hom_of_le {U V : α} (h : U ≤ V) : U ⟶ V := ulift.up (plift.up h)
 
-@[simp] lemma hom_of_le_refl {U : α} : hom_of_le (le_refl U) = 𝟙 U := rfl
+alias hom_of_le ← has_le.le.hom
+
+@[simp] lemma hom_of_le_refl {U : α} : (le_refl U).hom = 𝟙 U := rfl
 @[simp] lemma hom_of_le_comp {U V W : α} (h : U ≤ V) (k : V ≤ W) :
-  hom_of_le h ≫ hom_of_le k = hom_of_le (h.trans k) := rfl
+  h.hom ≫ k.hom = (h.trans k).hom := rfl
 
 /--
 Extract the underlying inequality from a morphism in a preorder category.
 -/
 lemma le_of_hom {U V : α} (h : U ⟶ V) : U ≤ V := h.down.down
 
-@[simp] lemma le_of_hom_hom_of_le {a b : α} (h : a ≤ b) :
-  le_of_hom (hom_of_le h) = h := rfl
-@[simp] lemma hom_of_le_le_of_hom {a b : α} (h : a ⟶ b) :
-  hom_of_le (le_of_hom h) = h :=
+alias le_of_hom ← quiver.hom.le
+
+@[simp] lemma le_of_hom_hom_of_le {a b : α} (h : a ≤ b) : h.hom.le = h := rfl
+@[simp] lemma hom_of_le_le_of_hom {a b : α} (h : a ⟶ b) : h.le.hom = h :=
 by { cases h, cases h, refl, }
 
 end category_theory

src/category_theory/category/pairwise.lean

@@ -143,7 +143,7 @@ def cocone_is_colimit : is_colimit (cocone U) :=
   begin
     apply complete_lattice.Sup_le,
     rintros _ ⟨j, rfl⟩,
-    exact le_of_hom (s.ι.app (single j))
+    exact (s.ι.app (single j)).le
   end }
 
 end

src/category_theory/equivalence.lean

@@ -563,9 +563,8 @@ def equivalence.to_order_iso (e : α ≌ β) : α ≃o β :=
   left_inv := λ a, (e.unit_iso.app a).to_eq.symm,
   right_inv := λ b, (e.counit_iso.app b).to_eq,
   map_rel_iff' := λ a a',
-    ⟨λ h, le_of_hom
-      ((equivalence.unit e).app a ≫ e.inverse.map (hom_of_le h) ≫ (equivalence.unit_inv e).app a'),
-     λ (h : a ≤ a'), le_of_hom (e.functor.map (hom_of_le h))⟩, }
+    ⟨λ h, ((equivalence.unit e).app a ≫ e.inverse.map h.hom ≫ (equivalence.unit_inv e).app a').le,
+     λ (h : a ≤ a'), (e.functor.map h.hom).le⟩, }
 
 -- `@[simps]` on `equivalence.to_order_iso` produces lemmas that fail the `simp_nf` linter,
 -- so we provide them by hand:

src/category_theory/functor.lean

@@ -106,7 +106,7 @@ end
 
 @[mono] lemma monotone {α β : Type*} [preorder α] [preorder β] (F : α ⥤ β) :
   monotone F.obj :=
-λ a b h, le_of_hom (F.map (hom_of_le h))
+λ a b h, (F.map h.hom).le
 
 end functor
 

src/category_theory/isomorphism.lean

@@ -390,8 +390,7 @@ end functor
 section partial_order
 variables {α β : Type*} [partial_order α] [partial_order β]
 
-lemma iso.to_eq {X Y : α} (f : X ≅ Y) : X = Y :=
-le_antisymm (le_of_hom f.hom) (le_of_hom f.inv)
+lemma iso.to_eq {X Y : α} (f : X ≅ Y) : X = Y := le_antisymm f.hom.le f.inv.le
 
 end partial_order
 

src/category_theory/limits/lattice.lean

@@ -47,7 +47,7 @@ def limit_cone [complete_lattice α] (F : J ⥤ α) : limit_cone F :=
     { app := λ j, hom_of_le (complete_lattice.Inf_le _ _ (set.mem_range_self _)) } },
   is_limit :=
   { lift := λ s, hom_of_le (complete_lattice.le_Inf _ _
-    begin rintros _ ⟨j, rfl⟩, exact le_of_hom (s.π.app j), end) } }
+    begin rintros _ ⟨j, rfl⟩, exact (s.π.app j).le, end) } }
 
 /--
 The colimit cocone over any functor into a complete lattice.
@@ -59,7 +59,7 @@ def colimit_cocone [complete_lattice α] (F : J ⥤ α) : colimit_cocone F :=
     { app := λ j, hom_of_le (complete_lattice.le_Sup _ _ (set.mem_range_self _)) } },
   is_colimit :=
   { desc := λ s, hom_of_le (complete_lattice.Sup_le _ _
-    begin rintros _ ⟨j, rfl⟩, exact le_of_hom (s.ι.app j), end) } }
+    begin rintros _ ⟨j, rfl⟩, exact (s.ι.app j).le, end) } }
 
 -- It would be nice to only use the `Inf` half of the complete lattice, but
 -- this seems not to have been described separately.

src/category_theory/opposites.lean

@@ -419,18 +419,16 @@ universes v
 variables {α : Type v} [preorder α]
 
 /-- Construct a morphism in the opposite of a preorder category from an inequality. -/
-def op_hom_of_le {U V : αᵒᵖ} (h : unop V ≤ unop U) : U ⟶ V :=
-quiver.hom.op (hom_of_le h)
+def op_hom_of_le {U V : αᵒᵖ} (h : unop V ≤ unop U) : U ⟶ V := h.hom.op
 
-lemma le_of_op_hom {U V : αᵒᵖ} (h : U ⟶ V) : unop V ≤ unop U :=
-le_of_hom (h.unop)
+lemma le_of_op_hom {U V : αᵒᵖ} (h : U ⟶ V) : unop V ≤ unop U := h.unop.le
 
 namespace functor
 
 variables (C)
 variables (D : Type u₂) [category.{v₂} D]
 
-/-- 
+/--
 The equivalence of functor categories induced by `op` and `unop`.
 -/
 @[simps]

src/category_theory/sites/spaces.lean

@@ -45,7 +45,7 @@ def grothendieck_topology : grothendieck_topology (opens T) :=
   top_mem' := λ X x hx, ⟨_, 𝟙 _, trivial, hx⟩,
   pullback_stable' := λ X Y S f hf y hy,
   begin
-    rcases hf y (le_of_hom f hy) with ⟨U, g, hg, hU⟩,
+    rcases hf y (f.le hy) with ⟨U, g, hg, hU⟩,
     refine ⟨U ⊓ Y, hom_of_le inf_le_right, _, hU, hy⟩,
     apply S.downward_closed hg (hom_of_le inf_le_left),
   end,
@@ -60,10 +60,10 @@ def grothendieck_topology : grothendieck_topology (opens T) :=
 def pretopology : pretopology (opens T) :=
 { coverings := λ X R, ∀ x ∈ X, ∃ U (f : U ⟶ X), R f ∧ x ∈ U,
   has_isos := λ X Y f i x hx,
-        by exactI ⟨_, _, presieve.singleton_self _, le_of_hom (inv f) hx⟩,
+        by exactI ⟨_, _, presieve.singleton_self _, (inv f).le hx⟩,
   pullbacks := λ X Y f S hS x hx,
   begin
-    rcases hS _ (le_of_hom f hx) with ⟨U, g, hg, hU⟩,
+    rcases hS _ (f.le hx) with ⟨U, g, hg, hU⟩,
     refine ⟨_, _, presieve.pullback_arrows.mk _ _ hg, _⟩,
     have : U ⊓ Y ≤ pullback g f,
       refine le_of_hom (pullback.lift (hom_of_le inf_le_left) (hom_of_le inf_le_right) rfl),

src/category_theory/skeletal.lean

@@ -152,7 +152,7 @@ variables {C} {D}
 def map (F : C ⥤ D) : thin_skeleton C ⥤ thin_skeleton D :=
 { obj := quotient.map F.obj $ λ X₁ X₂ ⟨hX⟩, ⟨F.map_iso hX⟩,
   map := λ X Y, quotient.rec_on_subsingleton₂ X Y $
-           λ x y k, hom_of_le ((le_of_hom k).elim (λ t, ⟨F.map t⟩)) }
+           λ x y k, hom_of_le (k.le.elim (λ t, ⟨F.map t⟩)) }
 
 lemma comp_to_thin_skeleton (F : C ⥤ D) : F ⋙ to_thin_skeleton D = to_thin_skeleton C ⋙ map F :=
 rfl
@@ -172,11 +172,11 @@ def map₂ (F : C ⥤ D ⥤ E) :
                 (λ X₁ X₂ ⟨hX⟩ Y₁ Y₂ ⟨hY⟩, ⟨(F.obj X₁).map_iso hY ≪≫ (F.map_iso hX).app Y₂⟩) x y,
     map := λ y₁ y₂, quotient.rec_on_subsingleton x $
             λ X, quotient.rec_on_subsingleton₂ y₁ y₂ $
-              λ Y₁ Y₂ hY, hom_of_le ((le_of_hom hY).elim (λ g, ⟨(F.obj X).map g⟩)) },
+              λ Y₁ Y₂ hY, hom_of_le (hY.le.elim (λ g, ⟨(F.obj X).map g⟩)) },
   map := λ x₁ x₂, quotient.rec_on_subsingleton₂ x₁ x₂ $
            λ X₁ X₂ f,
            { app := λ y, quotient.rec_on_subsingleton y
-              (λ Y, hom_of_le ((le_of_hom f).elim (λ f', ⟨(F.map f').app Y⟩))) } }
+              (λ Y, hom_of_le (f.le.elim (λ f', ⟨(F.map f').app Y⟩))) } }
 
 variables (C)
 
@@ -192,7 +192,7 @@ noncomputable def from_thin_skeleton : thin_skeleton C ⥤ C :=
   map := λ x y, quotient.rec_on_subsingleton₂ x y $
     λ X Y f,
             (nonempty.some (quotient.mk_out X)).hom
-          ≫ (le_of_hom f).some
+          ≫ f.le.some
           ≫ (nonempty.some (quotient.mk_out Y)).inv }
 
 noncomputable instance from_thin_skeleton_equivalence : is_equivalence (from_thin_skeleton C) :=
@@ -218,7 +218,7 @@ instance thin_skeleton_partial_order : partial_order (thin_skeleton C) :=
   ..category_theory.thin_skeleton.preorder C }
 
 lemma skeletal : skeletal (thin_skeleton C) :=
-λ X Y, quotient.induction_on₂ X Y $ λ x y h, h.elim $ λ i, (le_of_hom i.1).antisymm (le_of_hom i.2)
+λ X Y, quotient.induction_on₂ X Y $ λ x y h, h.elim $ λ i, i.1.le.antisymm i.2.le
 
 lemma map_comp_eq (F : E ⥤ D) (G : D ⥤ C) : map (F ⋙ G) = map F ⋙ map G :=
 functor.eq_of_iso skeletal $

src/category_theory/subobject/basic.lean

@@ -237,7 +237,7 @@ eq_mk_of_comm _ ((underlying_iso f).trans i) $ by simp [w]
 -- it is possible to see its source and target
 -- (`h` will just display as `_`, because it is in `Prop`).
 def of_le {B : C} (X Y : subobject B) (h : X ≤ Y) : (X : C) ⟶ (Y : C) :=
-underlying.map $ hom_of_le h
+underlying.map $ h.hom
 
 @[simp, reassoc] lemma of_le_arrow {B : C} {X Y : subobject B} (h : X ≤ Y) :
   of_le X Y h ≫ Y.arrow = X.arrow :=

src/category_theory/subobject/lattice.lean

@@ -386,13 +386,8 @@ inf_eq_map_pullback' f₁ f₂
 lemma prod_eq_inf {A : C} {f₁ f₂ : subobject A} [has_binary_product f₁ f₂] :
   (f₁ ⨯ f₂) = f₁ ⊓ f₂ :=
 le_antisymm
-  (_root_.le_inf
-    (le_of_hom limits.prod.fst)
-    (le_of_hom limits.prod.snd))
-  (le_of_hom
-    (prod.lift
-      (hom_of_le _root_.inf_le_left)
-      (hom_of_le _root_.inf_le_right)))
+  (_root_.le_inf (limits.prod.fst).le (limits.prod.snd).le)
+  ((prod.lift (_root_.inf_le_left.hom) (_root_.inf_le_right.hom))).le
 
 lemma inf_def {B : C} (m m' : subobject B) :
   m ⊓ m' = (inf.obj m).obj m' := rfl

src/category_theory/subobject/types.lean

@@ -46,7 +46,7 @@ def types.mono_over_equivalence_set (α : Type u) : mono_over α ≌ set α :=
     end, },
   inverse :=
   { obj := λ s, mono_over.mk' (subtype.val : s → α),
-    map := λ s t b, mono_over.hom_mk (λ w, ⟨w.1, set.mem_of_mem_of_subset w.2 (le_of_hom b)⟩)
+    map := λ s t b, mono_over.hom_mk (λ w, ⟨w.1, set.mem_of_mem_of_subset w.2 b.le⟩)
       (by { ext, simp, }), },
   unit_iso := nat_iso.of_components
     (λ f, mono_over.iso_mk

src/topology/category/Profinite/as_limit.lean

@@ -41,7 +41,7 @@ variables (X : Profinite.{u})
 /-- The functor `discrete_quotient X ⥤ Fintype` whose limit is isomorphic to `X`. -/
 def fintype_diagram : discrete_quotient X ⥤ Fintype :=
 { obj := λ S, Fintype.of S,
-  map := λ S T f, discrete_quotient.of_le $ le_of_hom f }
+  map := λ S T f, discrete_quotient.of_le f.le }
 
 /-- An abbreviation for `X.fintype_diagram ⋙ Fintype_to_Profinite`. -/
 abbreviation diagram : discrete_quotient X ⥤ Profinite :=

src/topology/category/Top/limits.lean

@@ -130,11 +130,11 @@ begin
   classical,
   use λ (j' : Jᵒᵖ),
     if h : j'.unop ≤ j.unop then
-      F.map (hom_of_le h).op (classical.arbitrary (F.obj j))
+      F.map h.hom.op (classical.arbitrary (F.obj j))
     else
       classical.arbitrary _,
   intros j' fle,
-  simp only [dif_pos (le_of_hom fle.unop)],
+  simp only [dif_pos fle.unop.le, dif_pos le_rfl],
   dsimp, simp,
 end
 

src/topology/category/Top/open_nhds.lean

@@ -47,7 +47,7 @@ by {unfold open_nhds, apply_instance}
 
 instance opens_nhds_hom_has_coe_to_fun {x : X} {U V : open_nhds x} : has_coe_to_fun (U ⟶ V) :=
 { F := λ f, U.1 → V.1,
-  coe := λ f x, ⟨x, (le_of_hom f) x.2⟩ }
+  coe := λ f x, ⟨x, f.le x.2⟩ }
 
 /--
 The inclusion `U ⊓ V ⟶ U` as a morphism in the category of open sets.

src/topology/category/Top/opens.lean

@@ -44,7 +44,7 @@ the morphisms `U ⟶ V` are not just proofs `U ≤ V`, but rather
 
 instance opens_hom_has_coe_to_fun {U V : opens X} : has_coe_to_fun (U ⟶ V) :=
 { F := λ f, U → V,
-  coe := λ f x, ⟨x, (le_of_hom f) x.2⟩ }
+  coe := λ f x, ⟨x, f.le x.2⟩ }
 
 /-!
 We now construct as morphisms various inclusions of open sets.
@@ -54,32 +54,27 @@ We now construct as morphisms various inclusions of open sets.
 /--
 The inclusion `U ⊓ V ⟶ U` as a morphism in the category of open sets.
 -/
-def inf_le_left (U V : opens X) : U ⊓ V ⟶ U :=
-hom_of_le inf_le_left
+def inf_le_left (U V : opens X) : U ⊓ V ⟶ U := inf_le_left.hom
 
 /--
 The inclusion `U ⊓ V ⟶ V` as a morphism in the category of open sets.
 -/
-def inf_le_right (U V : opens X) : U ⊓ V ⟶ V :=
-hom_of_le inf_le_right
+def inf_le_right (U V : opens X) : U ⊓ V ⟶ V := inf_le_right.hom
 
 /--
 The inclusion `U i ⟶ supr U` as a morphism in the category of open sets.
 -/
-def le_supr {ι : Type*} (U : ι → opens X) (i : ι) : U i ⟶ supr U :=
-hom_of_le (le_supr U i)
+def le_supr {ι : Type*} (U : ι → opens X) (i : ι) : U i ⟶ supr U := (le_supr U i).hom
 
 /--
 The inclusion `⊥ ⟶ U` as a morphism in the category of open sets.
 -/
-def bot_le (U : opens X) : ⊥ ⟶ U :=
-hom_of_le bot_le
+def bot_le (U : opens X) : ⊥ ⟶ U := bot_le.hom
 
 /--
 The inclusion `U ⟶ ⊤` as a morphism in the category of open sets.
 -/
-def le_top (U : opens X) : U ⟶ ⊤ :=
-hom_of_le le_top
+def le_top (U : opens X) : U ⟶ ⊤ := le_top.hom
 
 -- We do not mark this as a simp lemma because it breaks open `x`.
 -- Nevertheless, it is useful in `sheaf_of_functions`.
@@ -103,12 +98,12 @@ realising each open set as a topological space itself.
 -/
 def to_Top (X : Top.{u}) : opens X ⥤ Top :=
 { obj := λ U, ⟨U.val, infer_instance⟩,
-  map := λ U V i, ⟨λ x, ⟨x.1, (le_of_hom i) x.2⟩,
+  map := λ U V i, ⟨λ x, ⟨x.1, i.le x.2⟩,
     (embedding.continuous_iff embedding_subtype_coe).2 continuous_induced_dom⟩ }
 
 @[simp]
 lemma to_Top_map (X : Top.{u}) {U V : opens X} {f : U ⟶ V} {x} {h} :
-  ((to_Top X).map f) ⟨x, h⟩ = ⟨x, (le_of_hom f) h⟩ :=
+  ((to_Top X).map f) ⟨x, h⟩ = ⟨x, f.le h⟩ :=
 rfl
 
 /--
@@ -126,7 +121,7 @@ is_open.open_embedding_subtype_coe U.2
     given by taking preimages under f. -/
 def map (f : X ⟶ Y) : opens Y ⥤ opens X :=
 { obj := λ U, ⟨ f ⁻¹' U.val, U.property.preimage f.continuous ⟩,
-  map := λ U V i, ⟨ ⟨ λ a b, (le_of_hom i) b ⟩ ⟩ }.
+  map := λ U V i, ⟨ ⟨ λ a b, i.le b ⟩ ⟩ }.
 
 @[simp] lemma map_obj (f : X ⟶ Y) (U) (p) :
   (map f).obj ⟨U, p⟩ = ⟨f ⁻¹' U, p.preimage f.continuous⟩ := rfl

src/topology/sheaves/local_predicate.lean

@@ -67,7 +67,7 @@ Continuity is a "prelocal" predicate on functions to a fixed topological space `
 @[simps]
 def continuous_prelocal (T : Top.{v}) : prelocal_predicate (λ x : X, T) :=
 { pred := λ U f, continuous f,
-  res := λ U V i f h, continuous.comp h (opens.open_embedding_of_le (le_of_hom i)).continuous, }
+  res := λ U V i f h, continuous.comp h (opens.open_embedding_of_le i.le).continuous, }
 
 /-- Satisfying the inhabited linter. -/
 instance inhabited_prelocal_predicate (T : Top.{v}) : inhabited (prelocal_predicate (λ x : X, T)) :=
@@ -105,7 +105,7 @@ def continuous_local (T : Top.{v}) : local_predicate (λ x : X, T) :=
      dsimp at w,
      rw continuous_iff_continuous_at at w,
      specialize w ⟨x, m⟩,
-     simpa using (opens.open_embedding_of_le (le_of_hom i)).continuous_at_iff.1 w,
+     simpa using (opens.open_embedding_of_le i.le).continuous_at_iff.1 w,
    end,
   ..continuous_prelocal X T }
 

src/topology/sheaves/sheaf_condition/opens_le_cover.lean

@@ -67,7 +67,7 @@ def index (V : opens_le_cover U) : ι := V.property.some
 The morphism from `V` to `U i` for some `i`.
 -/
 def hom_to_index (V : opens_le_cover U) : V.val ⟶ U (index V) :=
-hom_of_le (V.property.some_spec)
+(V.property.some_spec).hom
 
 end opens_le_cover
 
@@ -150,36 +150,35 @@ instance : cofinal (pairwise_to_opens_le_cover U) :=
   dsimp at *,
   { refine ⟨[
     { left := punit.star, right := pair i i',
-      hom := hom_of_le (le_inf (le_of_hom a) (le_of_hom b)), }, _], _, rfl⟩,
+      hom := (le_inf a.le b.le).hom, }, _], _, rfl⟩,
     exact
       list.chain.cons (or.inr ⟨{ left := 𝟙 _, right := left i i', }⟩)
         (list.chain.cons (or.inl ⟨{ left := 𝟙 _, right := right i i', }⟩) list.chain.nil) },
   { refine ⟨[
     { left := punit.star, right := pair i' i,
-      hom := hom_of_le (le_inf ((le_of_hom b).trans inf_le_left) (le_of_hom a)), },
+      hom := (le_inf (b.le.trans inf_le_left) a.le).hom, },
     { left := punit.star, right := single i',
-      hom := hom_of_le ((le_of_hom b).trans inf_le_left), }, _], _, rfl⟩,
+      hom := (b.le.trans inf_le_left).hom, }, _], _, rfl⟩,
     exact
       list.chain.cons (or.inr ⟨{ left := 𝟙 _, right := right i' i, }⟩)
         (list.chain.cons (or.inl ⟨{ left := 𝟙 _, right := left i' i, }⟩)
           (list.chain.cons (or.inr ⟨{ left := 𝟙 _, right := left i' j', }⟩) list.chain.nil)) },
   { refine ⟨[
     { left := punit.star, right := single i,
-      hom := hom_of_le ((le_of_hom a).trans inf_le_left), },
+      hom := (a.le.trans inf_le_left).hom, },
     { left := punit.star, right := pair i i', hom :=
-      hom_of_le (le_inf ((le_of_hom a).trans inf_le_left) (le_of_hom b)), }, _], _, rfl⟩,
+      (le_inf (a.le.trans inf_le_left) b.le).hom, }, _], _, rfl⟩,
     exact
       list.chain.cons (or.inl ⟨{ left := 𝟙 _, right := left i j, }⟩)
         (list.chain.cons (or.inr ⟨{ left := 𝟙 _, right := left i i', }⟩)
           (list.chain.cons (or.inl ⟨{ left := 𝟙 _, right := right i i', }⟩) list.chain.nil)) },
   { refine ⟨[
     { left := punit.star, right := single i,
-      hom := hom_of_le ((le_of_hom a).trans inf_le_left), },
+      hom := (a.le.trans inf_le_left).hom, },
     { left := punit.star, right := pair i i',
-      hom :=
-        hom_of_le (le_inf ((le_of_hom a).trans inf_le_left) ((le_of_hom b).trans inf_le_left)), },
+      hom := (le_inf (a.le.trans inf_le_left) (b.le.trans inf_le_left)).hom, },
     { left := punit.star, right := single i',
-      hom := hom_of_le ((le_of_hom b).trans inf_le_left), }, _], _, rfl⟩,
+      hom := (b.le.trans inf_le_left).hom, }, _], _, rfl⟩,
     exact
       list.chain.cons (or.inl ⟨{ left := 𝟙 _, right := left i j, }⟩)
       (list.chain.cons (or.inr ⟨{ left := 𝟙 _, right := left i i', }⟩)