A9

Theorem: is-univalent f ⇒ x ∈ Dom f ⇒ f ⦇ { x } ⦈ = { f @ x }
Proof:
  Assuming `is-univalent f`, `x ∈ Dom f`:
      Using “Set extensionality”:
          true
        ≡⟨ “True ∀ body”, “Reflexivity of ≡” ⟩
          ∀ a • a ∈ { f @ x } ≡ a ∈ { f @ x }
        ≡⟨ “Singleton set membership” ⟩
          ∀ a • a = f @ x ≡ a ∈ { f @ x }
        ≡⟨ “Partial-function application” with Assumption `is-univalent f` `x ∈ Dom f`  ⟩
          ∀ a • (x ⦗ f ⦘ a) ≡ a ∈ { f @ x }
        ≡⟨ Substitution ⟩
          ∀ a • (b ⦗ f ⦘ a)[b ≔ x] ≡ a ∈ { f @ x }
        ≡⟨ “One-point rule for ∃”, “Trading for ∃” ⟩
          ∀ a • (∃ b • x = b ∧ b ⦗ f ⦘ a) ≡ a ∈ { f @ x }
        ≡⟨ “Singleton set membership” ⟩
          ∀ a • (∃ b • b ∈ { x }  ∧ b ⦗ f ⦘ a) ≡ a ∈ { f @ x }
        ≡⟨ “Trading for ∃” ⟩
          ∀ a • (∃ b ❙ b ∈ { x } • b ⦗ f ⦘ a) ≡ a ∈ { f @ x }
        ≡⟨ “Relational image” ⟩
          ∀ a • a ∈ f ⦇ { x } ⦈ ≡ a ∈ { f @ x }

Theorem “Relationship with @”:
  is-univalent f ⇒ x ∈ Dom f ⇒ x ⦗ f ⦘ (f @ x)
Proof:
    Assuming `is-univalent f`, `x ∈ Dom f`:
        x ⦗ f ⦘ (f @ x)
      ≡⟨ “Partial-function application” with Assumption `is-univalent f` `x ∈ Dom f` ⟩
        (f @ x) = f @ x
      ≡⟨ “Reflexivity of =” ⟩
        true

Theorem “Membership in domain of ⨾”:
    x ∈ Dom (R ⨾ S) ≡ x ∈ Dom R ∧ (∃ y ❙ x ⦗ R ⦘ y • y ∈ Dom S)
