Issue376.agda

-- {-# OPTIONS -v tc.meta:50 #-}
-- Andreas 2012-03-27, record pattern unification
module Issue376 where

import Common.Level
open import Common.Equality
open import Common.Irrelevance

record Sigma (A : Set)(B : A -> Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B fst
open Sigma public

record Unit : Set where
  constructor unit

bla1 : (A : Set) (a : A) ->
  let X : Unit -> A
      X = _
  in  X unit ≡ a
bla1 A a = refl

bla2 : (A : Set)(B : A -> Set) ->
  let X : Sigma A B -> Sigma A B
      X = _
  in  (x : A)(y : B x) -> X (x , y) ≡ (x , y)
bla2 A B x y = refl
-- _55 A B (x , y) := (x , y)

-- irrelevant records
bla3 : (A : Set)(B : A -> Set) ->
  let X : .(z : Sigma A B) -> (C : .(Sigma A B) -> Set) -> (.(z : Sigma A B) -> C z) -> C z
      X = _
  in  (x : A)(y : B x)(C : .(Sigma A B) -> Set)(k : .(z : Sigma A B) -> C z) ->
      X (x , y) C k ≡ k (x , y)
bla3 A B x y C k = refl

-- nested irrelevance
bla4 : (A : Set) ->
  let A' = Squash (Squash A) in
  let X : .(z : A') -> (C : .A' -> Set) -> (.(z : A') -> C z) -> C z
      X = _
  in  (a : A)(C : .A' -> Set)(k : .(z : A') -> C z) ->
      X (squash (squash a)) C k ≡ k (squash (squash a))
bla4 A a C k = refl