Test 2

Problem 1 (p. 204)

Suppose X^{↻\alpha} \xrightarrow{f} Y^{↻\beta} is a map in 𝑺↻. Show that if \alpha has a fixed point, then \beta must also have a fixed point.

Solution: Problem 1

The sequence of rewrites in the example below mirrors Danilo's solution on p. 205.

example (X Y : SetWithEndomap) (f : X ⟶ Y) :
    (∃ x ∈ X.carrier, X.toEnd x = x) →
    (∃ y ∈ Y.carrier, Y.toEnd y = y) := byX:SetWithEndomapY:SetWithEndomapf:X ⟶ Y⊢ (∃ x ∈ X.carrier, X.toEnd x = x) → ∃ y ∈ Y.carrier, Y.toEnd y = y
  obtain ⟨f, hf_mtc, hf_comm⟩ := fX:SetWithEndomapY:SetWithEndomapf:X.t ⟶ Y.thf_mtc:∀ x ∈ X.carrier, f x ∈ Y.carrierhf_comm:f ⊚ X.toEnd = Y.toEnd ⊚ f⊢ (∃ x ∈ X.carrier, X.toEnd x = x) → ∃ y ∈ Y.carrier, Y.toEnd y = y
  intro ⟨x, hx, hα⟩X:SetWithEndomapY:SetWithEndomapf:X.t ⟶ Y.thf_mtc:∀ x ∈ X.carrier, f x ∈ Y.carrierhf_comm:f ⊚ X.toEnd = Y.toEnd ⊚ fx:X.thx:x ∈ X.carrierhα:X.toEnd x = x⊢ ∃ y ∈ Y.carrier, Y.toEnd y = y
  use f xhX:SetWithEndomapY:SetWithEndomapf:X.t ⟶ Y.thf_mtc:∀ x ∈ X.carrier, f x ∈ Y.carrierhf_comm:f ⊚ X.toEnd = Y.toEnd ⊚ fx:X.thx:x ∈ X.carrierhα:X.toEnd x = x⊢ f x ∈ Y.carrier ∧ Y.toEnd (f x) = f x
  constructorh.leftX:SetWithEndomapY:SetWithEndomapf:X.t ⟶ Y.thf_mtc:∀ x ∈ X.carrier, f x ∈ Y.carrierhf_comm:f ⊚ X.toEnd = Y.toEnd ⊚ fx:X.thx:x ∈ X.carrierhα:X.toEnd x = x⊢ f x ∈ Y.carrierh.rightX:SetWithEndomapY:SetWithEndomapf:X.t ⟶ Y.thf_mtc:∀ x ∈ X.carrier, f x ∈ Y.carrierhf_comm:f ⊚ X.toEnd = Y.toEnd ⊚ fx:X.thx:x ∈ X.carrierhα:X.toEnd x = x⊢ Y.toEnd (f x) = f x
  ·h.leftX:SetWithEndomapY:SetWithEndomapf:X.t ⟶ Y.thf_mtc:∀ x ∈ X.carrier, f x ∈ Y.carrierhf_comm:f ⊚ X.toEnd = Y.toEnd ⊚ fx:X.thx:x ∈ X.carrierhα:X.toEnd x = x⊢ f x ∈ Y.carrier exact hf_mtc x hxAll goals completed! 🐙
  ·h.rightX:SetWithEndomapY:SetWithEndomapf:X.t ⟶ Y.thf_mtc:∀ x ∈ X.carrier, f x ∈ Y.carrierhf_comm:f ⊚ X.toEnd = Y.toEnd ⊚ fx:X.thx:x ∈ X.carrierhα:X.toEnd x = x⊢ Y.toEnd (f x) = f x rw [← types_comp_apply _ Y.toEnd, ← hf_comm, types_comp_apply,
        hα]All goals completed! 🐙

Problem 2 (p. 204)

Find all maps of (irreflexive) graphs from

inductive A₁
  | a | b

inductive D₁
  | p | q | r

def G₁ : IrreflexiveGraph := {
  tA := A₁
  carrierA := Set.univ
  tD := D₁
  carrierD := Set.univ
  toSrc := fun
    | A₁.a => D₁.p
    | A₁.b => D₁.q
  toSrc_mem := fun _ ↦ Set.mem_univ _
  toTgt := fun
    | A₁.a => D₁.r
    | A₁.b => D₁.r
  toTgt_mem := fun _ ↦ Set.mem_univ _
}

inductive A₂
  | c | d

inductive D₂
  | v | w

def G₂ : IrreflexiveGraph := {
  tA := A₂
  carrierA := Set.univ
  tD := D₂
  carrierD := Set.univ
  toSrc := fun
    | A₂.c => D₂.w
    | A₂.d => D₂.v
  toSrc_mem := fun _ ↦ Set.mem_univ _
  toTgt := fun
    | A₂.c => D₂.w
    | A₂.d => D₂.w
  toTgt_mem := fun _ ↦ Set.mem_univ _
}

(There are not more than a half-dozen of them.)

Solution: Problem 2

