Skip to content

Instantly share code, notes, and snippets.

@madnight

madnight/identity_is_isomorphism.v

Created October 7, 2023 21:01
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save madnight/4d00970f1944a66113d7f04465af20f8 to your computer and use it in GitHub Desktop.
Save madnight/4d00970f1944a66113d7f04465af20f8 to your computer and use it in GitHub Desktop.
Download ZIP
Proof that Identity Morphism is an Isomorphism
Raw
identity_is_isomorphism.v
Section IdentityIsomorphism.
Variable Obj : Type.
Variable Hom : Obj -> Obj -> Type.
Variable id : forall A : Obj, Hom A A.
Variable composition : forall {X Y Z : Obj}, Hom Y Z -> Hom X Y -> Hom X Z.
Notation "g 'o' f" := (composition g f) (at level 50).
Hypothesis id_left : forall A B : Obj, forall f : Hom A B, (id B) o f = f.
Hypothesis id_right : forall A B : Obj, forall f : Hom A B, f o (id A) = f.
Proposition identity_is_isomorphism : forall A : Obj, (id A) o (id A) = id A.
Proof.
intros A.
rewrite <- id_right.
reflexivity.
Qed.
End IdentityIsomorphism.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment