defn: Add id₂ to Cat.Reasoning

the1lab · May 15, 2022 · 9f8475d · 9f8475d
1 parent bf86b57
commit 9f8475d
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/Cat/Reasoning.lagda.md b/src/Cat/Reasoning.lagda.md
@@ -37,6 +37,9 @@ id-comm {f = f} = idr f ∙ sym (idl f)
 id-comm-sym : ∀ {a b} {f : Hom a b} → id ∘ f ≡ f ∘ id
 id-comm-sym {f = f} = idl f ∙ sym (idr f)
 
+id₂ : ∀ {a} → id ∘ id ≡ id {a}
+id₂ = idl id
+
 module _ (a≡id : a ≡ id) where
 
   eliml : a ∘ f ≡ f