There are four maps, as given below (cf. the discussion of Omer's solution on pp. 207–210):

def f₁ : G₁ ⟶ G₂ := {
  val := (
    fun -- maps arrows
      | A₁.a => A₂.d
      | A₁.b => A₂.d,
    fun -- maps dots
      | D₁.p => D₂.v
      | D₁.q => D₂.v
      | D₁.r => D₂.w
  )
  property := by⊢ (∀ x ∈ G₁.carrierA,
    (fun x ↦
            match x with
            | A₁.a => A₂.d
            | A₁.b => A₂.d,
            fun x ↦
            match x with
            | D₁.p => D₂.v
            | D₁.q => D₂.v
            | D₁.r => D₂.w).1
        x ∈
      G₂.carrierA) ∧
  (∀ x ∈ G₁.carrierD,
      (fun x ↦
              match x with
              | A₁.a => A₂.d
              | A₁.b => A₂.d,
              fun x ↦
              match x with
              | D₁.p => D₂.v
              | D₁.q => D₂.v
              | D₁.r => D₂.w).2
          x ∈
        G₂.carrierD) ∧
    (fun x ↦
              match x with
              | A₁.a => A₂.d
              | A₁.b => A₂.d,
              fun x ↦
              match x with
              | D₁.p => D₂.v
              | D₁.q => D₂.v
              | D₁.r => D₂.w).2 ⊚
          G₁.toSrc =
        G₂.toSrc ⊚
          (fun x ↦
              match x with
              | A₁.a => A₂.d
              | A₁.b => A₂.d,
              fun x ↦
              match x with
              | D₁.p => D₂.v
              | D₁.q => D₂.v
              | D₁.r => D₂.w).1 ∧
      (fun x ↦
              match x with
              | A₁.a => A₂.d
              | A₁.b => A₂.d,
              fun x ↦
              match x with
              | D₁.p => D₂.v
              | D₁.q => D₂.v
              | D₁.r => D₂.w).2 ⊚
          G₁.toTgt =
        G₂.toTgt ⊚
          (fun x ↦
              match x with
              | A₁.a => A₂.d
              | A₁.b => A₂.d,
              fun x ↦
              match x with
              | D₁.p => D₂.v
              | D₁.q => D₂.v
              | D₁.r => D₂.w).1
    split_andsrefine_1⊢ ∀ x ∈ G₁.carrierA,
  (fun x ↦
          match x with
          | A₁.a => A₂.d
          | A₁.b => A₂.d,
          fun x ↦
          match x with
          | D₁.p => D₂.v
          | D₁.q => D₂.v
          | D₁.r => D₂.w).1
      x ∈
    G₂.carrierArefine_2.refine_1⊢ ∀ x ∈ G₁.carrierD,
  (fun x ↦
          match x with
          | A₁.a => A₂.d
          | A₁.b => A₂.d,
          fun x ↦
          match x with
          | D₁.p => D₂.v
          | D₁.q => D₂.v
          | D₁.r => D₂.w).2
      x ∈
    G₂.carrierDrefine_2.refine_2.refine_1⊢ (fun x ↦
        match x with
        | A₁.a => A₂.d
        | A₁.b => A₂.d,
        fun x ↦
        match x with
        | D₁.p => D₂.v
        | D₁.q => D₂.v
        | D₁.r => D₂.w).2 ⊚
    G₁.toSrc =
  G₂.toSrc ⊚
    (fun x ↦
        match x with
        | A₁.a => A₂.d
        | A₁.b => A₂.d,
        fun x ↦
        match x with
        | D₁.p => D₂.v
        | D₁.q => D₂.v
        | D₁.r => D₂.w).1refine_2.refine_2.refine_2⊢ (fun x ↦
        match x with
        | A₁.a => A₂.d
        | A₁.b => A₂.d,
        fun x ↦
        match x with
        | D₁.p => D₂.v
        | D₁.q => D₂.v
        | D₁.r => D₂.w).2 ⊚
    G₁.toTgt =
  G₂.toTgt ⊚
    (fun x ↦
        match x with
        | A₁.a => A₂.d
        | A₁.b => A₂.d,
        fun x ↦
        match x with
        | D₁.p => D₂.v
        | D₁.q => D₂.v
        | D₁.r => D₂.w).1
    all_goals
      first | exact fun _ _ ↦ Set.mem_univ _refine_2.refine_2.refine_2⊢ (fun x ↦
        match x with
        | A₁.a => A₂.d
        | A₁.b => A₂.d,
        fun x ↦
        match x with
        | D₁.p => D₂.v
        | D₁.q => D₂.v
        | D₁.r => D₂.w).2 ⊚
    G₁.toTgt =
  G₂.toTgt ⊚
    (fun x ↦
        match x with
        | A₁.a => A₂.d
        | A₁.b => A₂.d,
        fun x ↦
        match x with
        | D₁.p => D₂.v
        | D₁.q => D₂.v
        | D₁.r => D₂.w).1
            | funext xrefine_2.refine_2.refine_2.hx:G₁.tA⊢ ((fun x ↦
          match x with
          | A₁.a => A₂.d
          | A₁.b => A₂.d,
          fun x ↦
          match x with
          | D₁.p => D₂.v
          | D₁.q => D₂.v
          | D₁.r => D₂.w).2 ⊚
      G₁.toTgt)
    x =
  (G₂.toTgt ⊚
      (fun x ↦
          match x with
          | A₁.a => A₂.d
          | A₁.b => A₂.d,
          fun x ↦
          match x with
          | D₁.p => D₂.v
          | D₁.q => D₂.v
          | D₁.r => D₂.w).1)
    x; cases xrefine_2.refine_2.refine_2.h.a⊢ ((fun x ↦
          match x with
          | A₁.a => A₂.d
          | A₁.b => A₂.d,
          fun x ↦
          match x with
          | D₁.p => D₂.v
          | D₁.q => D₂.v
          | D₁.r => D₂.w).2 ⊚
      G₁.toTgt)
    A₁.a =
  (G₂.toTgt ⊚
      (fun x ↦
          match x with
          | A₁.a => A₂.d
          | A₁.b => A₂.d,
          fun x ↦
          match x with
          | D₁.p => D₂.v
          | D₁.q => D₂.v
          | D₁.r => D₂.w).1)
    A₁.arefine_2.refine_2.refine_2.h.b⊢ ((fun x ↦
          match x with
          | A₁.a => A₂.d
          | A₁.b => A₂.d,
          fun x ↦
          match x with
          | D₁.p => D₂.v
          | D₁.q => D₂.v
          | D₁.r => D₂.w).2 ⊚
      G₁.toTgt)
    A₁.b =
  (G₂.toTgt ⊚
      (fun x ↦
          match x with
          | A₁.a => A₂.d
          | A₁.b => A₂.d,
          fun x ↦
          match x with
          | D₁.p => D₂.v
          | D₁.q => D₂.v
          | D₁.r => D₂.w).1)
    A₁.b <;>refine_2.refine_2.refine_2.h.a⊢ ((fun x ↦
          match x with
          | A₁.a => A₂.d
          | A₁.b => A₂.d,
          fun x ↦
          match x with
          | D₁.p => D₂.v
          | D₁.q => D₂.v
          | D₁.r => D₂.w).2 ⊚
      G₁.toTgt)
    A₁.a =
  (G₂.toTgt ⊚
      (fun x ↦
          match x with
          | A₁.a => A₂.d
          | A₁.b => A₂.d,
          fun x ↦
          match x with
          | D₁.p => D₂.v
          | D₁.q => D₂.v
          | D₁.r => D₂.w).1)
    A₁.arefine_2.refine_2.refine_2.h.b⊢ ((fun x ↦
          match x with
          | A₁.a => A₂.d
          | A₁.b => A₂.d,
          fun x ↦
          match x with
          | D₁.p => D₂.v
          | D₁.q => D₂.v
          | D₁.r => D₂.w).2 ⊚
      G₁.toTgt)
    A₁.b =
  (G₂.toTgt ⊚
      (fun x ↦
          match x with
          | A₁.a => A₂.d
          | A₁.b => A₂.d,
          fun x ↦
          match x with
          | D₁.p => D₂.v
          | D₁.q => D₂.v
          | D₁.r => D₂.w).1)
    A₁.b rflAll goals completed! 🐙
}

def f₂ : G₁ ⟶ G₂ := {
  val := (
    fun -- maps arrows
      | A₁.a => A₂.c
      | A₁.b => A₂.c,
    fun -- maps dots
      | D₁.p => D₂.w
      | D₁.q => D₂.w
      | D₁.r => D₂.w
  )
  property := by⊢ (∀ x ∈ G₁.carrierA,
    (fun x ↦
            match x with
            | A₁.a => A₂.c
            | A₁.b => A₂.c,
            fun x ↦
            match x with
            | D₁.p => D₂.w
            | D₁.q => D₂.w
            | D₁.r => D₂.w).1
        x ∈
      G₂.carrierA) ∧
  (∀ x ∈ G₁.carrierD,
      (fun x ↦
              match x with
              | A₁.a => A₂.c
              | A₁.b => A₂.c,
              fun x ↦
              match x with
              | D₁.p => D₂.w
              | D₁.q => D₂.w
              | D₁.r => D₂.w).2
          x ∈
        G₂.carrierD) ∧
    (fun x ↦
              match x with
              | A₁.a => A₂.c
              | A₁.b => A₂.c,
              fun x ↦
              match x with
              | D₁.p => D₂.w
              | D₁.q => D₂.w
              | D₁.r => D₂.w).2 ⊚
          G₁.toSrc =
        G₂.toSrc ⊚
          (fun x ↦
              match x with
              | A₁.a => A₂.c
              | A₁.b => A₂.c,
              fun x ↦
              match x with
              | D₁.p => D₂.w
              | D₁.q => D₂.w
              | D₁.r => D₂.w).1 ∧
      (fun x ↦
              match x with
              | A₁.a => A₂.c
              | A₁.b => A₂.c,
              fun x ↦
              match x with
              | D₁.p => D₂.w
              | D₁.q => D₂.w
              | D₁.r => D₂.w).2 ⊚
          G₁.toTgt =
        G₂.toTgt ⊚
          (fun x ↦
              match x with
              | A₁.a => A₂.c
              | A₁.b => A₂.c,
              fun x ↦
              match x with
              | D₁.p => D₂.w
              | D₁.q => D₂.w
              | D₁.r => D₂.w).1
    split_andsrefine_1⊢ ∀ x ∈ G₁.carrierA,
  (fun x ↦
          match x with
          | A₁.a => A₂.c
          | A₁.b => A₂.c,
          fun x ↦
          match x with
          | D₁.p => D₂.w
          | D₁.q => D₂.w
          | D₁.r => D₂.w).1
      x ∈
    G₂.carrierArefine_2.refine_1⊢ ∀ x ∈ G₁.carrierD,
  (fun x ↦
          match x with
          | A₁.a => A₂.c
          | A₁.b => A₂.c,
          fun x ↦
          match x with
          | D₁.p => D₂.w
          | D₁.q => D₂.w
          | D₁.r => D₂.w).2
      x ∈
    G₂.carrierDrefine_2.refine_2.refine_1⊢ (fun x ↦
        match x with
        | A₁.a => A₂.c
        | A₁.b => A₂.c,
        fun x ↦
        match x with
        | D₁.p => D₂.w
        | D₁.q => D₂.w
        | D₁.r => D₂.w).2 ⊚
    G₁.toSrc =
  G₂.toSrc ⊚
    (fun x ↦
        match x with
        | A₁.a => A₂.c
        | A₁.b => A₂.c,
        fun x ↦
        match x with
        | D₁.p => D₂.w
        | D₁.q => D₂.w
        | D₁.r => D₂.w).1refine_2.refine_2.refine_2⊢ (fun x ↦
        match x with
        | A₁.a => A₂.c
        | A₁.b => A₂.c,
        fun x ↦
        match x with
        | D₁.p => D₂.w
        | D₁.q => D₂.w
        | D₁.r => D₂.w).2 ⊚
    G₁.toTgt =
  G₂.toTgt ⊚
    (fun x ↦
        match x with
        | A₁.a => A₂.c
        | A₁.b => A₂.c,
        fun x ↦
        match x with
        | D₁.p => D₂.w
        | D₁.q => D₂.w
        | D₁.r => D₂.w).1
    all_goals
      first | exact fun _ _ ↦ Set.mem_univ _refine_2.refine_2.refine_2⊢ (fun x ↦
        match x with
        | A₁.a => A₂.c
        | A₁.b => A₂.c,
        fun x ↦
        match x with
        | D₁.p => D₂.w
        | D₁.q => D₂.w
        | D₁.r => D₂.w).2 ⊚
    G₁.toTgt =
  G₂.toTgt ⊚
    (fun x ↦
        match x with
        | A₁.a => A₂.c
        | A₁.b => A₂.c,
        fun x ↦
        match x with
        | D₁.p => D₂.w
        | D₁.q => D₂.w
        | D₁.r => D₂.w).1
            | funext xrefine_2.refine_2.refine_2.hx:G₁.tA⊢ ((fun x ↦
          match x with
          | A₁.a => A₂.c
          | A₁.b => A₂.c,
          fun x ↦
          match x with
          | D₁.p => D₂.w
          | D₁.q => D₂.w
          | D₁.r => D₂.w).2 ⊚
      G₁.toTgt)
    x =
  (G₂.toTgt ⊚
      (fun x ↦
          match x with
          | A₁.a => A₂.c
          | A₁.b => A₂.c,
          fun x ↦
          match x with
          | D₁.p => D₂.w
          | D₁.q => D₂.w
          | D₁.r => D₂.w).1)
    x; cases xrefine_2.refine_2.refine_2.h.a⊢ ((fun x ↦
          match x with
          | A₁.a => A₂.c
          | A₁.b => A₂.c,
          fun x ↦
          match x with
          | D₁.p => D₂.w
          | D₁.q => D₂.w
          | D₁.r => D₂.w).2 ⊚
      G₁.toTgt)
    A₁.a =
  (G₂.toTgt ⊚
      (fun x ↦
          match x with
          | A₁.a => A₂.c
          | A₁.b => A₂.c,
          fun x ↦
          match x with
          | D₁.p => D₂.w
          | D₁.q => D₂.w
          | D₁.r => D₂.w).1)
    A₁.arefine_2.refine_2.refine_2.h.b⊢ ((fun x ↦
          match x with
          | A₁.a => A₂.c
          | A₁.b => A₂.c,
          fun x ↦
          match x with
          | D₁.p => D₂.w
          | D₁.q => D₂.w
          | D₁.r => D₂.w).2 ⊚
      G₁.toTgt)
    A₁.b =
  (G₂.toTgt ⊚
      (fun x ↦
          match x with
          | A₁.a => A₂.c
          | A₁.b => A₂.c,
          fun x ↦
          match x with
          | D₁.p => D₂.w
          | D₁.q => D₂.w
          | D₁.r => D₂.w).1)
    A₁.b <;>refine_2.refine_2.refine_2.h.a⊢ ((fun x ↦
          match x with
          | A₁.a => A₂.c
          | A₁.b => A₂.c,
          fun x ↦
          match x with
          | D₁.p => D₂.w
          | D₁.q => D₂.w
          | D₁.r => D₂.w).2 ⊚
      G₁.toTgt)
    A₁.a =
  (G₂.toTgt ⊚
      (fun x ↦
          match x with
          | A₁.a => A₂.c
          | A₁.b => A₂.c,
          fun x ↦
          match x with
          | D₁.p => D₂.w
          | D₁.q => D₂.w
          | D₁.r => D₂.w).1)
    A₁.arefine_2.refine_2.refine_2.h.b⊢ ((fun x ↦
          match x with
          | A₁.a => A₂.c
          | A₁.b => A₂.c,
          fun x ↦
          match x with
          | D₁.p => D₂.w
          | D₁.q => D₂.w
          | D₁.r => D₂.w).2 ⊚
      G₁.toTgt)
    A₁.b =
  (G₂.toTgt ⊚
      (fun x ↦
          match x with
          | A₁.a => A₂.c
          | A₁.b => A₂.c,
          fun x ↦
          match x with
          | D₁.p => D₂.w
          | D₁.q => D₂.w
          | D₁.r => D₂.w).1)
    A₁.b rflAll goals completed! 🐙
}

def f₃ : G₁ ⟶ G₂ := {
  val := (
    fun -- maps arrows
      | A₁.a => A₂.c
      | A₁.b => A₂.d,
    fun -- maps dots
      | D₁.p => D₂.w
      | D₁.q => D₂.v
      | D₁.r => D₂.w
  )
  property := by⊢ (∀ x ∈ G₁.carrierA,
    (fun x ↦
            match x with
            | A₁.a => A₂.c
            | A₁.b => A₂.d,
            fun x ↦
            match x with
            | D₁.p => D₂.w
            | D₁.q => D₂.v
            | D₁.r => D₂.w).1
        x ∈
      G₂.carrierA) ∧
  (∀ x ∈ G₁.carrierD,
      (fun x ↦
              match x with
              | A₁.a => A₂.c
              | A₁.b => A₂.d,
              fun x ↦
              match x with
              | D₁.p => D₂.w
              | D₁.q => D₂.v
              | D₁.r => D₂.w).2
          x ∈
        G₂.carrierD) ∧
    (fun x ↦
              match x with
              | A₁.a => A₂.c
              | A₁.b => A₂.d,
              fun x ↦
              match x with
              | D₁.p => D₂.w
              | D₁.q => D₂.v
              | D₁.r => D₂.w).2 ⊚
          G₁.toSrc =
        G₂.toSrc ⊚
          (fun x ↦
              match x with
              | A₁.a => A₂.c
              | A₁.b => A₂.d,
              fun x ↦
              match x with
              | D₁.p => D₂.w
              | D₁.q => D₂.v
              | D₁.r => D₂.w).1 ∧
      (fun x ↦
              match x with
              | A₁.a => A₂.c
              | A₁.b => A₂.d,
              fun x ↦
              match x with
              | D₁.p => D₂.w
              | D₁.q => D₂.v
              | D₁.r => D₂.w).2 ⊚
          G₁.toTgt =
        G₂.toTgt ⊚
          (fun x ↦
              match x with
              | A₁.a => A₂.c
              | A₁.b => A₂.d,
              fun x ↦
              match x with
              | D₁.p => D₂.w
              | D₁.q => D₂.v
              | D₁.r => D₂.w).1
    split_andsrefine_1⊢ ∀ x ∈ G₁.carrierA,
  (fun x ↦
          match x with
          | A₁.a => A₂.c
          | A₁.b => A₂.d,
          fun x ↦
          match x with
          | D₁.p => D₂.w
          | D₁.q => D₂.v
          | D₁.r => D₂.w).1
      x ∈
    G₂.carrierArefine_2.refine_1⊢ ∀ x ∈ G₁.carrierD,
  (fun x ↦
          match x with
          | A₁.a => A₂.c
          | A₁.b => A₂.d,
          fun x ↦
          match x with
          | D₁.p => D₂.w
          | D₁.q => D₂.v
          | D₁.r => D₂.w).2
      x ∈
    G₂.carrierDrefine_2.refine_2.refine_1⊢ (fun x ↦
        match x with
        | A₁.a => A₂.c
        | A₁.b => A₂.d,
        fun x ↦
        match x with
        | D₁.p => D₂.w
        | D₁.q => D₂.v
        | D₁.r => D₂.w).2 ⊚
    G₁.toSrc =
  G₂.toSrc ⊚
    (fun x ↦
        match x with
        | A₁.a => A₂.c
        | A₁.b => A₂.d,
        fun x ↦
        match x with
        | D₁.p => D₂.w
        | D₁.q => D₂.v
        | D₁.r => D₂.w).1refine_2.refine_2.refine_2⊢ (fun x ↦
        match x with
        | A₁.a => A₂.c
        | A₁.b => A₂.d,
        fun x ↦
        match x with
        | D₁.p => D₂.w
        | D₁.q => D₂.v
        | D₁.r => D₂.w).2 ⊚
    G₁.toTgt =
  G₂.toTgt ⊚
    (fun x ↦
        match x with
        | A₁.a => A₂.c
        | A₁.b => A₂.d,
        fun x ↦
        match x with
        | D₁.p => D₂.w
        | D₁.q => D₂.v
        | D₁.r => D₂.w).1
    all_goals
      first | exact fun _ _ ↦ Set.mem_univ _refine_2.refine_2.refine_2⊢ (fun x ↦
        match x with
        | A₁.a => A₂.c
        | A₁.b => A₂.d,
        fun x ↦
        match x with
        | D₁.p => D₂.w
        | D₁.q => D₂.v
        | D₁.r => D₂.w).2 ⊚
    G₁.toTgt =
  G₂.toTgt ⊚
    (fun x ↦
        match x with
        | A₁.a => A₂.c
        | A₁.b => A₂.d,
        fun x ↦
        match x with
        | D₁.p => D₂.w
        | D₁.q => D₂.v
        | D₁.r => D₂.w).1
            | funext xrefine_2.refine_2.refine_2.hx:G₁.tA⊢ ((fun x ↦
          match x with
          | A₁.a => A₂.c
          | A₁.b => A₂.d,
          fun x ↦
          match x with
          | D₁.p => D₂.w
          | D₁.q => D₂.v
          | D₁.r => D₂.w).2 ⊚
      G₁.toTgt)
    x =
  (G₂.toTgt ⊚
      (fun x ↦
          match x with
          | A₁.a => A₂.c
          | A₁.b => A₂.d,
          fun x ↦
          match x with
          | D₁.p => D₂.w
          | D₁.q => D₂.v
          | D₁.r => D₂.w).1)
    x; cases xrefine_2.refine_2.refine_2.h.a⊢ ((fun x ↦
          match x with
          | A₁.a => A₂.c
          | A₁.b => A₂.d,
          fun x ↦
          match x with
          | D₁.p => D₂.w
          | D₁.q => D₂.v
          | D₁.r => D₂.w).2 ⊚
      G₁.toTgt)
    A₁.a =
  (G₂.toTgt ⊚
      (fun x ↦
          match x with
          | A₁.a => A₂.c
          | A₁.b => A₂.d,
          fun x ↦
          match x with
          | D₁.p => D₂.w
          | D₁.q => D₂.v
          | D₁.r => D₂.w).1)
    A₁.arefine_2.refine_2.refine_2.h.b⊢ ((fun x ↦
          match x with
          | A₁.a => A₂.c
          | A₁.b => A₂.d,
          fun x ↦
          match x with
          | D₁.p => D₂.w
          | D₁.q => D₂.v
          | D₁.r => D₂.w).2 ⊚
      G₁.toTgt)
    A₁.b =
  (G₂.toTgt ⊚
      (fun x ↦
          match x with
          | A₁.a => A₂.c
          | A₁.b => A₂.d,
          fun x ↦
          match x with
          | D₁.p => D₂.w
          | D₁.q => D₂.v
          | D₁.r => D₂.w).1)
    A₁.b <;>refine_2.refine_2.refine_2.h.a⊢ ((fun x ↦
          match x with
          | A₁.a => A₂.c
          | A₁.b => A₂.d,
          fun x ↦
          match x with
          | D₁.p => D₂.w
          | D₁.q => D₂.v
          | D₁.r => D₂.w).2 ⊚
      G₁.toTgt)
    A₁.a =
  (G₂.toTgt ⊚
      (fun x ↦
          match x with
          | A₁.a => A₂.c
          | A₁.b => A₂.d,
          fun x ↦
          match x with
          | D₁.p => D₂.w
          | D₁.q => D₂.v
          | D₁.r => D₂.w).1)
    A₁.arefine_2.refine_2.refine_2.h.b⊢ ((fun x ↦
          match x with
          | A₁.a => A₂.c
          | A₁.b => A₂.d,
          fun x ↦
          match x with
          | D₁.p => D₂.w
          | D₁.q => D₂.v
          | D₁.r => D₂.w).2 ⊚
      G₁.toTgt)
    A₁.b =
  (G₂.toTgt ⊚
      (fun x ↦
          match x with
          | A₁.a => A₂.c
          | A₁.b => A₂.d,
          fun x ↦
          match x with
          | D₁.p => D₂.w
          | D₁.q => D₂.v
          | D₁.r => D₂.w).1)
    A₁.b rflAll goals completed! 🐙
}

def f₄ : G₁ ⟶ G₂ := {
  val := (
    fun -- maps arrows
      | A₁.a => A₂.d
      | A₁.b => A₂.c,
    fun -- maps dots
      | D₁.p => D₂.v
      | D₁.q => D₂.w
      | D₁.r => D₂.w
  )
  property := by⊢ (∀ x ∈ G₁.carrierA,
    (fun x ↦
            match x with
            | A₁.a => A₂.d
            | A₁.b => A₂.c,
            fun x ↦
            match x with
            | D₁.p => D₂.v
            | D₁.q => D₂.w
            | D₁.r => D₂.w).1
        x ∈
      G₂.carrierA) ∧
  (∀ x ∈ G₁.carrierD,
      (fun x ↦
              match x with
              | A₁.a => A₂.d
              | A₁.b => A₂.c,
              fun x ↦
              match x with
              | D₁.p => D₂.v
              | D₁.q => D₂.w
              | D₁.r => D₂.w).2
          x ∈
        G₂.carrierD) ∧
    (fun x ↦
              match x with
              | A₁.a => A₂.d
              | A₁.b => A₂.c,
              fun x ↦
              match x with
              | D₁.p => D₂.v
              | D₁.q => D₂.w
              | D₁.r => D₂.w).2 ⊚
          G₁.toSrc =
        G₂.toSrc ⊚
          (fun x ↦
              match x with
              | A₁.a => A₂.d
              | A₁.b => A₂.c,
              fun x ↦
              match x with
              | D₁.p => D₂.v
              | D₁.q => D₂.w
              | D₁.r => D₂.w).1 ∧
      (fun x ↦
              match x with
              | A₁.a => A₂.d
              | A₁.b => A₂.c,
              fun x ↦
              match x with
              | D₁.p => D₂.v
              | D₁.q => D₂.w
              | D₁.r => D₂.w).2 ⊚
          G₁.toTgt =
        G₂.toTgt ⊚
          (fun x ↦
              match x with
              | A₁.a => A₂.d
              | A₁.b => A₂.c,
              fun x ↦
              match x with
              | D₁.p => D₂.v
              | D₁.q => D₂.w
              | D₁.r => D₂.w).1
    split_andsrefine_1⊢ ∀ x ∈ G₁.carrierA,
  (fun x ↦
          match x with
          | A₁.a => A₂.d
          | A₁.b => A₂.c,
          fun x ↦
          match x with
          | D₁.p => D₂.v
          | D₁.q => D₂.w
          | D₁.r => D₂.w).1
      x ∈
    G₂.carrierArefine_2.refine_1⊢ ∀ x ∈ G₁.carrierD,
  (fun x ↦
          match x with
          | A₁.a => A₂.d
          | A₁.b => A₂.c,
          fun x ↦
          match x with
          | D₁.p => D₂.v
          | D₁.q => D₂.w
          | D₁.r => D₂.w).2
      x ∈
    G₂.carrierDrefine_2.refine_2.refine_1⊢ (fun x ↦
        match x with
        | A₁.a => A₂.d
        | A₁.b => A₂.c,
        fun x ↦
        match x with
        | D₁.p => D₂.v
        | D₁.q => D₂.w
        | D₁.r => D₂.w).2 ⊚
    G₁.toSrc =
  G₂.toSrc ⊚
    (fun x ↦
        match x with
        | A₁.a => A₂.d
        | A₁.b => A₂.c,
        fun x ↦
        match x with
        | D₁.p => D₂.v
        | D₁.q => D₂.w
        | D₁.r => D₂.w).1refine_2.refine_2.refine_2⊢ (fun x ↦
        match x with
        | A₁.a => A₂.d
        | A₁.b => A₂.c,
        fun x ↦
        match x with
        | D₁.p => D₂.v
        | D₁.q => D₂.w
        | D₁.r => D₂.w).2 ⊚
    G₁.toTgt =
  G₂.toTgt ⊚
    (fun x ↦
        match x with
        | A₁.a => A₂.d
        | A₁.b => A₂.c,
        fun x ↦
        match x with
        | D₁.p => D₂.v
        | D₁.q => D₂.w
        | D₁.r => D₂.w).1
    all_goals
      first | exact fun _ _ ↦ Set.mem_univ _refine_2.refine_2.refine_2⊢ (fun x ↦
        match x with
        | A₁.a => A₂.d
        | A₁.b => A₂.c,
        fun x ↦
        match x with
        | D₁.p => D₂.v
        | D₁.q => D₂.w
        | D₁.r => D₂.w).2 ⊚
    G₁.toTgt =
  G₂.toTgt ⊚
    (fun x ↦
        match x with
        | A₁.a => A₂.d
        | A₁.b => A₂.c,
        fun x ↦
        match x with
        | D₁.p => D₂.v
        | D₁.q => D₂.w
        | D₁.r => D₂.w).1
            | funext xrefine_2.refine_2.refine_2.hx:G₁.tA⊢ ((fun x ↦
          match x with
          | A₁.a => A₂.d
          | A₁.b => A₂.c,
          fun x ↦
          match x with
          | D₁.p => D₂.v
          | D₁.q => D₂.w
          | D₁.r => D₂.w).2 ⊚
      G₁.toTgt)
    x =
  (G₂.toTgt ⊚
      (fun x ↦
          match x with
          | A₁.a => A₂.d
          | A₁.b => A₂.c,
          fun x ↦
          match x with
          | D₁.p => D₂.v
          | D₁.q => D₂.w
          | D₁.r => D₂.w).1)
    x; cases xrefine_2.refine_2.refine_2.h.a⊢ ((fun x ↦
          match x with
          | A₁.a => A₂.d
          | A₁.b => A₂.c,
          fun x ↦
          match x with
          | D₁.p => D₂.v
          | D₁.q => D₂.w
          | D₁.r => D₂.w).2 ⊚
      G₁.toTgt)
    A₁.a =
  (G₂.toTgt ⊚
      (fun x ↦
          match x with
          | A₁.a => A₂.d
          | A₁.b => A₂.c,
          fun x ↦
          match x with
          | D₁.p => D₂.v
          | D₁.q => D₂.w
          | D₁.r => D₂.w).1)
    A₁.arefine_2.refine_2.refine_2.h.b⊢ ((fun x ↦
          match x with
          | A₁.a => A₂.d
          | A₁.b => A₂.c,
          fun x ↦
          match x with
          | D₁.p => D₂.v
          | D₁.q => D₂.w
          | D₁.r => D₂.w).2 ⊚
      G₁.toTgt)
    A₁.b =
  (G₂.toTgt ⊚
      (fun x ↦
          match x with
          | A₁.a => A₂.d
          | A₁.b => A₂.c,
          fun x ↦
          match x with
          | D₁.p => D₂.v
          | D₁.q => D₂.w
          | D₁.r => D₂.w).1)
    A₁.b <;>refine_2.refine_2.refine_2.h.a⊢ ((fun x ↦
          match x with
          | A₁.a => A₂.d
          | A₁.b => A₂.c,
          fun x ↦
          match x with
          | D₁.p => D₂.v
          | D₁.q => D₂.w
          | D₁.r => D₂.w).2 ⊚
      G₁.toTgt)
    A₁.a =
  (G₂.toTgt ⊚
      (fun x ↦
          match x with
          | A₁.a => A₂.d
          | A₁.b => A₂.c,
          fun x ↦
          match x with
          | D₁.p => D₂.v
          | D₁.q => D₂.w
          | D₁.r => D₂.w).1)
    A₁.arefine_2.refine_2.refine_2.h.b⊢ ((fun x ↦
          match x with
          | A₁.a => A₂.d
          | A₁.b => A₂.c,
          fun x ↦
          match x with
          | D₁.p => D₂.v
          | D₁.q => D₂.w
          | D₁.r => D₂.w).2 ⊚
      G₁.toTgt)
    A₁.b =
  (G₂.toTgt ⊚
      (fun x ↦
          match x with
          | A₁.a => A₂.d
          | A₁.b => A₂.c,
          fun x ↦
          match x with
          | D₁.p => D₂.v
          | D₁.q => D₂.w
          | D₁.r => D₂.w).1)
    A₁.b rflAll goals completed! 🐙
}

Problem 3 (p. 204)

Find an example of a set X and an endomap {X \xrightarrow{\alpha} X} with {\alpha^2 = \alpha^3} but {\alpha \neq \alpha^2}.

Solution: Problem 3

cf. the discussion of Katie's attempted solution on pp. 205–207.

inductive X
  | x₁ | x₂ | x₃

def α : End X
  | X.x₁ => X.x₂
  | X.x₂ => X.x₃
  | X.x₃ => X.x₃

example : α ^ 2 = α ^ 3 ∧ α ≠ α ^ 2 := by⊢ α ^ 2 = α ^ 3 ∧ α ≠ α ^ 2
  constructorleft⊢ α ^ 2 = α ^ 3right⊢ α ≠ α ^ 2
  ·left⊢ α ^ 2 = α ^ 3 funext xleft.hx:X⊢ (α ^ 2) x = (α ^ 3) x
    cases xleft.h.x₁⊢ (α ^ 2) X.x₁ = (α ^ 3) X.x₁left.h.x₂⊢ (α ^ 2) X.x₂ = (α ^ 3) X.x₂left.h.x₃⊢ (α ^ 2) X.x₃ = (α ^ 3) X.x₃ <;>left.h.x₁⊢ (α ^ 2) X.x₁ = (α ^ 3) X.x₁left.h.x₂⊢ (α ^ 2) X.x₂ = (α ^ 3) X.x₂left.h.x₃⊢ (α ^ 2) X.x₃ = (α ^ 3) X.x₃ rflAll goals completed! 🐙
  ·right⊢ α ≠ α ^ 2 by_contra hrighth:α = α ^ 2⊢ False
    have h_false : α X.x₁ = (α ^ 2) X.x₁ := congrFun h X.x₁righth:α = α ^ 2h_false:α X.x₁ = (α ^ 2) X.x₁ := congrFun h X.x₁⊢ False
    have hα : α X.x₁ = X.x₂ := rflrighth:α = α ^ 2h_false:α X.x₁ = (α ^ 2) X.x₁ := congrFun h X.x₁hα:α X.x₁ = X.x₂ := rfl⊢ False
    have hαα : (α ^ 2) X.x₁ = X.x₃ := rflrighth:α = α ^ 2h_false:α X.x₁ = (α ^ 2) X.x₁ := congrFun h X.x₁hα:α X.x₁ = X.x₂ := rflhαα:(α ^ 2) X.x₁ = X.x₃ := rfl⊢ False
    rw [hα, hαα] at h_falserighth:α = α ^ 2h_false:X.x₂ = X.x₃hα:α X.x₁ = X.x₂hαα:(α ^ 2) X.x₁ = X.x₃⊢ False
    contradictionAll goals completed! 🐙

In fact, since hα and hαα just establish definitional equalities, the contradiction tactic can take care of the last few steps automatically.

example : α ^ 2 = α ^ 3 ∧ α ≠ α ^ 2 := by⊢ α ^ 2 = α ^ 3 ∧ α ≠ α ^ 2
  constructorleft⊢ α ^ 2 = α ^ 3right⊢ α ≠ α ^ 2
  ·left⊢ α ^ 2 = α ^ 3 funext xleft.hx:X⊢ (α ^ 2) x = (α ^ 3) x
    cases xleft.h.x₁⊢ (α ^ 2) X.x₁ = (α ^ 3) X.x₁left.h.x₂⊢ (α ^ 2) X.x₂ = (α ^ 3) X.x₂left.h.x₃⊢ (α ^ 2) X.x₃ = (α ^ 3) X.x₃ <;>left.h.x₁⊢ (α ^ 2) X.x₁ = (α ^ 3) X.x₁left.h.x₂⊢ (α ^ 2) X.x₂ = (α ^ 3) X.x₂left.h.x₃⊢ (α ^ 2) X.x₃ = (α ^ 3) X.x₃ rflAll goals completed! 🐙
  ·right⊢ α ≠ α ^ 2 by_contra hrighth:α = α ^ 2⊢ False
    have h_false : α X.x₁ = (α ^ 2) X.x₁ := congrFun h X.x₁righth:α = α ^ 2h_false:α X.x₁ = (α ^ 2) X.x₁ := congrFun h X.x₁⊢ False
    -- have hα : α X.x₁ = X.x₂ := rfl
    -- have hαα : (α ^ 2) X.x₁ = X.x₃ := rfl
    -- rw [hα, hαα] at h_false
    contradictionAll goals completed! 🐙