Skip to content

Commit

Permalink
rename opposite initial/terminal instances
Browse files Browse the repository at this point in the history
Signed-off-by: Ali Caglayan <[email protected]>

<!-- ps-id: 55a4d338-836f-4570-b7da-31bc9702dde5 -->
  • Loading branch information
Alizter committed Jul 4, 2024
1 parent 093e98e commit e28fbfa
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions theories/WildCat/Opposite.v
Original file line number Diff line number Diff line change
Expand Up @@ -127,10 +127,10 @@ Proof.
refine (@isequiv_Htpy_path _ _ _ _ _ H0 b a f g).
Defined.

Global Instance isinitial_isterminal_op {A : Type} `{Is1Cat A} (x : A)
Global Instance isinitial_op_isterminal {A : Type} `{Is1Cat A} (x : A)
{t : IsTerminal x} : IsInitial (A := A^op) x
:= t.

Global Instance isterminal_isinitial_op {A : Type} `{Is1Cat A} (x : A)
Global Instance isterminal_op_isinitial {A : Type} `{Is1Cat A} (x : A)
{i : IsInitial x} : IsTerminal (A := A^op) x
:= i.

0 comments on commit e28fbfa

Please sign in to comment.