Proof:
  Using “Mutual implication”:
    Subproof for `x ∈ Dom (R ⨾ S) ⇒ x ∈ Dom R ∧ (∃ y ❙ x ⦗ R ⦘ y • y ∈ Dom S)`:
      Assuming `x ∈ Dom (R ⨾ S)`:
          true
        ≡⟨ Assumption `x ∈ Dom (R ⨾ S)` ⟩
          x ∈ Dom (R ⨾ S)
        ≡⟨ “Membership in `Dom`” ⟩
          (∃ b • x ⦗ R ⨾ S ⦘ b)
        ≡⟨ “Relation composition” ⟩
          (∃ b • ∃ y • x ⦗ R ⦘ y ∧ y ⦗ S ⦘ b)
        ≡⟨ “Interchange of dummies for ∃” ⟩
          ∃ y • ∃ b • x ⦗ R ⦘ y ∧ y ⦗ S ⦘ b
        ≡⟨ “Distributivity of ∧ over ∃” ⟩
          (∃ y • x ⦗ R ⦘ y ∧ ∃ b • y ⦗ S ⦘ b)
        ≡⟨ “Idempotency of ∧” ⟩
          (∃ y • x ⦗ R ⦘ y ∧ ∃ b • y ⦗ S ⦘ b)
          ∧
          (∃ y • x ⦗ R ⦘ y ∧ ∃ b • y ⦗ S ⦘ b)
        ≡⟨ “Trading for ∃” ⟩
          (∃ y • x ⦗ R ⦘ y ∧ ∃ b • y ⦗ S ⦘ b)
          ∧
          (∃ y ❙ x ⦗ R ⦘ y • ∃ b • y ⦗ S ⦘ b)
        ≡⟨ “Membership in `Dom`” ⟩
          (∃ y • x ⦗ R ⦘ y ∧ y ∈ Dom S )
          ∧
          (∃ y ❙ x ⦗ R ⦘ y • ∃ b • y ⦗ S ⦘ b)
        ⇒⟨ Monotonicity with “Weakening” ⟩
          (∃ y • x ⦗ R ⦘ y) ∧ (∃ y ❙ x ⦗ R ⦘ y • (∃ b • y ⦗ S ⦘ b))
        ≡⟨ “Membership in `Dom`” ⟩
          x ∈ Dom R ∧ (∃ y ❙ x ⦗ R ⦘ y • y ∈ Dom S)

    Subproof for `x ∈ Dom R ∧ (∃ y ❙ x ⦗ R ⦘ y • y ∈ Dom S) ⇒ x ∈ Dom (R ⨾ S)`:
      Assuming `x ∈ Dom R ∧ (∃ y ❙ x ⦗ R ⦘ y • y ∈ Dom S)`:
          true
        ≡⟨ Assumption `x ∈ Dom R ∧ (∃ y ❙ x ⦗ R ⦘ y • y ∈ Dom S)` ⟩
          x ∈ Dom R ∧ (∃ y ❙ x ⦗ R ⦘ y • y ∈ Dom S)
        ⇒⟨ “Weakening” ⟩
          ∃ y ❙ x ⦗ R ⦘ y • y ∈ Dom S
        ≡⟨ “Membership in `Dom`” ⟩
          ∃ y ❙ x ⦗ R ⦘ y • ∃ b • y ⦗ S ⦘ b
        ≡⟨ “Nesting for ∃”, “Interchange of dummies for ∃” ⟩
          ∃ b • ∃ y ❙ x ⦗ R ⦘ y • y ⦗ S ⦘ b
        ≡⟨ “Trading for ∃” ⟩
          ∃ b • ∃ y • x ⦗ R ⦘ y ∧ y ⦗ S ⦘ b
        ≡⟨ “Relation composition” ⟩
          ∃ b • x ⦗ R ⨾ S ⦘ b
        ≡⟨ “Membership in `Dom`” ⟩
          x ∈ Dom (R ⨾ S)

Theorem “Partial-function application of ⨾”:
    is-univalent f ⇒
    is-univalent g ⇒
    x ∈ Dom (f ⨾ g) ⇒ (f ⨾ g) @ x = g @ (f @ x)
Proof:
  Assuming `is-univalent f`, `is-univalent g`:
    Assuming `x ∈ Dom (f ⨾ g)` and using with “Membership in domain of ⨾”:
        (f ⨾ g) @ x = g @ (f @ x)
      ≡⟨ “Left-identity of ⇒” ⟩
        true ⇒ (f ⨾ g) @ x = g @ (f @ x)
      ≡⟨ “Univalence of composition” with Assumption `is-univalent f` `is-univalent g` ⟩
        is-univalent (f ⨾ g) ⇒ (f ⨾ g) @ x = g @ (f @ x)
      ≡⟨ “Left-identity of ⇒” ⟩
        true ⇒ is-univalent (f ⨾ g) ⇒ (f ⨾ g) @ x = g @ (f @ x)
      ≡⟨ Assumption `x ∈ Dom (f ⨾ g)` ⟩
        x ∈ Dom f ∧ (∃ y ❙ x ⦗ f ⦘ y • y ∈ Dom g) ⇒ is-univalent (f ⨾ g) ⇒ (f ⨾ g) @ x = g @ (f @ x)
      ≡⟨  “Partial-function application” with Assumption `is-univalent f` `x ∈ Dom (f ⨾ g)` ⟩
        x ∈ Dom f ∧ (∃ y ❙ y = f @ x • y ∈ Dom g) ⇒ is-univalent (f ⨾ g) ⇒ (f ⨾ g) @ x = g @ (f @ x)
      ≡⟨  “Trading for ∃”, “One-point rule for ∃” ⟩
        x ∈ Dom f ∧ (y ∈ Dom g)[y ≔ f @ x] ⇒ is-univalent (f ⨾ g) ⇒ (f ⨾ g) @ x = g @ (f @ x)
      ≡⟨  Substitution, “Shunting” ⟩
        x ∈ Dom f ⇒ f @ x ∈ Dom g ⇒ is-univalent (f ⨾ g) ⇒ (f ⨾ g) @ x = g @ (f @ x)
      ≡⟨  Subproof:
            Assuming `x ∈ Dom f`, `(f @ x) ∈ Dom g`, `is-univalent (f ⨾ g)`:
                (f ⨾ g) @ x = g @ (f @ x)
              ≡⟨ “Partial-function application” with Assumption `is-univalent (f ⨾ g)` `x ∈ Dom (f ⨾ g)` ⟩
                x ⦗ (f ⨾ g) ⦘ (g @ (f @ x))
              ≡⟨ “Relation composition” ⟩
                ∃ b • x ⦗ f ⦘ b ∧ b ⦗ g ⦘ (g @ (f @ x))
              ≡⟨ “Partial-function application” with Assumption `is-univalent f` `x ∈ Dom (f ⨾ g)`  ⟩
                ∃ b • b = f @ x ∧ b ⦗ g ⦘ (g @ (f @ x))
              ≡⟨ “One-point rule for ∃”, “Trading for ∃” ⟩
                (b ⦗ g ⦘ (g @ (f @ x)))[b ≔ f @ x]
              ≡⟨ Substitution ⟩
                f @ x ⦗ g ⦘ (g @ (f @ x))
              ≡⟨ “Partial-function application” with Assumption `is-univalent g` `x ∈ Dom (f ⨾ g)` ⟩
                f @ x ⦗ g ⦘ (g @ (f @ x))
              ≡⟨ “Partial-function application” with Assumption `is-univalent g` `(f @ x) ∈ Dom g` ⟩
                (g @ (f @ x)) = (g @ (f @ x))
              ≡⟨ “Reflexivity of =” ⟩
                true
        ⟩
        true

