example.shari

// the characteristic of the diagonal mono δ : α → α × α
constant eq : α → α → Prop

infix = : 50 := eq

// This is definitionally equal to any term of the Unit type by the eta rule.
constant star : Unit

/-
This introduces a constant `top` and:
axiom top_spec : top = (star = star)
-/
def top : Prop := star = star

nofix ⊤ := top

def and (φ ψ : Prop) : Prop := ⟨φ, ψ⟩ = ⟨⊤, ⊤⟩

infixr ∧ : 35 := and

/-
Recall [x = x ∧ y] means [x ≤ y] in the preorder canonically induced by a lattice structure.
-/
def imp (φ ψ : Prop) : Prop := φ = φ ∧ ψ

infixr → : 25 := imp

def forall (P : α → Prop) : Prop := P = (λ x, ⊤)

def bot : Prop := ∀ ξ, ξ

nofix ⊥ := bot

def or (φ ψ : Prop) : Prop := ∀ ξ, (φ → ξ) ∧ (ψ → ξ) → ξ

infixr ∨ : 30 := or

def exists (P : α → Prop) : Prop := ∀ ξ, (∀ x, P x → ξ) → ξ

def not (φ : Prop) : Prop := φ → ⊥

prefix ¬ : 40 := not

def iff (φ ψ : Prop) : Prop := (φ → ψ) ∧ (ψ → φ)

infix ↔ : 20 := iff

def uexists (P : α → Prop) : Prop := ∃ x, P x ∧ (∀ y, P y → x = y)

/-
# Primitive rules

We assume contexts are sets.

h : [Γ ▸ Φ ⊢ φ]
-------------------------
h : [Γ, x : τ ▸ Φ, ψ ⊢ φ]

h : [Γ ▸ Φ ⊢ φ]
------------------
h : [Γ ▸ Φ, ψ ⊢ φ]

h : [Γ ▸ Φ ⊢ φ]
------------------------ (φ ≡ ψ)
change ψ h : [Γ ▸ Φ ⊢ ψ]

----------------------
assume φ : [Γ ▸ φ ⊢ φ]

--------------------------
eq_intro t : [Γ ▸ ⊢ t = t]

h₁ : [Γ ▸ Φ ⊢ t = s]  h₂ : [Γ ▸ Ψ ⊢ C t]
---------------------------------------- [indiscernibility of identicals]
eq_elim C h₁ h₂ : [Γ ∪ Δ ▸ Φ ∪ Ψ ⊢ C s]

h₁ : [Γ ▸ Φ, φ ⊢ ψ]  h₂ : [Γ ▸ Ψ, ψ ⊢ φ]
---------------------------------------- [(external) propositional extensionality]
prop_ext h₁ h₂ : [Γ ∪ Δ ▸ Φ ∪ Ψ ⊢ φ = ψ]

h : [Γ, x : τ ▸ Φ ⊢ t₁ = t₂]
--------------------------------------------- (x ∉ FV Φ) [(external) function extensionality]
fun_ext x h : [Γ ▸ Φ ⊢ (λ x, t₁) = (λ x, t₂)]

# Metatheorem

h : [Γ, x : τ ▸ Φ ⊢ φ]
-----------------------------------
subst x t h : [Γ ▸ [t/x]Φ ⊢ [t/x]φ]

# Derived rules

h : [Γ ▸ Φ, φ ⊢ ψ]
-----------------------------
imp_intro h : [Γ ▸ Φ ⊢ φ → ψ]

h₁ : [Γ ▸ Φ ⊢ φ → ψ]  h₂ : [Δ ▸ Ψ ⊢ φ]
---------------------------------------
imp_elim h₁ h₂ : [Γ ∪ Δ ▸ Φ ∪ Ψ ⊢ ψ]

h : [Γ, x : τ ▸ Φ ⊢ φ]
----------------------------------- (x ∉ FV Φ)
forall_intro x h : [Γ ▸ Φ ⊢ ∀ x, φ]

h : [Γ ▸ Φ ⊢ ∀ x, φ]
----------------------------------
forall_elim t h : [Γ ▸ Φ ⊢ [t/x]φ]
-/

/-
meta constant change : Term → Fact → Fact
meta constant assume : Term → Fact
meta constant eq_intro : Term → Fact
meta constant eq_elim : Term → Fact → Fact → Fact
meta constant prop_ext : Fact → Fact → Fact
meta constant fun_ext : Term → Fact → Fact

meta constant subst : Term → Term → Fact → Fact

meta constant imp_intro : Fact → Fact
meta constant imp_elim : Fact → Fact → Fact
meta constant forall_intro : Term → Fact → Fact
meta constant forall_elim : Term → Fact
-/

/-
Proof is done by constructing in the meta stage an object of the Fact type whose judgement has the form of [▸ ⊢ φ] when the target formula is φ.

After the symbol `:=` a meta expression constructing the proof object (= Fact) follows.

This `prop` block introduces a new meta object `eq_refl : Fact`.
-/
prop eq_refl : ∀ t, t = t :=
forall_intro `t (eq_intro `t)

prop eq_elim : ∀ t s C, t = s → C t → C s :=
forall_intro `t (forall_intro `s (forall_intro `C (imp_intro (imp_intro (eq_elim `C (assume `(t = s)) (assume `(C t)))))))

