simple.agda

module simple where

open import Agda.Builtin.Size public

_∘_ : ∀ {i j k} {A : Set i} {B : A → Set j} {C : ∀ {x} → B x → Set k}
      (f : ∀ {x} (y : B x) → C y) (g : (x : A) → B x) (x : A) → C (g x)
f ∘ g = λ x → f (g x)

data _≡_ {i} {X : Set i} (x : X) : {Y : Set i} → Y → Set where
  refl : x ≡ x

trans : ∀ {i} {A B C : Set i} {x : A} {y : B} {z : C} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl

sym : ∀ {i} {A : Set i} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

coerce : ∀ {i} {A B : Set i} → A ≡ B → A → B
coerce refl x = x

coerce' : ∀ {i} {A B : Set i} → A ≡ B → B → A
coerce' e = coerce (sym e)

coerce'' : ∀ {i j} {A B : Set i} (C : A → Set j) (e : B ≡ A) (f : (a : A) → C a) (b : B) → C (coerce e b)
coerce'' C e f = f ∘ coerce e

coerce-coh : ∀ {i} {A B : Set i} (e : A ≡ B) {x : A} → coerce e x ≡ x
coerce-coh refl = refl

subst : ∀ {i j} {A : Set i} (P : A → Set j) {x y} → x ≡ y → P x → P y
subst P refl p = p

cong : ∀ {i j} {A : Set i} {B : A → Set j} (f : (a : A) → B a) {x y} → x ≡ y → f x ≡ f y
cong f refl = refl

transp : ∀ {i j} {A B : Set i} {C : Set j} (f : A → C) (g : B → C) (x : B ≡ A) (y : ∀ a → f a ≡ g (coerce (sym x) a)) (b : B) → f (coerce x b) ≡ g b
transp f g x y b =
  trans (y (coerce x b)) (cong g (trans (coerce-coh (sym x)) (coerce-coh x)))



record Σ (X : Set) (Y : X → Set) : Set where
  constructor _,_
  field
    π₀ : X
    π₁ : Y π₀
open Σ public

Σ-ext : ∀ {X Y} {p₀ p₁ : Σ X Y} → π₀ p₀ ≡ π₀ p₁ → π₁ p₀ ≡ π₁ p₁ → p₀ ≡ p₁
Σ-ext refl refl = refl

postulate
  Π-ext : {X : Set} {Y : X → Set} {f₀ f₁ : (x : X) → Y x} → (∀ x → f₀ x ≡ f₁ x) → f₀ ≡ f₁

_⇒_ : ∀ {I : Set} (X Y : I → Set) → Set
X ⇒ Y = ∀ i → X i → Y i

data inv {X Y : Set} (f : X → Y) : Y → Set where
  ok : (x : X) → inv f (f x)

