This artifact contains the Coq formalization associated with the paper The Duality of Subtyping submitted in ECOOP 2020. This document explains how to run the Coq formalization. Artifact can either be compiled in the pre-built docker image with all the dependencies installed or it could be built from the scratch. Section 1 explains how to get the docker image for the artifact. Section 2 explains the prerequisites and the steps to run coq files from scratch. Section 3 explains coq files briefly.