module Semantics.EqualityJudgments where

open import Semantics.SyntaxComputationRulesITT79
open import IType.Nat
open import IType.Product

data isEqN : F zero → F zero → Set where
  zeroEqN : {a a' : F zero}
    → a => zeroV
    → a' => zeroV
    → isEqN a a'
  succEqN : {a a' b b' : F zero}
    → a => succV b
    → a' => succV b'
    → isEqN b b'
    → isEqN a a'

mutual
  data isEqset : F zero → F zero → Set where
    NEqset : {A A' : F zero}
      → A => NV
      → A' => NV
      → isEqset A A'
    piEqset : {A A' : F zero} → (B B' : F zero) → (C C' : F one)
      → A => piV B C
      → A' => piV B' C'
      → (p : isEqset B B')   
      → ((x x' : F zero) → isEqel x x' B B' p → isEqset (C [ x ]) (C' [ x' ]))
      → isEqset A A'
    IdEqset : {A A' : F zero} → (B C b c B' C' b' c' : F zero)
      → A => IdV B C b c
      → A' => IdV B' C' b' c'
      → isEqset B C
      → isEqset B' C'
      → (q : isEqset B B')   
      → (r : isEqset C C')   
      → isEqel b b' B B' q
      → isEqel c c' C C' r 
      → isEqset A A'
    
  isEqel : F zero → F zero → (A A' : F zero) → isEqset A A' → Set
  isEqel a a' A A' (NEqset d d') = isEqN a a'
  isEqel a a' A A' (piEqset B B' C C' d d' p q) = (x x' : F zero)
    → (y : isEqel x x' B B' p)
    → isEqel (a # x) (a' # x') (C [ x ]) (C' [ x' ]) (q x x' y)
  isEqel a a' A A' (IdEqset B C b c B' C' b' c' d d' p p' q r x y)
    = (isEqel b c B C p)
    × (isEqel b' c' B' C' p')
    × (a => refV)
    × (a' => refV)

mutual
  data isEqTy : F zero → F zero → Set where
    NEqTy : {A A' : F zero}
      → A => NV
      → A' => NV
      → isEqTy A A'
    piEqTy : {A A' : F zero} → (B B' : F zero) → (C C' : F one)
      → A => piV B C
      → A' => piV B' C'
      → (p : isEqTy B B')   
      → ((x x' : F zero) → isEqTm x x' B B' p → isEqTy (C [ x ]) (C' [ x' ]))
      → isEqTy A A'
    IdEqTy : {A A' : F zero} → (B C b c B' C' b' c' : F zero)
      → A => IdV B C b c
      → A' => IdV B' C' b' c'
      → (q : isEqTy B B')   
      → (r : isEqTy C C')
      → isEqTy B C
      → isEqTy B' C'
      → isEqTm b b' B B' q
      → isEqTm c c' C C' r 
      → isEqTy A A'
    setEqTy : {A A' : F zero}
      → A => setV
      → A' => setV
      → isEqTy A A'
      
  isEqTm : F zero → F zero → (A A' : F zero) → isEqTy A A' → Set
  isEqTm a a' A A' (NEqTy d d') = isEqN a a'
  isEqTm a a' A A' (piEqTy B B' C C' d d' p q) = (x x' : F zero)
    → (y : isEqTm x x' B B' p)
    → isEqTm (a # x) (a' # x') (C [ x ]) (C' [ x' ]) (q x x' y)
  isEqTm a a' A A' (IdEqTy B C b c B' C' b' c' d d' q r p p' x y)
    = (a => refV)
    × (a' => refV)
    × (isEqTm b c B C p)
    × (isEqTm b' c' B' C' p')
  isEqTm a a' A A' (setEqTy d d') = isEqset a a'

-- the last clause implies equality reflection and uniqueness of identity proofs
-- we get a model of extensional ITT (1979)

isTy : F zero → Set
isTy A = isEqTy A A

-- refEqTy : (A : F zero) → isTy A → isEqTy A A
-- refEqTy A p = p

isEqTm₁ : F zero → F zero → (A : F zero) → isTy A → Set
isEqTm₁ a a' A p = isEqTm a a' A A p

isTm :  F zero → (A : F zero) → isTy A → Set
isTm a A p = isEqTm₁ a a A p

-- equality reflection

postulate
  Id-formation : (a a' A : F zero)
    → (p : isTy A)
    → isTm a A p
    → isTm a' A p
    → isTy (IdF # A # a # a')
  
eqReflection : (a a' c A : F zero)
  → (p : isTy A)
  → (q : isTm a A p)
  → (q' : isTm a' A p)
  → isTm c (IdF # A # a # a') (Id-formation a a' A p q q')
  → isEqTm₁ a a' A p
eqReflection a a' c A p q r s = {!!}