-- The canonical inclusion graph of a subset
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Set.Inclusion
import Function

-- Its codomain can be larger than its domain. The only mathematical
-- obligation is the stated inclusion; graph and application laws are derived.
defgraph inclusionMap (A B : Set) (x ∈ A) : B := x
requires subset : A ⊆ B
proof
  unfold Subset at subset
  exact subset with x, member