File tree Expand file tree Collapse file tree 2 files changed +2
-2
lines changed
Mathlib/CategoryTheory/ObjectProperty Expand file tree Collapse file tree 2 files changed +2
-2
lines changed Original file line number Diff line number Diff line change @@ -40,7 +40,7 @@ instance nonempty_sup_right [Q.Nonempty] : (P ⊔ Q).Nonempty :=
4040
4141instance nonempty_top [_root_.Nonempty C] : Nonempty (⊤ : ObjectProperty C) :=
4242 nonempty_of_prop (X := Classical.arbitrary C) (by trivial)
43-
43+
4444lemma isoClosure_sup : (P ⊔ Q).isoClosure = P.isoClosure ⊔ Q.isoClosure := by
4545 ext X
4646 simp only [prop_sup_iff]
Original file line number Diff line number Diff line change @@ -150,7 +150,7 @@ lemma prop_initial [P.IsClosedUnderColimitsOfShape (Discrete.{0} PEmpty)] [HasIn
150150
151151-- see Note [lower instance priority]
152152instance (priority := 100 ) [P.IsClosedUnderColimitsOfShape (Discrete.{0 } PEmpty)] [HasInitial C] :
153- P.Nonempty :=
153+ P.Nonempty :=
154154 nonempty_of_prop P.prop_initial
155155
156156lemma IsClosedUnderBinaryCoproducts.closedUnderIsomorphisms [HasInitial C]
You can’t perform that action at this time.
0 commit comments