namespace latin:/❚

fixmeta ?SFOLEQND❚

theory Option =
  option: tp ⟶ tp ❘ # 1 ? prec 100 ❘ // unfortunately the notation ? does not work in binders, so use 'option A' there❙
  some: {A: tp} tm A ⟶ tm A? ❘ # some 2❙
  none: {A: tp} tm A? ❘ # none %I1 ❙

  defined_and_equal_to: {A: tp} tm A? ⟶ tm A ⟶ prop
    ❘ = [A, optionValue, value] optionValue ≐ some value
    ❘ # 2 ≡ 3 prec 20 ❙

  defined: {A: tp} tm A? ⟶ prop
    ❘ = [A, optionValue] ∃[v: tm A] optionValue ≡ v
    ❘ # 2 ↓ prec 20 ❘ // we need higher precedence than ∧ (which is 10 currently) ❙

  if_defined_then_equal_to: {A: tp} tm A? ⟶ tm A ⟶ prop
    ❘ = [A, optionValue, value] optionValue ≐ none ∨ optionValue ≡ value
    ❘ # ifDefEq 2 3
    ❙

  both_defined_and_equal: {A: tp} tm A? ⟶ tm A? ⟶ prop
    ❘ = [A, optionValue1, optionValue2] optionValue1↓ ∧ optionValue2↓ ∧ optionValue1 ≐ optionValue2
    ❘ # bothDefEq 2 3
   ❙

  equality_ax: {A: tp} ⊦ ∀[optionValue1: tm (option A)] ∀[optionValue2: tm (option A)]
      optionValue1 ≐ optionValue2 ⇔ (optionValue1 ≐ none ∧ optionValue2 ≐ none) ∨ (∃[v: tm A] optionValue1 ≡ v ∧ optionValue2 ≡ v) ❙

  map: {A, B} tm A? ⟶ (tm A ⟶ tm B) ⟶ tm B? ❘ # map 3 4 prec 25❙
  map_ax1: {A, B, f: tm A ⟶ tm B, a: tm A} ⊦ map (some a) f ≡ f a ❙
  map_ax2: {A, B, f: tm A ⟶ tm B} ⊦ (map none f) ≐ none ❙

  flatMap: {A, B} tm A? ⟶ (tm A ⟶ tm (option B)) ⟶ tm B? ❘ # flatMap 3 4 prec 25 ❙
❚

theory ObjectLessComposition =
  include ?Option ❙
  mor: tp ❙
  Mor = tm mor ❙
  OptionMor = tm mor? ❘ # Mor? ❙
  composition: Mor ⟶ Mor ⟶ Mor? ❘ # 2 ∘ 1 prec 200 ❙

  // The question mark is on the optional side ❙
  opt_composition: Mor? ⟶ Mor ⟶ Mor?
    ❘ = [α, β] flatMap α ([z] z ∘ β)
    ❘ # 2 ∘? 1
  ❙

  // The question mark is on the optional side ❙
  composition_opt: Mor ⟶ Mor? ⟶ Mor?
    ❘ = [α, β] flatMap β ([z] α ∘ z)
    ❘ # 2 ?∘ 1
  ❙
❚

// Object-less category theory according to
    https://arxiv.org/pdf/1602.01759.pdf ❚
