nonsense.v

(* mostly cribbing from https://golem.ph.utexas.edu/category/2021/02/native_type_theory.html and nlab *)
(*
A topos has has finite limits, is cartesian closed, and has a subobject classifier. I guess ? *)

(* FIXME cleanup notation levels *)
Inductive object : Set :=
| terminal
| tuple (_ : object) (_: object)
| fn (_ : object) (_: object)

| Z

| typ

| Ω .

Notation "*" := terminal.
Infix "×" := tuple (at level 80).
Infix "⇒" := fn (at level 90).

Section topos.

(* I know I should use type classes or modules but I couldn't bother *)
Variable hom : object -> object -> Set.

Variable id : forall a, hom a a.
Variable compose : forall a b c, hom b c -> hom a b -> hom a c.

(* Cartesian category stuff but in a higher order style, not related to the paper *)
Variable bang : forall a, hom a *.

Variable kappa : forall a b c, (hom * a -> hom b c) -> hom (a × b) c.
Variable lift: forall a b c, hom (a × b) c -> hom * a -> hom b c.

Variable zeta : forall a b c, (hom * a -> hom b c) -> hom b (a ⇒ c).
Variable pass : forall a b c, hom b (a ⇒ c) -> hom * a -> hom b c.

  (* I don't get subobject classifier stuff *)
Variable true : hom * Ω.
Variable subset : forall u x, hom u x -> hom x Ω.

Infix "∘" := (compose _ _ _) (at level 50).

Notation "'ζ' x . e" := (zeta _ _ _ (fun x => e)) (x ident, at level 100).
Notation "'κ' x . e" := (kappa _ _ _ (fun x => e)) (x ident, at level 100).

(* A slice object I think ? 
  mostly working from https://ncatlab.org/nlab/show/over+category
  
  https://golem.ph.utexas.edu/category/2021/02/native_type_theory.html
  *)
Inductive slice := | mkslice a (_ : hom a Ω).

Notation "f ∈ a" := (mkslice a f) (at level 90).

Definition slice_hom (x : slice) (y : slice) :=
match x with
| mkslice a f =>
  match y with
    | mkslice b f' =>
      (* FIXME make setoid *)
      { g : hom a b | (f' ∘ g) = f }
  end
end.

Infix "⊢" := slice_hom (at level 100).

Definition map {a b x} (f : hom a b) : (x ∘ f) ∈ a ⊢ x ∈ b.
eexists f.
reflexivity.
Defined.

(* I think I fell off the right track somewhere but I'm not really sure *)

Variable num : nat -> hom Z Ω.
Variable banger : hom * Ω.
Variable succ : forall a, hom Z a -> hom Z a.

(* Not sure about terminals *)
Variable constant_rule : forall n, (banger ∈ *) ⊢ (num n ∈ Z).
Variable succ_rule : forall n, (n ∈ Z) ⊢ (succ _ n ∈ Z).

Variable is_unit : hom typ Ω.
Variable is_prod : forall a, hom (typ × typ) a -> hom typ a.

Variable unit_rule : forall a x, x ∈ a ⊢ is_unit ∈ typ.
Variable prod_rule : forall x, x ∈ (typ × typ) ⊢ is_prod _ x ∈ typ.