module cont where
  -- On encode un endofoncteur (I → Set) → (I → Set)
  -- Moralement l'explication c'est que n'importe quel foncteur polynomial peut
  -- s'exprimer comme le choix d'une "forme" (argument constants),
  -- puis pour chaque forme un certain nombre de "positions" (utilisation de
  -- l'argument). Comme ici on est en indexé, pour chaque position il faut aussi
  -- donner l'indice qu'on veut.
  record cont (I : Set) : Set₁ where
    field
      shape : I → Set
      pos : ∀ i → shape i → Set
      next : ∀ i s → pos i s → I
  open cont public

  data ⟦_⟧c {I} (C : cont I) (X : I → Set) (i : I) : Set where
    _,_ : (s : shape C i) (f : (p : pos C i s) → X (next C i s p)) → ⟦ C ⟧c X i

  fmap : ∀ {I} (C : cont I) (X Y : I → Set) (F : X ⇒ Y) → ⟦ C ⟧c X ⇒ ⟦ C ⟧c Y
  fmap C X Y F i (s , f) = s , λ p → F _ (f p)

  data μ {I} (C : cont I) (i : I) : Set where
    [_] : ⟦ C ⟧c (μ C) i → μ C i

  fold : ∀ {I} (C : cont I) (X : I → Set) (alg : ⟦ C ⟧c X ⇒ X) → μ C ⇒ X
  fold C X alg i [ s , f ] = alg i (s , λ p → fold C X alg (next C i s p) (f p))

  record ornament {I J : Set} (re : J → I) (C : cont I) (D : cont J) : Set₁ where
    field
      o-shape : ∀ j → shape D j → shape C (re j)
      o-pos : ∀ j s → pos C (re j) (o-shape j s) ≡ pos D j s
      o-next : ∀ j s p → re (next D j s (coerce (o-pos j s) p)) ≡ next C _ _ p
  open ornament public

  nmap : ∀ {I J} {re : J → I} {C D} (O : ornament re C D) (X : I → Set) → ⟦ D ⟧c (X ∘ re) ⇒ (⟦ C ⟧c X ∘ re)
  nmap O X j (s , f) = o-shape O j s , λ p → subst X (o-next O j s p) (f (coerce (o-pos O j s) p))

  nnat : ∀ {I J} {re : J → I} {C D} (O : ornament re C D) (X Y : I → Set) (F : X ⇒ Y) j x →
    fmap C X Y F (re j) (nmap O X j x) ≡ nmap O Y j (fmap D (X ∘ re) (Y ∘ re) (F ∘ re) j x)
  nnat O X Y F j (s , f) = {! Σ-ext  !} -- flemme, faut du tooling

  -- yay!
  {-forget : ∀ {I J} {re : J → I} {C D} (O : ornament re C D) → μ D ⇒ (μ C ∘ re)
  forget O = fold _ _ λ j x → [ nmap O _ j x ]

  alg-cont : ∀ {I} (C : cont I) {X} (alg : ⟦ C ⟧c X ⇒ X) → cont (Σ I X)
  shape (alg-cont C alg) (i , x) = inv (alg i) x
  pos (alg-cont C alg) (i , _) (ok (s , f)) = {!   !}
  next (alg-cont C alg) = {!   !}-}

module desc where

  data desc (I : Set) : Set₁ where
    `var : (i : I) → desc I
    `kon : (S : Set) → desc I
    `pi : (S : Set) (T : S → desc I) → desc I
    `sg : (S : Set) (T : S → desc I) → desc I

  ⟦_⟧ : ∀ {I} (D : desc I) (X : I → Set) → Set
  ⟦ `var i  ⟧ X = X i
  ⟦ `kon S  ⟧ X = S
  ⟦ `pi S T ⟧ X = (s : S) → ⟦ T s ⟧ X
  ⟦ `sg S T ⟧ X = Σ S λ s → ⟦ T s ⟧ X

  data μ {I : Set} (D : I → desc I) {s : Size} (i : I) : Set where
    inj : ∀ {t : Size< s} → ⟦ D i ⟧ (μ D {t}) → μ D {s} i

  all : ∀ {I} (D : desc I) (X : I → Set) (P : ∀ {i} → X i → Set) (x : ⟦ D ⟧ X) → Set
  all (`var i)  X P x = P x
  all (`kon S)  X P x = S
  all (`pi S T) X P x = (s : S) → all (T s) X P (x s)
  all (`sg S T) X P x = all (T (π₀ x)) X P (π₁ x)

  every : ∀ {I} (D : desc I) (X : I → Set) (P : ∀ {i} → X i → Set) →
    (p : ∀ {i} (x : X i) → P x) → (x : ⟦ D ⟧ X) → all D X P x
  every (`var i)  X P p x = p x
  every (`kon S)  X P p x = x
  every (`pi S T) X P p x = λ s → every (T s) X P p (x s)
  every (`sg S T) X P p x = every (T (π₀ x)) X P p (π₁ x)

  induction : ∀ {I} (D : I → desc I) (P : ∀ {s i} → μ D {s} i → Set)
    (h : ∀ {s} {t : Size< s} {i} (x : ⟦ D i ⟧ (μ D {t})) → all (D i) (μ D {t}) P x → P {s} (inj x))
    {s} {i} (x : μ D {s} i) → P x
  induction D P h (inj x) = h x (every (D _) (μ D) P (induction D P h) x)