{-# OPTIONS --cubical --safe #-}

module Algebra.Construct.Free.Semilattice.Eliminators where

open import Algebra.Construct.Free.Semilattice.Definition
open import Prelude
open import Algebra

record _β‡˜_ {a p} (A : Type a) (P : 𝒦 A β†’ Type p) : Type (a β„“βŠ” p) where
  no-eta-equality
  constructor elim
  field
    ⟦_⟧-set : βˆ€ {xs} β†’ isSet (P xs)
    ⟦_⟧[] : P []
    ⟦_⟧_∷_⟨_⟩ : βˆ€ x xs β†’ P xs β†’ P (x ∷ xs)
  private z = ⟦_⟧[]; f = ⟦_⟧_∷_⟨_⟩
  field
    ⟦_⟧-com : βˆ€ x y xs pxs β†’
      f x (y ∷ xs) (f y xs pxs) ≑[ i ≔ P (com x y xs i) ]≑
      f y (x ∷ xs) (f x xs pxs)
    ⟦_⟧-dup : βˆ€ x xs pxs β†’
      f x (x ∷ xs) (f x xs pxs) ≑[ i ≔ P (dup x xs i) ]≑
      f x xs pxs
  ⟦_βŸ§β‡“ : βˆ€ xs β†’ P xs
  ⟦ [] βŸ§β‡“ = z
  ⟦ x ∷ xs βŸ§β‡“ = f x xs ⟦ xs βŸ§β‡“
  ⟦ com x y xs i βŸ§β‡“ = ⟦_⟧-com x y xs ⟦ xs βŸ§β‡“  i
  ⟦ dup x xs i βŸ§β‡“ = ⟦_⟧-dup x xs ⟦ xs βŸ§β‡“ i
  ⟦ trunc xs ys x y i j βŸ§β‡“ =
      isOfHLevel→isOfHLevelDep 2
        (Ξ» xs β†’ ⟦_⟧-set {xs})
        ⟦ xs βŸ§β‡“ ⟦ ys βŸ§β‡“
        (cong ⟦_βŸ§β‡“ x) (cong ⟦_βŸ§β‡“ y)
        (trunc xs ys x y)
        i j
  {-# INLINE ⟦_βŸ§β‡“ #-}
open _β‡˜_ public

infixr 0 β‡˜-syntax
β‡˜-syntax = _β‡˜_
syntax β‡˜-syntax A (Ξ» xs β†’ Pxs) = xs βˆˆπ’¦ A β‡’ Pxs

record _⇲_ {a p} (A : Type a) (P : 𝒦 A  β†’ Type p) : Type (a β„“βŠ” p) where
  no-eta-equality
  constructor elim-prop
  field
    βˆ₯_βˆ₯-prop : βˆ€ {xs} β†’ isProp (P xs)
    βˆ₯_βˆ₯[] : P []
    βˆ₯_βˆ₯_∷_⟨_⟩ : βˆ€ x xs β†’ P xs β†’ P (x ∷ xs)
  private z = βˆ₯_βˆ₯[]; f = βˆ₯_βˆ₯_∷_⟨_⟩
  βˆ₯_βˆ₯⇑ = elim
          (Ξ» {xs} β†’ isPropβ†’isSet (βˆ₯_βˆ₯-prop {xs}))
          z f
          (Ξ» x y xs pxs β†’ toPathP (βˆ₯_βˆ₯-prop (transp (Ξ» i β†’ P (com x y xs i)) i0 (f x (y ∷ xs) (f y xs pxs))) (f y (x ∷ xs) (f x xs pxs))))
          (Ξ» x xs pxs β†’ toPathP (βˆ₯_βˆ₯-prop (transp (Ξ» i β†’ P (dup x xs i)) i0 (f x (x ∷ xs) (f x xs pxs))) (f x xs pxs) ))
  βˆ₯_βˆ₯⇓ = ⟦ βˆ₯_βˆ₯⇑ βŸ§β‡“
  {-# INLINE βˆ₯_βˆ₯⇑ #-}
  {-# INLINE βˆ₯_βˆ₯⇓ #-}

open _⇲_ public
elim-prop-syntax : βˆ€ {a p} β†’ (A : Type a) β†’ (𝒦 A β†’ Type p) β†’ Type (a β„“βŠ” p)
elim-prop-syntax = _⇲_

syntax elim-prop-syntax A (Ξ» xs β†’ Pxs) = xs βˆˆπ’¦ A β‡’βˆ₯ Pxs βˆ₯

record _β†˜βˆ₯_βˆ₯ {a p} (A : Type a) (P : 𝒦 A β†’ Type p) : Type (a β„“βŠ” p) where
  no-eta-equality
  constructor elim-to-prop
  field
    ∣_∣[] : P []
    ∣_∣_∷_⟨_⟩ : βˆ€ x xs β†’ P xs β†’ P (x ∷ xs)
  private z = ∣_∣[]; f = ∣_∣_∷_⟨_⟩
  open import HITs.PropositionalTruncation.Sugar
  open import HITs.PropositionalTruncation

  ∣_βˆ£β‡‘ : xs βˆˆπ’¦ A β‡’βˆ₯ βˆ₯ P xs βˆ₯ βˆ₯
  ∣_βˆ£β‡‘ = elim-prop squash ∣ z ∣ Ξ» x xs ∣Pxs∣ β†’ f x xs βˆ₯$βˆ₯ ∣Pxs∣
  ∣_βˆ£β‡“ = βˆ₯ ∣_βˆ£β‡‘ βˆ₯⇓


open _β†˜βˆ₯_βˆ₯ public
elim-to-prop-syntax : βˆ€ {a p} β†’ (A : Type a) β†’ (𝒦 A β†’ Type p) β†’ Type (a β„“βŠ” p)
elim-to-prop-syntax = _β†˜βˆ₯_βˆ₯

syntax elim-to-prop-syntax A (Ξ» xs β†’ Pxs) = xs βˆˆπ’¦ A β‡’βˆ£ Pxs ∣

infixr 0 _β†˜_
record _β†˜_ {a b} (A : Type a) (B : Type b) : Type (a β„“βŠ” b) where
  no-eta-equality
  constructor rec
  field
    [_]-set  : isSet B
    [_]_∷_   : A β†’ B β†’ B
    [_][]    : B
  private f = [_]_∷_; z = [_][]
  field
    [_]-dup  : βˆ€ x xs β†’ f x (f x xs) ≑ f x xs
    [_]-com : βˆ€ x y xs β†’ f x (f y xs) ≑ f y (f x xs)
  [_]↑ = elim
            [_]-set
            z
            (Ξ» x _ xs β†’ f x xs)
            (Ξ» x y xs β†’ [_]-com x y)
            (Ξ» x xs β†’ [_]-dup x)
  [_]↓ = ⟦ [_]↑ βŸ§β‡“
  {-# INLINE [_]↑ #-}
  {-# INLINE [_]↓ #-}
open _β†˜_ public

module _ {a p} {A : Type a} {P : 𝒦 A β†’ Type p} where
    𝒦-elim-prop : (βˆ€ {xs} β†’ isProp (P xs)) β†’
                  (βˆ€ x xs β†’ P xs β†’ P (x ∷ xs)) β†’
                  (P []) β†’
                  βˆ€ xs β†’ P xs
    𝒦-elim-prop isPropB f n = go
      where
      go : βˆ€ xs β†’ P xs
      go [] = n
      go (x ∷ xs) = f x xs (go xs)
      go (com x y xs j) = toPathP {A = Ξ» i β†’ P (com x y xs i)} (isPropB (transp (Ξ» i β†’ P (com x y xs i)) i0 (f x (y ∷ xs) (f y xs (go xs)))) (f y (x ∷ xs) (f x xs (go xs)))) j
      go (dup x xs j) = toPathP {A = Ξ» i β†’ P (dup x xs i)} (isPropB (transp (Ξ» i β†’ P (dup x xs i)) i0 (f x (x ∷ xs) (f x xs (go xs)))) (f x xs (go xs)) ) j
      go (trunc xs ys x y i j) =
        isOfHLevel→isOfHLevelDep 2
          (λ xs → isProp→isSet (isPropB {xs}))
          (go xs) (go ys)
          (cong go x) (cong go y)
          (trunc xs ys x y)
          i j

module _ {a b} {A : Type a} {B : Type b} where
  𝒦-rec : isSet B β†’
          (f : A β†’ B β†’ B) β†’
          (n : B) β†’
          (fdup : βˆ€ x xs β†’ f x (f x xs) ≑ f x xs) β†’
          (fcom : βˆ€ x y xs β†’ f x (f y xs) ≑ f y (f x xs)) β†’
          𝒦 A β†’
          B
  𝒦-rec isSetB f n fdup fcom = go
    where
    go : 𝒦 A β†’ B
    go [] = n
    go (x ∷ xs) = f x (go xs)
    go (com x y xs i) = fcom x y (go xs) i
    go (dup x xs i) = fdup x (go xs) i
    go (trunc xs ys x y i j) =
      isOfHLevel→isOfHLevelDep 2
        (Ξ» xs β†’ isSetB)
        (go xs) (go ys)
        (cong go x) (cong go y)
        (trunc xs ys x y)
        i j