Skip to content

Commit

Permalink
Add two missing duals (#2122)
Browse files Browse the repository at this point in the history
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
  • Loading branch information
TwoFX and mergify[bot] committed Mar 10, 2020
1 parent 699401b commit 36ac916
Showing 1 changed file with 4 additions and 0 deletions.
4 changes: 4 additions & 0 deletions src/category_theory/limits/shapes/equalizers.lean
Original file line number Diff line number Diff line change
Expand Up @@ -185,6 +185,10 @@ def cofork.of_π {P : C} (π : Y ⟶ P) (w : f ≫ π = g ≫ π) : cofork f g :
(fork.of_ι ι w).π.app zero = ι := rfl
@[simp] lemma fork.of_ι_app_one {P : C} (ι : P ⟶ X) (w : ι ≫ f = ι ≫ g) :
(fork.of_ι ι w).π.app one = ι ≫ f := rfl
@[simp] lemma cofork.of_π_app_zero {P : C} (π : Y ⟶ P) (w : f ≫ π = g ≫ π) :
(cofork.of_π π w).ι.app zero = f ≫ π := rfl
@[simp] lemma cofork.of_π_app_one {P : C} (π : Y ⟶ P) (w : f ≫ π = g ≫ π) :
(cofork.of_π π w).ι.app one = π := rfl

def fork.ι (t : fork f g) := t.π.app zero
def cofork.π (t : cofork f g) := t.ι.app one
Expand Down

0 comments on commit 36ac916

Please sign in to comment.