Theorem “Injectivity and @”:
    is-univalent f ⇒
    is-injective f ⇒
    x₁ ∈ Dom f ⇒
    x₂ ∈ Dom f ⇒
    (f @ x₁ = f @ x₂ ≡ x₁ = x₂)
Proof:
  Assuming `is-univalent f`, `is-injective f`, `x₁ ∈ Dom f`, `x₂ ∈ Dom f`:
    Using “Mutual implication”:
      Subproof for `(f @ x₁ = f @ x₂ ⇒ x₁ = x₂)`:
        Assuming `f @ x₁ = f @ x₂`:
            true
          ≡⟨ “Identity of ∧”, “Relationship with @” with Assumption `is-univalent f` `x₁ ∈ Dom f` `x₂ ∈ Dom f` ⟩
            x₂ ⦗ f ⦘ (f @ x₂) ∧ x₁ ⦗ f ⦘ (f @ x₁)
          ≡⟨ Assumption `f @ x₁ = f @ x₂` ⟩
            x₂ ⦗ f ⦘ (f @ x₂) ∧ x₁ ⦗ f ⦘ (f @ x₂)
          ⇒⟨ Assumption `is-injective f` with “Injectivity” ⟩
            x₁ = x₂
      Subproof for `x₁ = x₂ ⇒ f @ x₁ = f @ x₂`:
        Assuming `x₁ = x₂`:
            true
          ≡⟨ “Identity of ∧”, “Relationship with @” with Assumption `is-univalent f` `x₁ ∈ Dom f` `x₂ ∈ Dom f` ⟩
            x₂ ⦗ f ⦘ (f @ x₂) ∧ x₁ ⦗ f ⦘ (f @ x₁)
          ≡⟨ Assumption `x₁ = x₂` ⟩
            x₁ ⦗ f ⦘ (f @ x₂) ∧ x₁ ⦗ f ⦘ (f @ x₁)
          ⇒⟨ Assumption `is-univalent f` with “Univalence” ⟩
            f @ x₁ = f @ x₂

------ A9.2

Lemma “Subset of intersection”: (Q ∩ R) ⊆ Q
Proof:
    (Q ∩ R) ⊆ Q
  ≡⟨ “Weakening for ∩”, “Identity of ∧” ⟩
    (Q ∩ R) ⊆ Q ∧ (Q ∩ R) ⊆ R ∧ (Q ∩ R) ⊆ Q
  ≡⟨ “Characterisation of ∩” ⟩
    (Q ∩ R) ⊆ (Q ∩ R) ∩ Q
  ≡⟨ “Symmetry of ∩”, “Associativity of ∩” ⟩
    (Q ∩ R) ⊆ (Q ∩ Q) ∩ R
  ≡⟨ “Idempotency of ∩” ⟩
    (Q ∩ R) ⊆ Q ∩ R
  ≡⟨ “Reflexivity of ⊆” ⟩
    true

