With --postfix-projections, record fields are printed preceded by a dot when working within the record

[andreasabel]

{-# OPTIONS --postfix-projections #-}

open import Agda.Primitive  -- Universe levels
open import Relation.Binary using (Setoid; IsEquivalence); open Setoid; open IsEquivalence

---------------------------------------------------------------------------
-- Cartesian closed category as mathematical structure
---------------------------------------------------------------------------

record CCC o m e : Set (lsuc (o ⊔ m ⊔ e)) where

  ---------------------------------------------------------------------------
  -- Category
  ---------------------------------------------------------------------------

  field
    -- Objects.  We use propositional equality for objects.
    Ob  : Set o

    -- Morphisms.  The equality may be non-trivial.
    Homs : (a b : Ob) → Setoid m e

  -- Abbreviations to access Hom-set and its equality

  Hom : (a b : Ob) → Set m
  Hom a b = Homs a b .Carrier

  Eq : ∀{a b} (f g : Hom a b) → Set e
  Eq f g = Homs _ _ ._≈_ f g

  eq-refl : ∀{a b} {f : Hom a b} → Eq f f
  eq-refl {a} {b} {f} = Homs a b .isEquivalence .refl {f}

  eq-sym : ∀{a b} {f g : Hom a b} → Eq g f → Eq f g
  eq-sym e = Homs _ _ .isEquivalence .sym e

  eq-trans : ∀{a b} {f g h : Hom a b} → Eq f g → Eq g h → Eq f h
  eq-trans e e' = Homs _ _ .isEquivalence .trans e e'

  field
    -- Category operations
    id   : (a : Ob) → Hom a a
    comp : {a b c : Ob} (f : Hom b c) (g : Hom a b) → Hom a c

    -- Category laws
    id-l : ∀{a b} (f : Hom a b)
      → Eq (comp (id b) f) f
    id-r : ∀{a b} (f : Hom a b)
      → Eq (comp f (id a)) f
    assoc : ∀{a b c d} (f : Hom c d) (g : Hom b c) (h : Hom a b)
      → Eq (comp (comp f g) h) (comp f (comp g h))

    comp-cong : ∀{a b c} {f f' : Hom b c} {g g' : Hom a b}
      → Eq f f'
      → Eq g g'
      → Eq (comp f g) (comp f' g')

  ---------------------------------------------------------------------------
  -- Cartesian
  ---------------------------------------------------------------------------

  field
    -- Product object and projections
    Prod : (a b : Ob) → Ob
    π₁    : ∀{a b} → Hom (Prod a b) a
    π₂    : ∀{a b} → Hom (Prod a b) b

  -- Properties of candidates for the pairing function

  IsPair₁ : ∀{a b c} (f : Hom c a) (h : Hom c (Prod a b)) → Set _
  IsPair₁ f h = Eq (comp π₁ h) f

  IsPair₂ : ∀{a b c} (g : Hom c b) (h : Hom c (Prod a b)) → Set _
  IsPair₂ g h = Eq (comp π₂ h) g

  field
    -- Pairing and β-laws
    pair : ∀{a b c} (f : Hom c a) (g : Hom c b) → Hom c (Prod a b)
    β-π₁  : ∀{a b c} {f : Hom c a} {g : Hom c b} → IsPair₁ f (pair f g)
    β-π₂  : ∀{a b c} {f : Hom c a} {g : Hom c b} → IsPair₂ g (pair f g)

    -- Uniqueness of pairing
    pair-unique : ∀{a b c} (f : Hom c a) (g : Hom c b) (h : Hom c (Prod a b))
      → IsPair₁ f h
      → IsPair₂ g h
      → Eq h (pair f g)

  -- Congruence law for pairing

  pair-cong : ∀{a b c} {f f' : Hom c a} {g g' : Hom c b}
    → Eq f f'
    → Eq g g'
    → Eq (pair f g) (pair f' g')
  pair-cong {a} {b} {c} {f} {f'} {g} {g'} e e' = pair-unique f' g' (pair f g) ef eg
    where
    ef : Eq (comp π₁ (pair f g)) f'
    ef = eq-trans β-π₁ e
    eg : Eq (comp π₂ (pair f g)) g'
    eg = {! eq-trans β-π₂ e' !} -- C-c C-.

-- Prints:
-- Have: Eq (.comp (.π₂) (.pair (_f_415 e e') g)) g'
-- Note the extra dots!

[andreasabel]

Small test case:

{-# OPTIONS --postfix-projections #-}

open import Agda.Builtin.Equality

postulate
  A : Set

record R : Set where
  field
    a : A
    same : a ≡ a
  test : A
  test = same

-- Prints:  .a ≡ .a !=< A of type Set
-- Note the extra dots!

[andreasabel]

It works for prefix projections because the name of the record variable inside the declaration is "" (the empty string). Thus, the internal term a @0 is printed as a followed by the empty string which is what we expect. This hack breaks when we print projection postfix: empty string followed by .a. There is a workaround: use prefix projections if projecting from a variable with empty name. [Workaround onto hack, ever increasing the technological debt.]