{-# OPTIONS --prop --rewriting #-}

module test where

open import lib
open import initialStrict
open import model

open CwF Ciₛₛ
open Model Miₛₛ

variable
  Γ Δ Θ : Con
  γ δ θ : Sub Δ Γ
  A B C : Ty Γ

-- let's see if ,∘ is definitional
,∘ : (γ : Sub Δ Γ)(A : Ty Γ)(a : Tm Δ (_[_]T {Γ} A {Δ} γ))(δ : Sub Θ Δ) →
  _∘_ {Γ ▹ A}{Δ} (_,[_]_ {Γ}{Δ} γ {A}{_[_]T {Γ} A {Δ} γ} ~refl a) {Θ} δ ~
  _,[_]_ {Γ}{Θ} (_∘_ {Γ}{Δ} γ {Θ} δ) {A}{_[_]T {Γ} A {Θ} (_∘_ {Γ}{Δ} γ {Θ} δ)} ~refl ((_[_]t {Δ}{_[_]T {Γ} A {Δ} γ} a {Θ} δ))
,∘ γ A a δ = ~refl

-- let's see if the more general version is definitional
,∘e : (γ : Sub Δ Γ)(A : Ty Γ)(A' : Ty Δ)(e : _[_]T {Γ} A {Δ} γ ~ A')(a : Tm Δ A')(δ : Sub Θ Δ) →
  _∘_ {Γ ▹ A}{Δ} (_,[_]_ {Γ}{Δ} γ {A}{A'} e a) {Θ} δ ~
  _,[_]_ {Γ}{Θ} (_∘_ {Γ}{Δ} γ {Θ} δ) {A}{_[_]T {Δ} A' {Θ} δ} (cong (λ A → _[_]T {Δ} A {Θ} δ) e) ((_[_]t {Δ}{A'} a {Θ} δ))
,∘e γ A A' e a δ = ~refl

-- smaller η rule

▹η' : (Γ : Con)(A : Ty Γ) → id {Γ ▹ A} ~ _,[_]_ {Γ}{Γ ▹ A}(p {Γ}{A}) {A}{_[_]T {Γ} A {Γ ▹ A} (p {Γ}{A})} ~refl (q {Γ}{A})
▹η' Γ A =  ▹η {Γ = Γ}{Γ ▹ A}{A}{γa = id {Γ ▹ A}} ⁻¹ -- ~refl does not work