module NatAlgebra where

open import Preliminaries

record NatAlg (X : Set) : Set where
  field
    S : X → X
    Z : X

module _ {X : Set} (X-alg : NatAlg X) where
  private module X = NatAlg X-alg

  record DNatAlg (Y : X → Set) : Set where
    field
      S : {x : X} → Y x → Y (X.S x)
      Z : Y X.Z

  module _ {Y : X → Set} (Y-alg : DNatAlg Y) where
    private module Y = DNatAlg Y-alg

    record NSec : Set where
      field
        on-C : (x : X) → Y x
        on-S : (x : X) → on-C (X.S x) ≡ Y.S (on-C x)
        on-Z : on-C X.Z ≡ Y.Z

    Σ-alg : NatAlg (Σ X Y)
    Σ-alg .NatAlg.S x .fst = X.S (x .fst)
    Σ-alg .NatAlg.S x .snd = Y.S (x .snd)
    Σ-alg .NatAlg.Z = (X.Z , Y.Z)