{-# OPTIONS --without-K #-}

open import lib.Basics

{-
The generic nonrecursive higher inductive type with one point constructor and
one paths constructor.
-}

module lib.types.Generic1HIT {i j} (A : Type i) (B : Type j)
  (g h : B  A) where


{-
data T : Type where
  cc : A → T
  pp : (b : B) → cc (f' b) ≡ cc (g b)
-}
module _ where
  private
    data #T-aux : Type (lmax i j) where
      #cc : A  #T-aux

    data #T : Type (lmax i j) where
      #t : #T-aux  (Unit  Unit)  #T

  T : Type _
  T = #T

  cc : A  T
  cc a = #t (#cc a) _

  postulate  -- HIT
    pp : (b : B)  cc (g b) == cc (h b)

  module Elim {k} {P : T  Type k} (cc* : (a : A)  P (cc a))
    (pp* : (b : B)  cc* (g b) == cc* (h b) [ P  pp b ]) where

    f : Π T P
    f = f-aux phantom  where

      f-aux : Phantom pp*  Π T P
      f-aux phantom (#t (#cc a) _) = cc* a

    postulate  -- HIT
      pp-β : (b : B)  apd f (pp b) == pp* b

open Elim public using () renaming (f to elim)

module Rec {k} {C : Type k} (cc* : A  C)
  (pp* : (b : B)  cc* (g b) == cc* (h b)) where

  private module M = Elim cc*  b  ↓-cst-in (pp* b))

  f : T  C
  f = M.f

  pp-β : (b : B)  ap f (pp b) == pp* b
  pp-β b = apd=cst-in {f = f} (M.pp-β b)

module RecType {k} (C : A  Type k) (D : (b : B)  C (g b)  C (h b)) where

  open Rec C (ua  D) public

  coe-pp-β : (b : B) (d : C (g b))  coe (ap f (pp b)) d == –> (D b) d
  coe-pp-β b d =
    coe (ap f (pp b)) d   =⟨ pp-β _ |in-ctx  u  coe u d) 
    coe (ua (D b)) d      =⟨ coe-β (D b) d 
    –> (D b) d 

  -- Dependent path in [P] over [pp b]
  module _ {b : B} {d : C (g b)} {d' : C (h b)} where
    ↓-pp-in : –> (D b) d == d'  d == d' [ f  pp b ]
    ↓-pp-in p = from-transp f (pp b) (coe-pp-β b d ∙' p)

    ↓-pp-out : d == d' [ f  pp b ]  –> (D b) d == d'
    ↓-pp-out p = ! (coe-pp-β b d)  to-transp p

    ↓-pp-β : (q : –> (D b) d == d')  ↓-pp-out (↓-pp-in q) == q
    ↓-pp-β q =
      ↓-pp-out (↓-pp-in q)
                        =⟨ idp 
      ! (coe-pp-β b d)  to-transp (from-transp f (pp b) (coe-pp-β b d ∙' q))
                 =⟨ to-transp-β f (pp b) (coe-pp-β b d ∙' q) |in-ctx  u  ! (coe-pp-β b d)  u) 
      ! (coe-pp-β b d)  (coe-pp-β b d ∙' q)
                 =⟨ lem (coe-pp-β b d) q 
      q   where

        lem :  {i} {A : Type i} {x y z : A} (p : x == y) (q : y == z)
           ! p  (p ∙' q) == q
        lem idp idp = idp