theory ObjectLessCategory =
  include ?Option ❙
  include ?ObjectLessComposition ❙

  associativity: {α: Mor, β: Mor, γ: Mor}
    ⊦ (α ∘ β)↓ ∧ (β ∘ γ)↓ ⇒ (α ∘? (β ∘ γ))↓ ∧ ((α ∘ β) ?∘ γ)↓ ∧ (α ∘? (β ∘ γ)) ≐ ((α ∘ β) ?∘ γ)
  ❙
  existence_of_subcompositions1: {α: Mor, β: Mor, γ: Mor} ⊦ (α ∘? (β ∘ γ))↓ ⇒ (α ∘ β)↓ ❙
  existence_of_subcompositions2: {α: Mor, β: Mor, γ: Mor} ⊦ ((α ∘ β) ?∘ γ)↓ ⇒ (β ∘ γ)↓ ❙

  leftIdentity: {m: Mor} Mor ❘ # ' 1 prec 20 ❙
  leftIdentityAlternativeNotation = leftIdentity ❘ # dom 1 prec 20 ❙
  rightIdentity: {m: Mor} Mor ❘ # 1 '' prec 20 ❘ // notation ' 1 doesn't work with MMT's notation parser somehow ❙
  rightIdentityAlternativeNotation = rightIdentity ❘ # cod 1 prec 20 ❙

  ax_leftIdentityComposable: {α: Mor} ⊦ (α ∘ 'α)↓ ❙
  ax_rightIdentityComposable: {α: Mor} ⊦ (α'' ∘ α)↓ ❙

  ax_leftIdentityNeutral : {α: Mor, β: Mor} ⊦ (ifDefEq  (β ∘ 'α) β) ∧ (ifDefEq  (('α) ∘ β) β)❙
  ax_rightIdentityNeutral: {α: Mor, β: Mor} ⊦ (ifDefEq (β ∘ (α'')) β) ∧ (ifDefEq (α'' ∘ β) β)❙
  // {β: Mor} ⊦ (β ∘ ⟜β)↓ ⇒ (β ∘ ⟜β) ≡ β ❙

  is_identity: Mor ⟶ prop ❘ = [α] ∃[β] α ≐ dom β ∨ α ≐ cod β ❙
  // Hom set between (dom α) and (cod β)
  hom: {α: Mor, β: Mor} tp ❙
❚

// https://ncatlab.org/nlab/show/category#OneCollectionOfMorphisms ❚
theory CategoryWithOneCollection =
  include ?Option ❙
  include ?ObjectLessComposition ❙

  obj: tp ❙
  dom: Mor ⟶ tm obj ❙
  cod: Mor ⟶ tm obj ❙

  id: tm obj ⟶ Mor ❙

  ax_dom_preserved: {f, g} ⊦ map (g ∘ f) dom ≡ dom f ❙
  ax_cod_preserved: {f, g} ⊦ map (g ∘ f) cod ≡ cod g ❙

  ax_identities_dom_cod: {a} ⊦ dom (id a) ≐ a ∧ cod (id a) ≐ a ❙

  ax_comp_defined: {f, g} ⊦ cod f ≐ dom g ⇒ (g ∘ f)↓ ❙

  ax_associativity: {f, g, h} ⊦ (dom g ≐ cod f ∧ dom h ≐ cod g) ⇒ bothDefEq ((h ∘ g) ?∘ f) (h ∘? (g ∘ f)) ❙
❚

// https://ncatlab.org/nlab/show/category#AFamilyOfCollectionsOfMorphisms ❚
theory CategoryWithHomSetsSFOL =
  obj: tp ❙

  hom: {dom: tm obj, cod: tm obj} tp ❙
  Hom: tm obj ⟶ tm obj ⟶ type ❘ = [a, b] tm (hom a b) ❙
  id: {a} Hom a a ❙
  compositionABC: {x, y, z} Hom x y ⟶ Hom y z ⟶ Hom x z ❘ # 5 ∘ 4 prec 200 ❙

  associativity: {a, b, c, d, f: Hom a b, g: Hom b c, h: Hom c d} ⊦ h ∘ (g ∘ f) ≐ (h ∘ g) ∘ f❙

  ax_identityLeftNeutral : {a, b, f: Hom a b} ⊦ (id b) ∘ f ≐ f ❙
  ax_identityRightNeutral: {a, b, f: Hom a b} ⊦ f ∘ (id a) ≐ f ❙
❚

// view blah: ObjectLessCategory -> CategoryWithHomSetsSFOL =
  include ?Option ❙
  // mor = ? ❙
❚