Theorem “Modal rule”:
    (Q ⨾ R) ∩ S ⊆ (Q ∩ S ⨾ R ˘) ⨾ R
Proof:
    (Q ⨾ R) ∩ S
  ⊆⟨ “Dedekind rule” ⟩
    ((Q ∩ S ⨾ R ˘) ⨾ (R ∩ Q ˘ ⨾ S))
  ⊆⟨ “Sub-distributivity of ⨾ over ∩” ⟩
    ((Q ∩ S ⨾ R ˘) ⨾ R ) ∩ ((Q ∩ S ⨾ R ˘) ⨾ (Q ˘ ⨾ S))
  ⊆⟨ “Subset of intersection” ⟩
    (Q ∩ S ⨾ R ˘) ⨾ R

Theorem “Modal rule”:
    (Q ⨾ R) ∩ S ⊆ Q ⨾ (R ∩ Q ˘ ⨾ S)
Proof:
    (Q ⨾ R) ∩ S
  ⊆⟨ “Dedekind rule” ⟩
    (Q ∩ S ⨾ R ˘) ⨾ (R ∩ Q ˘ ⨾ S)
  ⊆⟨ “Sub-distributivity of ⨾ over ∩” ⟩
    (Q ⨾ (R ∩ Q ˘ ⨾ S)) ∩ (S ⨾ R ˘  ⨾ (R ∩ Q ˘ ⨾ S))
  ⊆⟨ “Subset of intersection” ⟩
    Q ⨾ (R ∩ Q ˘ ⨾ S)

Theorem “Hesitation”: R ⊆ R ⨾ R ˘ ⨾ R
Proof:
    R
  =⟨ “Idempotency of ∩”, “Reflexivity of ⊆” ⟩
    R ∩ R
  =⟨ “Identity of ⨾” ⟩
    R ⨾ Id ∩ R
  ⊆⟨ “Modal rule” ⟩
    R ⨾ (Id ∩ R ˘ ⨾ R)
  ⊆⟨ “Sub-distributivity of ⨾ over ∩” ⟩
    (R ⨾ Id ∩ R ⨾ R ˘ ⨾ R)
  ⊆⟨ “Subset of intersection” ⟩
    R ⨾ R ˘ ⨾ R

Theorem “PER factoring”:
    is-symmetric Q ⇒ is-transitive Q ⇒  Q ⨾ R ∩ Q = Q ⨾ (R ∩ Q)
Proof:
  Assuming `is-symmetric Q` and using with “Definition of symmetry”:
    Assuming `is-transitive Q` and using with “Definition of transitivity”:
          Q ⨾ R ∩ Q
        ⊆⟨ “Modal rule” ⟩
          Q ⨾ (R ∩ Q ˘ ⨾ Q)
        ⊆⟨ Monotonicity with Assumption `is-symmetric Q`  ⟩
          Q ⨾ (R ∩ Q ⨾ Q)
        ⊆⟨ Monotonicity with Assumption `is-transitive Q`  ⟩
          Q ⨾ (R ∩ Q)
        ⊆⟨ “Sub-distributivity of ⨾ over ∩” ⟩
          (Q ⨾ R) ∩ (Q ⨾ Q)
        ⊆⟨ Monotonicity with Assumption `is-transitive Q` ⟩
          Q ⨾ R ∩ Q

Theorem “Reflexive implies total”:
    is-reflexive R  ⇒  is-total R
Proof:
    is-reflexive R  ⇒  is-total R
  ≡⟨ “Idempotency of ∧” ⟩
    (is-reflexive R ∧ is-reflexive R)  ⇒  is-total R
  ≡⟨ “Reflexivity of converse”, “Shunting” ⟩
    is-reflexive (R ˘) ⇒ is-reflexive R  ⇒  is-total R
  ≡⟨  Subproof:
         Assuming `is-reflexive (R ˘)`, `is-reflexive R`:
             is-total R
           ≡⟨ “Definition of totality” ⟩
             Id ⊆ R ⨾ R ˘
           ≡⟨ “Definition of reflexivity” ⟩
             is-reflexive (R ⨾ R ˘)
           ≡⟨ “Reflexivity of ⨾” with Assumption `is-reflexive (R ˘)` `is-reflexive R` ⟩
             true
    ⟩
    true