/-
`{ .. }` syntax is a construct in the meta stage for tactical reasoning.
-/
prop eq_symm : ∀ t s, t = s → s = t := {
  fix t s,
  assume t = s,
  have t = s → t = t → s = t ..(1) := {
    apply eq_elim where C := (λ x, x = t),
  },
  show s = t := {
    apply (1),
    assumption,
    apply eq_refl
  },
}

prop eq_trans : ∀ t s u, t = s → s = u → t = u := {
  fix t s u,
  assume t = s,
  assume s = u,
  apply eq_elim where C := (λ x, t = x),
  assumption,
  assumption,
}

prop prod_eq : ∀ t₁ t₂ s₁ s₂, t₁ = t₂ → s₁ = s₂ → ⟨t₁, s₁⟩ = ⟨t₂, s₂⟩ := {
  fix t₁ t₂ s₁ s₂,
  assume t₁ = t₂,
  assume s₁ = s₂,
  have ⟨t₁, s₁⟩ = ⟨t₂, s₁⟩, from eq_elim (λ x, ⟨t₁, s₁⟩ = ⟨x, s₁⟩) (assume (t₁ = t₂)) (eq_intro ⟨t₁, s₁⟩),
  have ⟨t₂, s₁⟩ = ⟨t₂, s₂⟩, from eq_elim (λ x, ⟨t₂, s₁⟩ = ⟨t₂, x⟩) (assume (s₁ = s₂)) (eq_intro ⟨t₂, s₁⟩),
  show ⟨t₁, s₁⟩ = ⟨t₂, s₂⟩, {
    apply eq_trans,
    assumption ⟪⟨t₁, s₁⟩ = ⟨t₂, s₁⟩⟫,
    assumption,
  }
}

class Inhabited α :=
(prop inhabited : ∃ (x : α), ⊤)

instance [Inhabited β] : Inhabited (α → β) :=
(prop inhabited := {
  show ∃ (x : α → β), ⊤,
  obtain b from ⟪∃ (x : β), ⊤⟫,
  construction (λ _, b),
  trivial,
})

instance [Inhabited α] [Inhabited β] : Inhabited (α × β) :=
(prop inhabited := {
  show ∃ (x : α × β), ⊤,
  obtain (a : α) from ⟪∃ (x : α), ⊤⟫,
  obtain (b : β) from ⟪∃ (x : β), ⊤⟫,
  construction ⟨a, b⟩,
  trivial,
})

instance : Inhabited Unit :=
(prop inhabited := {
  construction star,
  trivial,
})

-- type abbreviation (does not introduce a new opaque type)
type Set α := α → Prop

def mem (x : α) (s : Set α) := s x

infix ∈ : 50 := mem

def inhabited (s : Set α) : Prop := ∃ a, a ∈ s

/-
Our standard model is ε-topos.
-/
const choice [Inhabited α] : (α → Prop) → α

axiom choice_spec [Inhabited α] : ∀ (P : α → Prop), inhabited P → P (choice P)

prop ac [Inhabited β] : ∀ (P : α → β → Prop), (∀ x, ∃ y, P x y) → ∃ f, ∀ x, P x (f x) := {
  fix P,
  assume ∀ x, ∃ y, P x y,
  construction λ x, choice (P x),
  show ∀ x, P x (choice (P x)),
  fix x,
  show P x (P x (choice (P x))),
  have inhabited (P x) → (P x (choice (P x))) := by apply choice_spec,
  have inhabited (P x) := {
    show ∃ y, y ∈ P x,
    show ∃ y, P x y,
    apply ⟪∀ x, ∃ y, P x y⟫,
  },
  apply inhabited (P x) → (P x (choice (P x))),
  assumption,
}

prop prop_ext : ∀ φ₁ φ₂, (φ₁ ↔ φ₂) → (φ₁ = φ₂) := by sorry
prop fun_ext : ∀ f₁ f₂, (∀ x, f₁ x = f₂ x) → (f₁ = f₂) := by sorry

def fst (p : α × β) : α := p.0
def snd (p : α × β) : β := p.1
def pair (a : α) (b : β) := ⟨a, b⟩

/-
⊢ φ : τ → Prop
⊢ rep : subtype φ → τ
rep_inj : [⊢ ∀ a₁ a₂, rep a₁ = rep a₂ → a₁ = a₂]
rep_im : [⊢ ∀ x, φ x → ∃ a, rep a = x]
-/

class Subtype β α :=
(pred : β → Prop)
(rep : α → β)
(prop inj : ∀ a₁ a₂, rep a₁ = rep a₂ → a₁ = a₂)
(prop im : ∀ x, pred x → ∃ a, rep a = x)

/-
This automatically defines a class instance [Subtype Unit Void].
-/
subtype Void := { x : Set Unit | ⊥ }

class Abs β α [Subtype β α] [Inhabited α] :=
(abs : β → α := λ b, choice (λ a, rep a = b))

def inv_image (f : α → β) (V : Set β) : Set α := λ a, V (f a)
def counit (a : α) : Set (Set α) := λ f, f a

/-
See [SGL, Ch IV, Sec 5]
-/
subtype Sum α β := { p : Set (Set α × Set β) | counit p = inv_image (λ x, ⟨ inv_image counit (inv_image (inv_image (λ p, p.0)) x), inv_image counit (inv_image (inv_image (λ p, p.1)) x) ⟩) p }