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

-- another simple example of the phenomenon: if we use point-free
-- equality, the equalities are provable without funext

data _≡_ {ℓ}{A : Set ℓ} (x : A) : A → Set ℓ where
  refl : x ≡ x
infix 4 _≡_
_◾_ : ∀{ℓ}{A : Set ℓ}{x y z : A} → x ≡ y → y ≡ z → x ≡ z
refl ◾ e = e
infixl 4 _◾_
ap : ∀{ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'}(f : A → B){a₀ a₁ : A}(a₂ : a₀ ≡ a₁) → f a₀ ≡ f a₁
ap f refl = refl
transport : ∀{ℓ ℓ'}{A : Set ℓ}(P : A → Set ℓ'){x y : A}(p : x ≡ y) → P x → P y
transport P refl u = u
apid : ∀{ℓ}{A : Set ℓ}{a₀ a₁ : A}(a₂ : a₀ ≡ a₁) → ap (λ x → x) a₂ ≡ a₂
apid refl = refl

record Con : Set₁ where
  field
    V : Set
    E : Set
    dom cod : E → V
open Con

module Sub1 where
  record Sub (Δ Γ : Con) : Set where
    constructor mk
    field
      V : V Δ → V Γ
      E : E Δ → E Γ
      dom : (f : Con.E Δ) → dom Γ (E f) ≡ V (dom Δ f)
      cod : (f : Con.E Δ) → cod Γ (E f) ≡ V (cod Δ f)
  open Sub

  mkSub= : {Δ Γ : Con}
    {V₀ V₁ : V Δ → V Γ}(V₂ : V₀ ≡ V₁)
    {E₀ E₁ : E Δ → E Γ}(E₂ : E₀ ≡ E₁)
    {dom₀ : (f : Con.E Δ) → dom Γ (E₀ f) ≡ V₀ (dom Δ f)}{dom₁ : (f : Con.E Δ) → dom Γ (E₁ f) ≡ V₁ (dom Δ f)}(dom₂ : _≡_ {A = (f : Con.E Δ) → dom Γ (E₁ f) ≡ V₁ (dom Δ f)} (transport (λ V → (f : Con.E Δ) → dom Γ (E₁ f) ≡ V (dom Δ f)) V₂ (transport (λ E → (f : Con.E Δ) → dom Γ (E f) ≡ V₀ (dom Δ f)) E₂ dom₀)) dom₁) → 
    {cod₀ : (f : Con.E Δ) → cod Γ (E₀ f) ≡ V₀ (cod Δ f)}{cod₁ : (f : Con.E Δ) → cod Γ (E₁ f) ≡ V₁ (cod Δ f)}(cod₂ : _≡_ {A = (f : Con.E Δ) → cod Γ (E₁ f) ≡ V₁ (cod Δ f)} (transport (λ V → (f : Con.E Δ) → cod Γ (E₁ f) ≡ V (cod Δ f)) V₂ (transport (λ E → (f : Con.E Δ) → cod Γ (E f) ≡ V₀ (cod Δ f)) E₂ cod₀)) cod₁) → 
    _≡_ {A = Sub Δ Γ} (mk V₀ E₀ dom₀ cod₀) (mk V₁ E₁ dom₁ cod₁)
  mkSub= refl refl refl refl = refl

  _∘_ : ∀{Γ Δ} → Sub Δ Γ → ∀{Θ} → Sub Θ Δ → Sub Θ Γ
  V (γ ∘ δ) = λ I → V γ (V δ I)
  E (γ ∘ δ) = λ f → E γ (E δ f)
  dom (γ ∘ δ) = λ f → dom γ (E δ f) ◾ ap (V γ) (dom δ f)
  cod (γ ∘ δ) = λ f → cod γ (E δ f) ◾ ap (V γ) (cod δ f)

  id : ∀{Γ} → Sub Γ Γ
  V id = λ I → I
  E id = λ f → f
  dom id = λ f → refl
  cod id = λ f → refl

  idl : ∀{Γ Δ}{f : Sub Δ Γ} → id ∘ f ≡ f
  idl = mkSub= refl refl {!!} {!!} -- we need funext or equality has to be in SProp

  idr : ∀{Γ Δ}{f : Sub Δ Γ} → f ∘ id ≡ f
  idr = mkSub= refl refl {!!} {!!}

module Sub2 where
  record Sub (Δ Γ : Con) : Set where
    constructor mk
    field
      V : V Δ → V Γ
      E : E Δ → E Γ
      dom : (λ (f : Con.E Δ) → dom Γ (E f)) ≡ (λ f → V (dom Δ f))
      cod : (λ (f : Con.E Δ) → cod Γ (E f)) ≡ (λ f → V (cod Δ f))
  open Sub

  mkSub= : {Δ Γ : Con}
    {V₀ V₁ : V Δ → V Γ}(V₂ : V₀ ≡ V₁)
    {E₀ E₁ : E Δ → E Γ}(E₂ : E₀ ≡ E₁)
    {dom₀ : (λ (f : Con.E Δ) → dom Γ (E₀ f)) ≡ (λ f → V₀ (dom Δ f))}{dom₁ : (λ (f : Con.E Δ) → dom Γ (E₁ f)) ≡ (λ f → V₁ (dom Δ f))}(dom₂ : _≡_ {A = (λ (f : Con.E Δ) → dom Γ (E₁ f)) ≡ (λ f → V₁ (dom Δ f))} (transport (λ V → (λ (f : Con.E Δ) → dom Γ (E₁ f)) ≡ (λ f → V (dom Δ f))) V₂ (transport (λ E → (λ (f : Con.E Δ) → dom Γ (E f)) ≡ (λ f → V₀ (dom Δ f))) E₂ dom₀)) dom₁) → 
    {cod₀ : (λ (f : Con.E Δ) → cod Γ (E₀ f)) ≡ (λ f → V₀ (cod Δ f))}{cod₁ : (λ (f : Con.E Δ) → cod Γ (E₁ f)) ≡ (λ f → V₁ (cod Δ f))}(cod₂ : _≡_ {A = (λ (f : Con.E Δ) → cod Γ (E₁ f)) ≡ (λ f → V₁ (cod Δ f))} (transport (λ V → (λ (f : Con.E Δ) → cod Γ (E₁ f)) ≡ (λ f → V (cod Δ f))) V₂ (transport (λ E → (λ (f : Con.E Δ) → cod Γ (E f)) ≡ (λ f → V₀ (cod Δ f))) E₂ cod₀)) cod₁) → 
    _≡_ {A = Sub Δ Γ} (mk V₀ E₀ dom₀ cod₀) (mk V₁ E₁ dom₁ cod₁)
  mkSub= refl refl refl refl = refl

  _∘_ : ∀{Γ Δ} → Sub Δ Γ → ∀{Θ} → Sub Θ Δ → Sub Θ Γ
  V (γ ∘ δ) = λ I → V γ (V δ I)
  E (γ ∘ δ) = λ f → E γ (E δ f)
  dom (γ ∘ δ) = ap (λ α → λ f → α (E δ f)) (dom γ) ◾ ap (λ α → λ f → V γ (α f)) (dom δ)
  cod (γ ∘ δ) = ap (λ α → λ f → α (E δ f)) (cod γ) ◾ ap (λ α → λ f → V γ (α f)) (cod δ)

  id : ∀{Γ} → Sub Γ Γ
  V id = λ I → I
  E id = λ f → f
  dom id = refl
  cod id = refl

  idl : ∀{Γ Δ}{f : Sub Δ Γ} → id ∘ f ≡ f
  idl {Γ}{Δ}{f} = mkSub= refl refl (apid (dom f)) (apid (cod f))

  idr : ∀{Γ Δ}{f : Sub Δ Γ} → f ∘ id ≡ f
  idr = mkSub= refl refl {!!} {!!} -- TODO

  -- TODO: ass

  -- the following are not provable (they are equalities in the empty context):
  {-
  idl' : (λ (Γ Δ : Con)(f : Sub Δ Γ) → id ∘ f) ≡ (λ Γ Δ f → f)
  idl' = {!!}

  idr' : (λ (Γ Δ : Con)(f : Sub Δ Γ) → f ∘ id) ≡ λ Γ Δ f → f
  idr' = {!!}
  -}