Theorem “Idempotency from symmetric and transitive”:
    is-symmetric R ⇒ is-transitive R ⇒ is-idempotent R
Proof:
    is-symmetric R ⇒ is-transitive R ⇒ is-idempotent R
  ≡⟨ “Definition of idempotency” ⟩
    is-symmetric R ⇒ is-transitive R ⇒ R ⨾ R = R
  ≡⟨  Subproof:
        Assuming `is-symmetric R` and using with “Definition of symmetry”:
          Assuming `is-transitive R` and using with “Definition of transitivity”:
                  R ⨾ R
                ⊆⟨ Assumption `is-transitive R` ⟩
                  R
                ⊆⟨ “Hesitation” ⟩
                  R ⨾ R ˘ ⨾ R
                ⊆⟨ Monotonicity with Assumption `is-symmetric R` ⟩
                  R ⨾ R ⨾ R
                ⊆⟨ Monotonicity with Assumption `is-transitive R` ⟩
                  R ⨾ R
    ⟩
    true

Theorem “Right-distributivity of ⨾ with univalent over ∩”:
    is-univalent F  ⇒  F ⨾ (R ∩ S) = F ⨾ R ∩ F ⨾ S
Proof:
  Assuming `is-univalent F` and using with “Definition of univalence”:
      F ⨾ (R ∩ S)
    ⊆⟨ “Sub-distributivity of ⨾ over ∩” ⟩
      F ⨾ R ∩ (F ⨾ S)
    ⊆⟨ “Modal rule” ⟩
      F ⨾ (R ∩ F ˘ ⨾ (F ⨾ S))
    =⟨ “Associativity of ⨾” ⟩
      F ⨾ (R ∩ (F ˘ ⨾ F) ⨾ S)
    ⊆⟨ Monotonicity with Assumption `is-univalent F` ⟩
      F ⨾ (R ∩ Id ⨾ S)
    =⟨ “Identity of ⨾” ⟩
      F ⨾ (R ∩ S)

Theorem “Swapping mapping across ⊆”:
    is-mapping F  ⇒  (R ⨾ F ⊆ S  ≡  R ⊆ S ⨾ F ˘)
Proof:
    is-mapping F  ⇒  (R ⨾ F ⊆ S  ≡  R ⊆ S ⨾ F ˘)
  ≡⟨ “Definition of mappings” ⟩
    F ˘ ⨾ F ⊆ Id ∧ Id ⊆ F ⨾ F ˘  ⇒  (R ⨾ F ⊆ S  ≡  R ⊆ S ⨾ F ˘)
  ≡⟨ “Shunting” ⟩
    F ˘ ⨾ F ⊆ Id ⇒ Id ⊆ F ⨾ F ˘  ⇒  (R ⨾ F ⊆ S  ≡  R ⊆ S ⨾ F ˘)
  ≡⟨  Subproof:
        Assuming `F ˘ ⨾ F ⊆ Id` , `Id ⊆ F ⨾ F ˘`:
            R ⨾ F ⊆ S
          ⇒⟨ “Monotonicity of ⨾” ⟩
            R ⨾ F ⨾ F ˘ ⊆ S ⨾ F ˘
          ⇒⟨ Antitonicity with Assumption `Id ⊆ F ⨾ F ˘` ⟩
            R ⨾ Id ⊆ S ⨾ F ˘
          ≡⟨ “Identity of ⨾” ⟩
            R ⊆ S ⨾ F ˘
          ⇒⟨ “Monotonicity of ⨾”  ⟩
            R ⨾ F ⊆ S ⨾ F ˘ ⨾ F
          ⇒⟨ Monotonicity with Assumption `F ˘ ⨾ F ⊆ Id` ⟩
            R ⨾ F ⊆ S ⨾ Id
          ≡⟨ “Identity of ⨾” ⟩
            R ⨾ F ⊆ S
    ⟩
      true