text:
open import Prelude
open import Nat
open import core
open import contexts
open import disjointness

-- this module contains lemmas and properties about the holes-disjoint
-- judgement that double check that it acts as we would expect

module holes-disjoint-checks where
  -- these lemmas are all structurally recursive and quite
  -- mechanical. morally, they establish the properties about reduction
  -- that would be obvious / baked into Agda if holes-disjoint was defined
  -- as a function rather than a judgement (datatype), or if we had defined
  -- all the O(n^2) cases rather than relying on a little indirection to
  -- only have O(n) cases. that work has to go somewhwere, and we prefer
  -- that it goes here.
  ds-lem-asc : ∀{e1 e2 τ} → holes-disjoint e2 e1 → holes-disjoint e2 (e1 ·: τ)
  ds-lem-asc HDConst = HDConst
  ds-lem-asc (HDAsc hd) = HDAsc (ds-lem-asc hd)
  ds-lem-asc HDVar = HDVar
  ds-lem-asc (HDLam1 hd) = HDLam1 (ds-lem-asc hd)
  ds-lem-asc (HDLam2 hd) = HDLam2 (ds-lem-asc hd)
  ds-lem-asc (HDHole x) = HDHole (HNAsc x)
  ds-lem-asc (HDNEHole x hd) = HDNEHole (HNAsc x) (ds-lem-asc hd)
  ds-lem-asc (HDAp hd hd₁) = HDAp (ds-lem-asc hd) (ds-lem-asc hd₁)
  ds-lem-asc (HDFst hd) = HDFst (ds-lem-asc hd)
  ds-lem-asc (HDSnd hd) = HDSnd (ds-lem-asc hd)
  ds-lem-asc (HDPair hd hd₁) = HDPair (ds-lem-asc hd) (ds-lem-asc hd₁)

  ds-lem-lam1 : ∀{e1 e2 x} → holes-disjoint e2 e1 → holes-disjoint e2 (·λ x e1)
  ds-lem-lam1 HDConst = HDConst
  ds-lem-lam1 (HDAsc hd) = HDAsc (ds-lem-lam1 hd)
  ds-lem-lam1 HDVar = HDVar
  ds-lem-lam1 (HDLam1 hd) = HDLam1 (ds-lem-lam1 hd)
  ds-lem-lam1 (HDLam2 hd) = HDLam2 (ds-lem-lam1 hd)
  ds-lem-lam1 (HDHole x₁) = HDHole (HNLam1 x₁)
  ds-lem-lam1 (HDNEHole x₁ hd) = HDNEHole (HNLam1 x₁) (ds-lem-lam1 hd)
  ds-lem-lam1 (HDAp hd hd₁) = HDAp (ds-lem-lam1 hd) (ds-lem-lam1 hd₁)
  ds-lem-lam1 (HDFst hd) = HDFst (ds-lem-lam1 hd)
  ds-lem-lam1 (HDSnd hd) = HDSnd (ds-lem-lam1 hd)
  ds-lem-lam1 (HDPair hd hd₁) = HDPair (ds-lem-lam1 hd) (ds-lem-lam1 hd₁)

  ds-lem-lam2 : ∀{e1 e2 x τ} → holes-disjoint e2 e1 → holes-disjoint e2 (·λ x [ τ ] e1)
  ds-lem-lam2 HDConst = HDConst
  ds-lem-lam2 (HDAsc hd) = HDAsc (ds-lem-lam2 hd)
  ds-lem-lam2 HDVar = HDVar
  ds-lem-lam2 (HDLam1 hd) = HDLam1 (ds-lem-lam2 hd)
  ds-lem-lam2 (HDLam2 hd) = HDLam2 (ds-lem-lam2 hd)
  ds-lem-lam2 (HDHole x₁) = HDHole (HNLam2 x₁)
  ds-lem-lam2 (HDNEHole x₁ hd) = HDNEHole (HNLam2 x₁) (ds-lem-lam2 hd)
  ds-lem-lam2 (HDAp hd hd₁) = HDAp (ds-lem-lam2 hd) (ds-lem-lam2 hd₁)
  ds-lem-lam2 (HDFst hd) = HDFst (ds-lem-lam2 hd)
  ds-lem-lam2 (HDSnd hd) = HDSnd (ds-lem-lam2 hd)
  ds-lem-lam2 (HDPair hd hd₁) = HDPair (ds-lem-lam2 hd) (ds-lem-lam2 hd₁)

  ds-lem-nehole : ∀{e e1 u} → holes-disjoint e e1 → hole-name-new e u → holes-disjoint e ⦇⌜ e1 ⌟⦈[ u ]
  ds-lem-nehole HDConst ν = HDConst
  ds-lem-nehole (HDAsc hd) (HNAsc ν) = HDAsc (ds-lem-nehole hd ν)
  ds-lem-nehole HDVar ν = HDVar
  ds-lem-nehole (HDLam1 hd) (HNLam1 ν) = HDLam1 (ds-lem-nehole hd ν)
  ds-lem-nehole (HDLam2 hd) (HNLam2 ν) = HDLam2 (ds-lem-nehole hd ν)
  ds-lem-nehole (HDHole x) (HNHole x₁) = HDHole (HNNEHole (flip x₁) x)
  ds-lem-nehole (HDNEHole x hd) (HNNEHole x₁ ν) = HDNEHole (HNNEHole (flip x₁) x) (ds-lem-nehole hd ν)
  ds-lem-nehole (HDAp hd hd₁) (HNAp ν ν₁) = HDAp (ds-lem-nehole hd ν) (ds-lem-nehole hd₁ ν₁)
  ds-lem-nehole (HDFst hd) (HNFst v) = HDFst (ds-lem-nehole hd v)
  ds-lem-nehole (HDSnd hd) (HNSnd v) = HDSnd (ds-lem-nehole hd v)
  ds-lem-nehole (HDPair hd hd₁) (HNPair v v₁) = HDPair (ds-lem-nehole hd v) (ds-lem-nehole hd₁ v₁)

  ds-lem-ap : ∀{e1 e2 e3} → holes-disjoint e3 e1 → holes-disjoint e3 e2 → holes-disjoint e3 (e1 ∘ e2)
  ds-lem-ap HDConst hd2 = HDConst
  ds-lem-ap (HDAsc hd1) (HDAsc hd2) = HDAsc (ds-lem-ap hd1 hd2)
  ds-lem-ap HDVar hd2 = HDVar
  ds-lem-ap (HDLam1 hd1) (HDLam1 hd2) = HDLam1 (ds-lem-ap hd1 hd2)
  ds-lem-ap (HDLam2 hd1) (HDLam2 hd2) = HDLam2 (ds-lem-ap hd1 hd2)
  ds-lem-ap (HDHole x) (HDHole x₁) = HDHole (HNAp x x₁)
  ds-lem-ap (HDNEHole x hd1) (HDNEHole x₁ hd2) = HDNEHole (HNAp x x₁) (ds-lem-ap hd1 hd2)
  ds-lem-ap (HDAp hd1 hd2) (HDAp hd3 hd4) = HDAp (ds-lem-ap hd1 hd3) (ds-lem-ap hd2 hd4)
  ds-lem-ap (HDFst hd) (HDFst hd2) = HDFst (ds-lem-ap hd hd2)
  ds-lem-ap (HDSnd hd) (HDSnd hd2) = HDSnd (ds-lem-ap hd hd2)
  ds-lem-ap (HDPair hd1 hd2) (HDPair hd3 hd4) = HDPair (ds-lem-ap hd1 hd3) (ds-lem-ap hd2 hd4)

  ds-lem-pair : ∀{e1 e2 e3} → holes-disjoint e3 e1 → holes-disjoint e3 e2 → holes-disjoint e3 ⟨ e1 , e2 ⟩
  ds-lem-pair HDConst HDConst = HDConst
  ds-lem-pair (HDAsc hd1) (HDAsc hd2) = HDAsc (ds-lem-pair hd1 hd2)
  ds-lem-pair HDVar HDVar = HDVar
  ds-lem-pair (HDLam1 hd1) (HDLam1 hd2) = HDLam1 (ds-lem-pair hd1 hd2)
  ds-lem-pair (HDLam2 hd1) (HDLam2 hd2) = HDLam2 (ds-lem-pair hd1 hd2)
  ds-lem-pair (HDHole x) (HDHole x₁) = HDHole (HNPair x x₁)
  ds-lem-pair (HDNEHole x hd1) (HDNEHole x₁ hd2) = HDNEHole (HNPair x x₁) (ds-lem-pair hd1 hd2)
  ds-lem-pair (HDAp hd1 hd2) (HDAp hd3 hd4) = HDAp (ds-lem-pair hd1 hd3) (ds-lem-pair hd2 hd4)
  ds-lem-pair (HDFst hd1) (HDFst hd2) = HDFst (ds-lem-pair hd1 hd2)
  ds-lem-pair (HDSnd hd1) (HDSnd hd2) = HDSnd (ds-lem-pair hd1 hd2)
  ds-lem-pair (HDPair hd1 hd2) (HDPair hd3 hd4) = HDPair (ds-lem-pair hd1 hd3) (ds-lem-pair hd2 hd4)

  ds-lem-fst : ∀{e e'} → holes-disjoint e' e → holes-disjoint e' (fst e)
  ds-lem-fst HDConst = HDConst
  ds-lem-fst (HDAsc hd) = HDAsc (ds-lem-fst hd)
  ds-lem-fst HDVar = HDVar
  ds-lem-fst (HDLam1 hd) = HDLam1 (ds-lem-fst hd)
  ds-lem-fst (HDLam2 hd) = HDLam2 (ds-lem-fst hd)
  ds-lem-fst (HDHole x) = HDHole (HNFst x)
  ds-lem-fst (HDNEHole x hd) = HDNEHole (HNFst x) (ds-lem-fst hd)
  ds-lem-fst (HDAp hd hd₁) = HDAp (ds-lem-fst hd) (ds-lem-fst hd₁)
  ds-lem-fst (HDFst hd) = HDFst (ds-lem-fst hd)
  ds-lem-fst (HDSnd hd) = HDSnd (ds-lem-fst hd)
  ds-lem-fst (HDPair hd hd₁) = HDPair (ds-lem-fst hd) (ds-lem-fst hd₁)

  ds-lem-snd : ∀{e e'} → holes-disjoint e' e → holes-disjoint e' (snd e)
  ds-lem-snd HDConst = HDConst
  ds-lem-snd (HDAsc hd) = HDAsc (ds-lem-snd hd)
  ds-lem-snd HDVar = HDVar
  ds-lem-snd (HDLam1 hd) = HDLam1 (ds-lem-snd hd)
  ds-lem-snd (HDLam2 hd) = HDLam2 (ds-lem-snd hd)
  ds-lem-snd (HDHole x) = HDHole (HNSnd x)
  ds-lem-snd (HDNEHole x hd) = HDNEHole (HNSnd x) (ds-lem-snd hd)
  ds-lem-snd (HDAp hd hd₁) = HDAp (ds-lem-snd hd) (ds-lem-snd hd₁)
  ds-lem-snd (HDFst hd) = HDFst (ds-lem-snd hd)
  ds-lem-snd (HDSnd hd) = HDSnd (ds-lem-snd hd)
  ds-lem-snd (HDPair hd hd₁) = HDPair (ds-lem-snd hd) (ds-lem-snd hd₁)

  -- holes-disjoint is symmetric
  disjoint-sym : (e1 e2 : eexp) → holes-disjoint e1 e2 → holes-disjoint e2 e1
  disjoint-sym .c c HDConst = HDConst
  disjoint-sym .c (e2 ·: x) HDConst = HDAsc (disjoint-sym _ _ HDConst)
  disjoint-sym .c (X x) HDConst = HDVar
  disjoint-sym .c (·λ x e2) HDConst = HDLam1 (disjoint-sym c e2 HDConst)
  disjoint-sym .c (·λ x [ x₁ ] e2) HDConst = HDLam2 (disjoint-sym c e2 HDConst)
  disjoint-sym .c ⦇⦈[ x ] HDConst = HDHole HNConst
  disjoint-sym .c ⦇⌜ e2 ⌟⦈[ x ] HDConst = HDNEHole HNConst (disjoint-sym c e2 HDConst)
  disjoint-sym .c (e2 ∘ e3) HDConst = HDAp (disjoint-sym c e2 HDConst) (disjoint-sym c e3 HDConst)
  disjoint-sym .c ⟨ e2 , e3 ⟩ HDConst = HDPair (disjoint-sym c e2 HDConst) (disjoint-sym c e3 HDConst)
  disjoint-sym .c (fst e2) HDConst = HDFst (disjoint-sym c e2 HDConst)
  disjoint-sym .c (snd e2) HDConst = HDSnd (disjoint-sym c e2 HDConst)

  disjoint-sym _ c (HDAsc hd) = HDConst
  disjoint-sym _ (e2 ·: x) (HDAsc hd) with disjoint-sym _ _ hd
  disjoint-sym _ (e2 ·: x) (HDAsc hd) | HDAsc ih = HDAsc (ds-lem-asc ih)
  disjoint-sym _ (X x) (HDAsc hd) = HDVar
  disjoint-sym _ (·λ x e2) (HDAsc hd) with disjoint-sym _ _ hd
  disjoint-sym _ (·λ x e2) (HDAsc hd) | HDLam1 ih = HDLam1 (ds-lem-asc ih)
  disjoint-sym _ (·λ x [ x₁ ] e2) (HDAsc hd) with disjoint-sym _ _ hd
  disjoint-sym _ (·λ x [ x₁ ] e2) (HDAsc hd) | HDLam2 ih = HDLam2 (ds-lem-asc ih)
  disjoint-sym _ ⦇⦈[ x ] (HDAsc hd) with disjoint-sym _ _ hd
  disjoint-sym _ ⦇⦈[ x ] (HDAsc hd) | HDHole x₁ = HDHole (HNAsc x₁)
  disjoint-sym _ ⦇⌜ e2 ⌟⦈[ x ] (HDAsc hd) with disjoint-sym _ _ hd
  disjoint-sym _ ⦇⌜ e2 ⌟⦈[ x ] (HDAsc hd) | HDNEHole x₁ ih = HDNEHole (HNAsc x₁) (ds-lem-asc ih)
  disjoint-sym _ (e2 ∘ e3) (HDAsc hd) with disjoint-sym _ _ hd
  disjoint-sym _ (e2 ∘ e3) (HDAsc hd) | HDAp ih ih₁ = HDAp (ds-lem-asc ih) (ds-lem-asc ih₁)
  disjoint-sym _ ⟨ e2 , e3 ⟩ (HDAsc hd) with disjoint-sym _ _ hd
  disjoint-sym .(_ ·: _) ⟨ e2 , e3 ⟩ (HDAsc hd) | HDPair ih ih₁ = HDPair (ds-lem-asc ih) (ds-lem-asc ih₁)
  disjoint-sym _ (fst e2) (HDAsc hd) with disjoint-sym _ _ hd
  disjoint-sym .(_ ·: _) (fst e2) (HDAsc hd) | HDFst ih = HDFst (ds-lem-asc ih)
  disjoint-sym _ (snd e2) (HDAsc hd) with disjoint-sym _ _ hd
  disjoint-sym .(_ ·: _) (snd e2) (HDAsc hd) | HDSnd ih = HDSnd (ds-lem-asc ih)

  disjoint-sym _ c HDVar = HDConst
  disjoint-sym _ (e2 ·: x₁) HDVar = HDAsc (disjoint-sym _ e2 HDVar)
  disjoint-sym _ (X x₁) HDVar = HDVar
  disjoint-sym _ (·λ x₁ e2) HDVar = HDLam1 (disjoint-sym _ e2 HDVar)
  disjoint-sym _ (·λ x₁ [ x₂ ] e2) HDVar = HDLam2 (disjoint-sym _ e2 HDVar)
  disjoint-sym _ ⦇⦈[ x₁ ] HDVar = HDHole HNVar
  disjoint-sym _ ⦇⌜ e2 ⌟⦈[ x₁ ] HDVar = HDNEHole HNVar (disjoint-sym _ e2 HDVar)
  disjoint-sym _ (e2 ∘ e3) HDVar = HDAp (disjoint-sym _ e2 HDVar) (disjoint-sym _ e3 HDVar)
  disjoint-sym _ ⟨ e2 , e3 ⟩ HDVar = HDPair (disjoint-sym (X _) e2 HDVar)
                                       (disjoint-sym (X _) e3 HDVar)
  disjoint-sym _ (fst e2) HDVar = HDFst (disjoint-sym (X _) e2 HDVar)
  disjoint-sym _ (snd e2) HDVar = HDSnd (disjoint-sym (X _) e2 HDVar)

  disjoint-sym _ c (HDLam1 hd) = HDConst
  disjoint-sym _ (e2 ·: x₁) (HDLam1 hd) with disjoint-sym _ _ hd
  disjoint-sym _ (e2 ·: x₁) (HDLam1 hd) | HDAsc ih = HDAsc (ds-lem-lam1 ih)
  disjoint-sym _ (X x₁) (HDLam1 hd) = HDVar
  disjoint-sym _ (·λ x₁ e2) (HDLam1 hd) with disjoint-sym _ _ hd
  disjoint-sym _ (·λ x₁ e2) (HDLam1 hd) | HDLam1 ih = HDLam1 (ds-lem-lam1 ih)
  disjoint-sym _ (·λ x₁ [ x₂ ] e2) (HDLam1 hd) with disjoint-sym _ _ hd
  disjoint-sym _ (·λ x₁ [ x₂ ] e2) (HDLam1 hd) | HDLam2 ih = HDLam2 (ds-lem-lam1 ih)
  disjoint-sym _ ⦇⦈[ x₁ ] (HDLam1 hd) with disjoint-sym _ _ hd
  disjoint-sym _ ⦇⦈[ x₁ ] (HDLam1 hd) | HDHole x = HDHole (HNLam1 x)
  disjoint-sym _ ⦇⌜ e2 ⌟⦈[ x₁ ] (HDLam1 hd) with disjoint-sym _ _ hd
  disjoint-sym _ ⦇⌜ e2 ⌟⦈[ x₁ ] (HDLam1 hd) | HDNEHole x ih = HDNEHole (HNLam1 x) (ds-lem-lam1 ih)
  disjoint-sym _ (e2 ∘ e3) (HDLam1 hd) with disjoint-sym _ _ hd
  disjoint-sym _ (e2 ∘ e3) (HDLam1 hd) | HDAp ih ih₁ = HDAp (ds-lem-lam1 ih) (ds-lem-lam1 ih₁)
  disjoint-sym _ ⟨ e2 , e3 ⟩ (HDLam1 hd) with disjoint-sym _ _ hd
  disjoint-sym _ ⟨ e2 , e3 ⟩ (HDLam1 hd) | HDPair ih ih₁ = HDPair (ds-lem-lam1 ih) (ds-lem-lam1 ih₁)
  disjoint-sym _ (fst e2) (HDLam1 hd) with disjoint-sym _ _ hd
  disjoint-sym _ (fst e2) (HDLam1 hd) | HDFst ih = HDFst (ds-lem-lam1 ih)
  disjoint-sym _ (snd e2) (HDLam1 hd) with disjoint-sym _ _ hd
  disjoint-sym _ (snd e2) (HDLam1 hd) | HDSnd ih = HDSnd (ds-lem-lam1 ih)

  disjoint-sym _ c (HDLam2 hd) = HDConst
  disjoint-sym _ (e2 ·: x₁) (HDLam2 hd) with disjoint-sym _ _ hd
  disjoint-sym _ (e2 ·: x₁) (HDLam2 hd) | HDAsc ih = HDAsc (ds-lem-lam2 ih)
  disjoint-sym _ (X x₁) (HDLam2 hd) = HDVar
  disjoint-sym _ (·λ x₁ e2) (HDLam2 hd) with disjoint-sym _ _ hd
  disjoint-sym _ (·λ x₁ e2) (HDLam2 hd) | HDLam1 ih = HDLam1 (ds-lem-lam2 ih)
  disjoint-sym _ (·λ x₁ [ x₂ ] e2) (HDLam2 hd) with disjoint-sym _ _ hd
  disjoint-sym _ (·λ x₁ [ x₂ ] e2) (HDLam2 hd) | HDLam2 ih = HDLam2 (ds-lem-lam2 ih)
  disjoint-sym _ ⦇⦈[ x₁ ] (HDLam2 hd) with disjoint-sym _ _ hd
  disjoint-sym _ ⦇⦈[ x₁ ] (HDLam2 hd) | HDHole x = HDHole (HNLam2 x)
  disjoint-sym _ ⦇⌜ e2 ⌟⦈[ x₁ ] (HDLam2 hd) with disjoint-sym _ _ hd
  disjoint-sym _ ⦇⌜ e2 ⌟⦈[ x₁ ] (HDLam2 hd) | HDNEHole x ih = HDNEHole (HNLam2 x) (ds-lem-lam2 ih)
  disjoint-sym _ (e2 ∘ e3) (HDLam2 hd) with disjoint-sym _ _ hd
  disjoint-sym _ (e2 ∘ e3) (HDLam2 hd) | HDAp ih ih₁ = HDAp (ds-lem-lam2 ih) (ds-lem-lam2 ih₁)
  disjoint-sym _ ⟨ e2 , e3 ⟩ (HDLam2 hd) with disjoint-sym _ _ hd
  disjoint-sym _ ⟨ e2 , e3 ⟩ (HDLam2 hd) | HDPair ih ih₁ = HDPair (ds-lem-lam2 ih) (ds-lem-lam2 ih₁)
  disjoint-sym _ (fst e2) (HDLam2 hd) with disjoint-sym _ _ hd
  disjoint-sym _ (fst e2) (HDLam2 hd) | HDFst ih = HDFst (ds-lem-lam2 ih)
  disjoint-sym _ (snd e2) (HDLam2 hd) with disjoint-sym _ _ hd
  disjoint-sym _ (snd e2) (HDLam2 hd) | HDSnd ih = HDSnd (ds-lem-lam2 ih)

  disjoint-sym _ c (HDHole x) = HDConst
  disjoint-sym _ (e2 ·: x) (HDHole (HNAsc x₁)) = HDAsc (disjoint-sym ⦇⦈[ _ ] e2 (HDHole x₁))
  disjoint-sym _ (X x) (HDHole x₁) = HDVar
  disjoint-sym _ (·λ x e2) (HDHole (HNLam1 x₁)) = HDLam1 (disjoint-sym ⦇⦈[ _ ] e2 (HDHole x₁))
  disjoint-sym _ (·λ x [ x₁ ] e2) (HDHole (HNLam2 x₂)) = HDLam2 (disjoint-sym ⦇⦈[ _ ] e2 (HDHole x₂))
  disjoint-sym _ ⦇⦈[ x ] (HDHole (HNHole x₁)) =  HDHole (HNHole (flip x₁))
  disjoint-sym _ ⦇⌜ e2 ⌟⦈[ u' ] (HDHole (HNNEHole x x₁)) = HDNEHole (HNHole (flip x)) (disjoint-sym ⦇⦈[ _ ] e2 (HDHole x₁))
  disjoint-sym _ (e2 ∘ e3) (HDHole (HNAp x x₁)) = HDAp (disjoint-sym ⦇⦈[ _ ] e2 (HDHole x))
                                                    (disjoint-sym ⦇⦈[ _ ] e3 (HDHole x₁))
  disjoint-sym _ ⟨ e2 , e3 ⟩ (HDHole (HNPair x1 x2)) = HDPair (disjoint-sym ⦇⦈[ _ ] e2 (HDHole x1)) (disjoint-sym ⦇⦈[ _ ] e3 (HDHole x2))
  disjoint-sym _ (fst e2) (HDHole (HNFst x)) = HDFst (disjoint-sym ⦇⦈[ _ ] e2 (HDHole x))
  disjoint-sym _ (snd e2) (HDHole (HNSnd x)) = HDSnd (disjoint-sym ⦇⦈[ _ ] e2 (HDHole x))

  disjoint-sym _ c (HDNEHole x hd) = HDConst
  disjoint-sym _ (e2 ·: x) (HDNEHole x₁ hd) with disjoint-sym _ _ hd
  disjoint-sym _ (e ·: x) (HDNEHole (HNAsc x₁) hd) | HDAsc ih = HDAsc (ds-lem-nehole ih x₁)
  disjoint-sym _ (X x) (HDNEHole x₁ hd) = HDVar
  disjoint-sym _ (·λ x e2) (HDNEHole x₁ hd) with disjoint-sym _ _ hd
  disjoint-sym _ (·λ x e2) (HDNEHole (HNLam1 x₁) hd) | HDLam1 ih = HDLam1 (ds-lem-nehole ih x₁)
  disjoint-sym _ (·λ x [ x₁ ] e2) (HDNEHole x₂ hd) with disjoint-sym _ _ hd
  disjoint-sym _ (·λ x [ x₁ ] e2) (HDNEHole (HNLam2 x₂) hd) | HDLam2 ih = HDLam2 (ds-lem-nehole ih x₂)
  disjoint-sym _ ⦇⦈[ x ] (HDNEHole x₁ hd) with disjoint-sym _ _ hd
  disjoint-sym _ ⦇⦈[ x ] (HDNEHole (HNHole x₂) hd) | HDHole x₁ = HDHole (HNNEHole (flip x₂) x₁)
  disjoint-sym _ ⦇⌜ e2 ⌟⦈[ x ] (HDNEHole x₁ hd) with disjoint-sym _ _ hd
  disjoint-sym _ ⦇⌜ e2 ⌟⦈[ x ] (HDNEHole (HNNEHole x₂ x₃) hd) | HDNEHole x₁ ih = HDNEHole (HNNEHole (flip x₂) x₁) (ds-lem-nehole ih x₃)
  disjoint-sym _ (e2 ∘ e3) (HDNEHole x hd) with disjoint-sym _ _ hd
  disjoint-sym _ (e1 ∘ e3) (HDNEHole (HNAp x x₁) hd) | HDAp ih ih₁ = HDAp (ds-lem-nehole ih x) (ds-lem-nehole ih₁ x₁)
  disjoint-sym _ ⟨ e2 , e3 ⟩ (HDNEHole x hd) with disjoint-sym _ _ hd
  disjoint-sym _ ⟨ e2 , e3 ⟩ (HDNEHole (HNPair x x₁) hd) | HDPair ih ih₁ = HDPair (ds-lem-nehole ih x) (ds-lem-nehole ih₁ x₁)
  disjoint-sym _ (fst e2) (HDNEHole x hd) with disjoint-sym _ _ hd
  disjoint-sym _ (fst e2) (HDNEHole (HNFst x1) hd) | HDFst ih = HDFst (ds-lem-nehole ih x1)
  disjoint-sym _ (snd e2) (HDNEHole x hd) with disjoint-sym _ _ hd
  disjoint-sym _ (snd e2) (HDNEHole (HNSnd x1) hd) | HDSnd ih = HDSnd (ds-lem-nehole ih x1)

  disjoint-sym _ c (HDAp hd hd₁) = HDConst
  disjoint-sym _ (e3 ·: x) (HDAp hd hd₁) with disjoint-sym _ _ hd | disjoint-sym _ _ hd₁
  disjoint-sym _ (e3 ·: x) (HDAp hd hd₁) | HDAsc ih | HDAsc ih1 = HDAsc (ds-lem-ap ih ih1)
  disjoint-sym _ (X x) (HDAp hd hd₁) = HDVar
  disjoint-sym _ (·λ x e3) (HDAp hd hd₁) with disjoint-sym _ _ hd | disjoint-sym _ _ hd₁
  disjoint-sym _ (·λ x e3) (HDAp hd hd₁) | HDLam1 ih | HDLam1 ih1 = HDLam1 (ds-lem-ap ih ih1)
  disjoint-sym _ (·λ x [ x₁ ] e3) (HDAp hd hd₁) with disjoint-sym _ _ hd | disjoint-sym _ _ hd₁
  disjoint-sym _ (·λ x [ x₁ ] e3) (HDAp hd hd₁) | HDLam2 ih | HDLam2 ih1 = HDLam2 (ds-lem-ap ih ih1)
  disjoint-sym _ ⦇⦈[ x ] (HDAp hd hd₁) with disjoint-sym _ _ hd | disjoint-sym _ _ hd₁
  disjoint-sym _ ⦇⦈[ x ] (HDAp hd hd₁) | HDHole x₁ | HDHole x₂ = HDHole (HNAp x₁ x₂)
  disjoint-sym _ ⦇⌜ e3 ⌟⦈[ x ] (HDAp hd hd₁) with disjoint-sym _ _ hd | disjoint-sym _ _ hd₁
  disjoint-sym _ ⦇⌜ e3 ⌟⦈[ x ] (HDAp hd hd₁) | HDNEHole x₁ ih | HDNEHole x₂ ih1 = HDNEHole (HNAp x₁ x₂) (ds-lem-ap ih ih1)
  disjoint-sym _ (e3 ∘ e4) (HDAp hd hd₁) with disjoint-sym _ _ hd | disjoint-sym _ _ hd₁
  disjoint-sym _ (e3 ∘ e4) (HDAp hd hd₁) | HDAp ih ih₁ | HDAp ih1 ih2 = HDAp (ds-lem-ap ih ih1) (ds-lem-ap ih₁ ih2)
  disjoint-sym _ ⟨ e2 , e3 ⟩ (HDAp hd hd₁) with disjoint-sym _ _ hd | disjoint-sym _ _ hd₁
  disjoint-sym _ ⟨ e2 , e3 ⟩ (HDAp hd hd₁) | HDPair ih ih₁ | HDPair ih1 ih2 = HDPair (ds-lem-ap ih ih1) (ds-lem-ap ih₁ ih2)
  disjoint-sym _ (fst e2) (HDAp hd hd₁) with disjoint-sym _ _ hd | disjoint-sym _ _ hd₁
  disjoint-sym _ (fst e2) (HDAp hd hd₁) | HDFst ih | HDFst ih1 = HDFst (ds-lem-ap ih ih1)
  disjoint-sym _ (snd e2) (HDAp hd hd₁) with disjoint-sym _ _ hd | disjoint-sym _ _ hd₁
  disjoint-sym _ (snd e2) (HDAp hd hd₁) | HDSnd ih | HDSnd ih1 = HDSnd (ds-lem-ap ih ih1)

  disjoint-sym _ c (HDFst hd) = HDConst
  disjoint-sym _ (e2 ·: x) (HDFst hd) with disjoint-sym _ _ hd
  disjoint-sym _ (e2 ·: x) (HDFst hd) | HDAsc ih = HDAsc (ds-lem-fst ih)
  disjoint-sym _ (X x) (HDFst hd) = HDVar
  disjoint-sym _ (·λ x e2) (HDFst hd) with disjoint-sym _ _ hd
  disjoint-sym _ (·λ x e2) (HDFst hd) | HDLam1 ih = HDLam1 (ds-lem-fst ih)
  disjoint-sym _ (·λ x [ x₁ ] e2) (HDFst hd) with disjoint-sym _ _ hd
  disjoint-sym _ (·λ x [ x₁ ] e2) (HDFst hd) | HDLam2 ih = HDLam2 (ds-lem-fst ih)
  disjoint-sym _ ⦇⦈[ x ] (HDFst hd) with disjoint-sym _ _ hd
  disjoint-sym _ ⦇⦈[ x ] (HDFst hd) | HDHole ih = HDHole (HNFst ih)
  disjoint-sym _ ⦇⌜ e2 ⌟⦈[ x ] (HDFst hd) with disjoint-sym _ _ hd
  disjoint-sym _ ⦇⌜ e2 ⌟⦈[ x ] (HDFst hd) | HDNEHole x₁ ih = HDNEHole (HNFst x₁) (ds-lem-fst ih)
  disjoint-sym _ (e2 ∘ e3) (HDFst hd) with disjoint-sym _ _ hd
  disjoint-sym _ (e2 ∘ e3) (HDFst hd) | HDAp ih ih₁ = HDAp (ds-lem-fst ih) (ds-lem-fst ih₁)
  disjoint-sym _ ⟨ e2 , e3 ⟩ (HDFst hd) with disjoint-sym _ _ hd
  disjoint-sym _ ⟨ e2 , e3 ⟩ (HDFst hd) | HDPair ih ih₁ = HDPair (ds-lem-fst ih) (ds-lem-fst ih₁)
  disjoint-sym _ (fst e2) (HDFst hd) with disjoint-sym _ _ hd
  disjoint-sym _ (fst e2) (HDFst hd) | HDFst ih = HDFst (ds-lem-fst ih)
  disjoint-sym _ (snd e2) (HDFst hd) with disjoint-sym _ _ hd
  disjoint-sym _ (snd e2) (HDFst hd) | HDSnd ih = HDSnd (ds-lem-fst ih)

  disjoint-sym _ c (HDSnd hd) = HDConst
  disjoint-sym _ (e2 ·: x) (HDSnd hd) with disjoint-sym _ _ hd
  disjoint-sym _ (e2 ·: x) (HDSnd hd) | HDAsc ih = HDAsc (ds-lem-snd ih)
  disjoint-sym _ (X x) (HDSnd hd) = HDVar
  disjoint-sym _ (·λ x e2) (HDSnd hd) with disjoint-sym _ _ hd
  disjoint-sym _ (·λ x e2) (HDSnd hd) | HDLam1 ih = HDLam1 (ds-lem-snd ih)
  disjoint-sym _ (·λ x [ x₁ ] e2) (HDSnd hd) with disjoint-sym _ _ hd
  disjoint-sym _ (·λ x [ x₁ ] e2) (HDSnd hd) | HDLam2 ih = HDLam2 (ds-lem-snd ih)
  disjoint-sym _ ⦇⦈[ x ] (HDSnd hd) with disjoint-sym _ _ hd
  disjoint-sym _ ⦇⦈[ x ] (HDSnd hd) | HDHole ih = HDHole (HNSnd ih)
  disjoint-sym _ ⦇⌜ e2 ⌟⦈[ x ] (HDSnd hd) with disjoint-sym _ _ hd
  disjoint-sym _ ⦇⌜ e2 ⌟⦈[ x ] (HDSnd hd) | HDNEHole x₁ ih = HDNEHole (HNSnd x₁) (ds-lem-snd ih)
  disjoint-sym _ (e2 ∘ e3) (HDSnd hd) with disjoint-sym _ _ hd
  disjoint-sym _ (e2 ∘ e3) (HDSnd hd) | HDAp ih ih₁ = HDAp (ds-lem-snd ih) (ds-lem-snd ih₁)
  disjoint-sym _ ⟨ e2 , e3 ⟩ (HDSnd hd) with disjoint-sym _ _ hd
  disjoint-sym _ ⟨ e2 , e3 ⟩ (HDSnd hd) | HDPair ih ih₁ = HDPair (ds-lem-snd ih) (ds-lem-snd ih₁)
  disjoint-sym _ (fst e2) (HDSnd hd) with disjoint-sym _ _ hd
  disjoint-sym _ (fst e2) (HDSnd hd) | HDFst ih = HDFst (ds-lem-snd ih)
  disjoint-sym _ (snd e2) (HDSnd hd) with disjoint-sym _ _ hd
  disjoint-sym _ (snd e2) (HDSnd hd) | HDSnd ih = HDSnd (ds-lem-snd ih)

  disjoint-sym _ c (HDPair hd hd₁) = HDConst
  disjoint-sym _ (e3 ·: x) (HDPair hd hd₁) with disjoint-sym _ _ hd | disjoint-sym _ _ hd₁
  disjoint-sym _ (e3 ·: x) (HDPair hd hd₁) | HDAsc ih | HDAsc ih1 = HDAsc (ds-lem-pair ih ih1)
  disjoint-sym _ (X x) (HDPair hd hd₁) = HDVar
  disjoint-sym _ (·λ x e3) (HDPair hd hd₁) with disjoint-sym _ _ hd | disjoint-sym _ _ hd₁
  disjoint-sym _ (·λ x e3) (HDPair hd hd₁) | HDLam1 ih | HDLam1 ih1 = HDLam1 (ds-lem-pair ih ih1)
  disjoint-sym _ (·λ x [ x₁ ] e3) (HDPair hd hd₁) with disjoint-sym _ _ hd | disjoint-sym _ _ hd₁
  disjoint-sym _ (·λ x [ x₁ ] e3) (HDPair hd hd₁) | HDLam2 ih | HDLam2 ih1 = HDLam2 (ds-lem-pair ih ih1)
  disjoint-sym _ ⦇⦈[ x ] (HDPair hd hd₁) with disjoint-sym _ _ hd | disjoint-sym _ _ hd₁
  disjoint-sym _ ⦇⦈[ x ] (HDPair hd hd₁) | HDHole x₁ | HDHole x₂ = HDHole (HNPair x₁ x₂)
  disjoint-sym _ ⦇⌜ e3 ⌟⦈[ x ] (HDPair hd hd₁) with disjoint-sym _ _ hd | disjoint-sym _ _ hd₁
  disjoint-sym _ ⦇⌜ e3 ⌟⦈[ x ] (HDPair hd hd₁) | HDNEHole x₁ ih | HDNEHole x₂ ih1 = HDNEHole (HNPair x₁ x₂) (ds-lem-pair ih ih1)
  disjoint-sym _ (e3 ∘ e4) (HDPair hd hd₁) with disjoint-sym _ _ hd | disjoint-sym _ _ hd₁
  disjoint-sym _ (e3 ∘ e4) (HDPair hd hd₁) | HDAp ih ih₁ | HDAp ih1 ih2 = HDAp (ds-lem-pair ih ih1) (ds-lem-pair ih₁ ih2)
  disjoint-sym _ ⟨ e2 , e3 ⟩ (HDPair hd hd₁) with disjoint-sym _ _ hd | disjoint-sym _ _ hd₁
  disjoint-sym _ ⟨ e2 , e3 ⟩ (HDPair hd hd₁) | HDPair ih ih₁ | HDPair ih1 ih2 = HDPair (ds-lem-pair ih ih1) (ds-lem-pair ih₁ ih2)
  disjoint-sym _ (fst e2) (HDPair hd hd₁) with disjoint-sym _ _ hd | disjoint-sym _ _ hd₁
  disjoint-sym _ (fst e2) (HDPair hd hd₁) | HDFst ih | HDFst ih1 = HDFst (ds-lem-pair ih ih1)
  disjoint-sym _ (snd e2) (HDPair hd hd₁) with disjoint-sym _ _ hd | disjoint-sym _ _ hd₁
  disjoint-sym _ (snd e2) (HDPair hd hd₁) | HDSnd ih | HDSnd ih1 = HDSnd (ds-lem-pair ih ih1)

  -- note that this is false, so holes-disjoint isn't transitive
  -- disjoint-new : ∀{e1 e2 u} → holes-disjoint e1 e2 → hole-name-new e1 u → hole-name-new e2 u

  -- it's also not reflexive, because ⦇⦈[ u ] isn't hole-disjoint with
  -- itself since refl : u == u; it's also not anti-reflexive, because the
  -- expression c *is* hole-disjoint with itself (albeit vacuously)

max_stars_repo_name: hazelgrove/hazel-palette-agda

max_issues_repo_name: hazelgrove/hazel-palette-agda

max_forks_repo_name: hazelgrove/hazelnut-livelits-agda


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Agda.ISetoids.Cocomplete.Helpers where

open import Level
open import Relation.Binary using (Setoid; module Setoid; Preorder; module Preorder; Rel; _=[_]⇒_)
open import Data.Product using (Σ; _,_; Σ-syntax)
-- import Relation.Binary.EqReasoning as EqReasoning

open import Categories.Support.Equivalence using (module I→R-Wrapper; setoid-i→r; squash) renaming (Setoid to ISetoid; module Setoid to ISetoid)
open import Categories.Support.SetoidFunctions using (module _⟶_)
open import Categories.Support.PropositionalEquality
import Categories.Support.ZigZag as ZigZag

open import Categories.Category
open import Categories.Functor
open import Categories.Agda
open import Categories.Colimit
open import Categories.Object.Initial
open import Categories.Cocones
open import Categories.Cocone

open I→R-Wrapper

ding : Level → Level
ding ℓ = ℓ

module ColimitCocone {o ℓ e c ℓ′} {J : Category o ℓ e} (F : Functor J (ISetoids (c ⊔ ding (o ⊔ ℓ ⊔ e)) (c ⊔ ℓ′ ⊔ ding (o ⊔ ℓ ⊔ e)))) where
  c′ = c ⊔ ding (o ⊔ ℓ ⊔ e)
  ℓ″ = c ⊔ ℓ′ ⊔ ding (o ⊔ ℓ ⊔ e)
  C = ISetoids c′ ℓ″
  D = Cocones F
  module J = Category J
  open Functor F
  open ISetoid
  open _⟶_

  vertex-carrier = Σ[ x ∈ J.Obj ] Carrier (F₀ x)

  -- this lets us build a preorder out of an irrelevant setoid, since there
  -- are no irrelevant preorders
  dot-setoid : (j : J.Obj) → Setoid c′ ℓ″
  dot-setoid j = setoid-i→r (F₀ j)
  module DotSetoid (j : J.Obj) = Setoid (dot-setoid j)
  open DotSetoid using () renaming (_≈_ to _[_≈_])

  -- _↝_ means that an arrow in the diagram directly constrains the two
  -- objects of vertex-carrier to be equal.  completing this to an
  -- equivalence relation gives us the setoid we need
  _↝_ : (x y : vertex-carrier) → Set ℓ″
  (X , x) ↝ (Y , y) = Σ[ f ∈ J [ X , Y ] ] (Y [ (F₁ f ⟨$⟩ x) ≈ y ])

  ↝-preorder : Preorder c′ c′ ℓ″
  ↝-preorder = record
    { Carrier = vertex-carrier
    ; _≈_ = _≣_
    ; _∼_ = _↝_
    ; isPreorder = record
      { isEquivalence = ≣-isEquivalence
      ; reflexive = ↝-reflexive
      ; trans = ↝-trans
      }
    }
    where
    ↝-refl : ∀ {i} → (i ↝ i)
    ↝-refl {X , x} = J.id , squash (identity (refl (F₀ X)))

    ↝-reflexive : ∀ {i j} → (i ≣ j) → (i ↝ j)
    ↝-reflexive ≣-refl = ↝-refl

    -- the nice proof.  pretty proof!
    {-
    ↝-trans : ∀ {i j k} → (i ↝ j) → (j ↝ k) → (i ↝ k)
    ↝-trans {_ , i} {_ , j} {k₁ , k} (f , squash fi≈j) (g , gj≈k) =
      J [ g ∘ f ] , (
        begin
          F₁ (J [ g ∘ f ]) ⟨$⟩ i
        ≈⟨ squash homomorphism ⟩
          F₁ g ⟨$⟩ (F₁ f ⟨$⟩ i)
        ≈⟨ squash (cong (F₁ g) fi≈j) ⟩
          F₁ g ⟨$⟩ j
        ≈⟨ gj≈k ⟩
          k
        ∎ )
      where
      open EqReasoning (dot-setoid k₁)
    -}

    -- the ugly proof that loads before the sun burns out.
    ↝-trans : ∀ {i j k} → (i ↝ j) → (j ↝ k) → (i ↝ k)
    ↝-trans {X , _} {k = Z , _} (f , squash fx≈y) (g , gy≈z) =
      J [ g ∘ f ] , DotSetoid.trans Z (squash (trans (F₀ Z) (homomorphism (refl (F₀ X))) (cong (F₁ g) fx≈y))) gy≈z

  vertex = ZigZag.isetoid ↝-preorder

  ⊥ : Cocone F
  ⊥ = record
    { N = vertex
    ; ψ = λ X → record
      { _⟨$⟩_ = _,_ X
      ; cong = λ pf → ZigZag.disorient (ZigZag.slish (J.id , squash (identity pf)))
    -- cong would be easier if i'd used the proper dotwise equality for
    -- ↝-preorder above ... since this is basically the proof ↝ respects it
    }
    ; commute = λ {X Y} f {x : _} {y : _} (x≈y : _) → ZigZag.disorient (ZigZag.slish (f , (squash (cong (F₁ f) x≈y))))
    }

  ! : {A : Cocone F} → CoconeMorphism {F = F} ⊥ A
  ! {A} = record
    { f = record
      { _⟨$⟩_ = my-f
      ; cong = ZigZag.iminimal ↝-preorder A.N my-f my-precong
      }
    ; commute = λ {X x y} x≈y → cong (A.ψ X) x≈y
    }
    where
    module A = Cocone A
    my-f : vertex-carrier → Carrier A.N
    my-f (X , x) = A.ψ X ⟨$⟩ x

    .my-precong : _↝_ =[ my-f ]⇒ (_≈_ A.N)
    my-precong {X , x} {Y , y} (f , squash fx≈y) = trans A.N (A.commute f (refl (F₀ X))) (cong (A.ψ Y) (irr fx≈y))

ext: agda

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
{-# OPTIONS --without-K #-}

open import HoTT
open import homotopy.JoinComm
open import homotopy.JoinAssocCubical

module homotopy.JoinSusp where

module _ {i} {A : Type i} where

  private

      module Into = JoinRec {A = Bool} {B = A}
        {D = Suspension A}
        (if_then north else south)
        (λ _ → south)
        (λ {(true , a) → merid a;
            (false , a) → idp})

      into = Into.f

      module Out = SuspensionRec {C = Bool * A}
        (left true)
        (left false)
        (λ a → glue (true , a) ∙ ! (glue (false , a)))

      out = Out.f

      into-out : ∀ σ → into (out σ) == σ
      into-out = Suspension-elim
        idp
        idp
        (↓-∘=idf-from-square into out ∘ λ a → vert-degen-square $
           ap (ap into) (Out.merid-β a)
           ∙ ap-∙ into (glue (true , a)) (! (glue (false , a)))
           ∙ (Into.glue-β (true , a)
              ∙2 (ap-! into (glue (false , a))
                  ∙ ap ! (Into.glue-β (false , a))))
           ∙ ∙-unit-r _)

      out-into : ∀ j → out (into j) == j
      out-into = Join-elim
        (λ{true → idp ; false → idp})
        (λ a → glue (false , a))
        (↓-∘=idf-from-square out into ∘
          λ {(true , a) →
                (ap (ap out) (Into.glue-β (true , a)) ∙ Out.merid-β a)
                ∙v⊡ (vid-square {p = glue (true , a)}
                      ⊡h rt-square (glue (false , a)))
                ⊡v∙ ∙-unit-r _;
             (false , a) →
               ap (ap out) (Into.glue-β (false , a)) ∙v⊡ connection})

  *-Bool-equiv-Suspension : Bool * A ≃ Suspension A
  *-Bool-equiv-Suspension = equiv into out into-out out-into

  *-Lift-Bool-equiv-Suspension : Lift {j = i} Bool * A ≃ Suspension A
  *-Lift-Bool-equiv-Suspension = *-Bool-equiv-Suspension ∘e equiv-* lower-equiv (ide A)

  *-Bool = ua *-Bool-equiv-Suspension

module _ {i} (X : Ptd i) where

  ⊙*-⊙Bool : ⊙Bool ⊙* X == ⊙Susp X
  ⊙*-⊙Bool = ⊙ua (⊙≃-in *-Bool-equiv-Suspension idp)

  ⊙*-⊙Lift-⊙Bool : ⊙Lift {j = i} ⊙Bool ⊙* X == ⊙Susp X
  ⊙*-⊙Lift-⊙Bool = ⊙ua (⊙≃-in *-Lift-Bool-equiv-Suspension idp)

module _ {i j} {A : Type i} {B : Type j} where

  *-Suspension : Suspension A * B == Suspension (A * B)
  *-Suspension =
    ap (_* B) (! *-Bool)
    ∙ join-rearrange-path
    ∙ ua swap-equiv
    ∙ *-Bool
    ∙ ap Suspension (ua swap-equiv)

module _ {i j} (X : Ptd i) (Y : Ptd j) where

  ⊙*-⊙Susp : ⊙Susp X ⊙* Y == ⊙Susp (X ⊙* Y)
  ⊙*-⊙Susp =
    ap (_⊙* Y) (! (⊙*-⊙Bool X))
    ∙ join-rearrange-⊙path (⊙Sphere 0) X Y
    ∙ ⊙ua (⊙≃-in swap-equiv (! (glue _)))
    ∙ ⊙*-⊙Bool (Y ⊙* X)
    ∙ ap (λ A → (Suspension A , north)) (ua swap-equiv)

module _ {i} where

  ⊙*-⊙Sphere : (m : ℕ) (X : Ptd i) → ⊙Sphere m ⊙* X == ⊙Susp^ (S m) X
  ⊙*-⊙Sphere O X = ⊙*-⊙Bool X
  ⊙*-⊙Sphere (S m) X = ⊙*-⊙Susp (⊙Sphere m) X
                     ∙ ap ⊙Susp (⊙*-⊙Sphere m X)

  ⊙*-⊙Lift-⊙Sphere : (m : ℕ) (X : Ptd i) → ⊙Lift {j = i} (⊙Sphere m) ⊙* X == ⊙Susp^ (S m) X
  ⊙*-⊙Lift-⊙Sphere O X = ⊙*-⊙Lift-⊙Bool X
  ⊙*-⊙Lift-⊙Sphere (S m) X = ap (_⊙* X) (! $ ⊙Susp-⊙Lift (⊙Sphere m))
                           ∙ ⊙*-⊙Susp (⊙Lift (⊙Sphere m)) X
                           ∙ ap ⊙Susp (⊙*-⊙Lift-⊙Sphere m X)

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
{-# OPTIONS --safe --warning=error --without-K --guardedness #-}

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Setoids.Setoids
open import Rings.Definition
open import Rings.Orders.Partial.Definition
open import Rings.Orders.Total.Definition
open import Groups.Definition
open import Groups.Lemmas
open import Fields.Fields
open import Sets.EquivalenceRelations
open import Sequences
open import Setoids.Orders.Partial.Definition
open import Setoids.Orders.Total.Definition
open import Functions.Definition
open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Numbers.Naturals.Order.Lemmas
open import Semirings.Definition

module Fields.CauchyCompletion.Comparison {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) where

open Setoid S
open SetoidTotalOrder (TotallyOrderedRing.total order)
open SetoidPartialOrder pOrder
open Equivalence eq
open PartiallyOrderedRing pRing
open Ring R
open Group additiveGroup
open Field F
open import Fields.Orders.Lemmas {F = F} {pRing} (record { oRing = order })

open import Rings.Orders.Partial.Lemmas pRing
open import Rings.Orders.Total.Lemmas order
open import Rings.Orders.Total.AbsoluteValue order
open import Fields.Lemmas F
open import Fields.CauchyCompletion.Definition order F
open import Fields.CauchyCompletion.Setoid order F
open import Fields.CauchyCompletion.Group order F
open import Fields.Orders.Total.Lemmas {F = F} (record { oRing = order })

-- "<C rational", where the r indicates where the rational number goes
record _<Cr_ (a : CauchyCompletion) (b : A) : Set (m ⊔ o) where
  field
    e : A
    0<e : 0G < e
    N : ℕ
    property : ((m : ℕ) → (N<m : N <N m) → (e + index (CauchyCompletion.elts a) m) < b)

<CrWellDefinedRight : (a : CauchyCompletion) (b c : A) → b ∼ c → a <Cr b → a <Cr c
<CrWellDefinedRight a b c b=c record { e = ε ; 0<e = 0<e ; N = N ; property = pr } = record { e = ε ; 0<e = 0<e ; N = N ; property = λ m N<m → <WellDefined (Equivalence.reflexive eq) b=c (pr m N<m) }

private
  <CrWellDefinedLemma : (a b e/2 e : A) (0<e : 0G < e) (pr : e/2 + e/2 ∼ e) → abs (a + inverse b) < e/2 → (e/2 + b) < (e + a)
  <CrWellDefinedLemma a b e/2 e 0<e pr a-b<e with totality 0G (a + inverse b)
  <CrWellDefinedLemma a b e/2 e 0<e pr a-b<e | inl (inl 0<a-b) = ringAddInequalities (halfLess e/2 e 0<e pr) (<WellDefined identLeft (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) invLeft) identRight)) (orderRespectsAddition 0<a-b b))
  <CrWellDefinedLemma a b e/2 e 0<e pr a-b<e | inl (inr a-b<0) = <WellDefined (Equivalence.transitive eq (+WellDefined (invContravariant (Ring.additiveGroup R)) groupIsAbelian) (Equivalence.transitive eq (Equivalence.transitive eq +Associative (+WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (Equivalence.transitive eq (+WellDefined (invTwice additiveGroup b) invLeft) identRight)) (Equivalence.reflexive eq))) groupIsAbelian)) (Equivalence.transitive eq +Associative (+WellDefined pr (Equivalence.reflexive eq))) (orderRespectsAddition a-b<e (e/2 + a))
  <CrWellDefinedLemma a b e/2 e 0<e pr a-b<e | inr 0=a-b = <WellDefined (Equivalence.reflexive eq) (+WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq (transferToRight (Ring.additiveGroup R) (Equivalence.symmetric eq 0=a-b)))) (orderRespectsAddition (halfLess e/2 e 0<e pr) b)

<CrWellDefinedLeft : (a b : CauchyCompletion) (c : A) → Setoid._∼_ cauchyCompletionSetoid a b → a <Cr c → b <Cr c
<CrWellDefinedLeft a b c a=b record { e = ε ; 0<e = 0<e ; N = N ; property = pr } with halve charNot2 ε
... | e/2 , prE/2 with halvePositive e/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/2) 0<e)
... | 0<e/2 with a=b e/2 0<e/2
... | N2 , prN2 = record { e = e/2 ; 0<e = 0<e/2 ; N = N +N N2 ; property = ans }
  where
    ans : (m : ℕ) → (N<m : (N +N N2) <N m) → (e/2 + index (CauchyCompletion.elts b) m) < c
    ans m N<m with prN2 {m} (inequalityShrinkRight N<m)
    ... | bl rewrite indexAndApply (CauchyCompletion.elts a) (map inverse (CauchyCompletion.elts b)) _+_ {m} | equalityCommutative (mapAndIndex (CauchyCompletion.elts b) inverse m) = SetoidPartialOrder.<Transitive pOrder (<CrWellDefinedLemma (index (CauchyCompletion.elts a) m) (index (CauchyCompletion.elts b) m) e/2 ε 0<e prE/2 bl) (pr m (inequalityShrinkLeft N<m))

<CrWellDefined : (a b : CauchyCompletion) (c d : A) → Setoid._∼_ cauchyCompletionSetoid a b → c ∼ d → a <Cr c → b <Cr d
<CrWellDefined a b c d a=b c=d a<c = <CrWellDefinedLeft a b d a=b (<CrWellDefinedRight a c d c=d a<c)

record _r<C_ (a : A) (b : CauchyCompletion) : Set (m ⊔ o) where
  field
    e : A
    0<e : 0G < e
    N : ℕ
    pr : (m : ℕ) → (N<m : N <N m) → (a + e) < index (CauchyCompletion.elts b) m

r<CWellDefinedLeft : (a b : A) (c : CauchyCompletion) → (a ∼ b) → (a r<C c) → b r<C c
r<CWellDefinedLeft a b c a=b record { e = e ; 0<e = 0<e ; N = N ; pr = pr } = record { e = e ; 0<e = 0<e ; N = N ; pr =  λ m N<m → <WellDefined (+WellDefined a=b (Equivalence.reflexive eq)) (Equivalence.reflexive eq) (pr m N<m) }

private
  r<CWellDefinedLemma : (a b c e e/2 : A) (_ : e/2 + e/2 ∼ e) (0<e : 0G < e) (_ : abs (a + inverse b) < e/2) (_ : (c + e) < a) → (c + e/2) < b
  r<CWellDefinedLemma a b c e e/2 prE/2 0<e pr c+e<a with totality 0G (a + inverse b)
  r<CWellDefinedLemma a b c e e/2 prE/2 0<e pr c+e<a | inl (inl 0<a-b) = SetoidPartialOrder.<Transitive pOrder (<WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (+WellDefined (Equivalence.symmetric eq prE/2) (Equivalence.reflexive eq)) (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) invRight)) identRight)))) (Equivalence.reflexive eq) (orderRespectsAddition c+e<a (inverse e/2))) (<WellDefined (Equivalence.transitive eq +Associative (+WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) invLeft) identRight)) (Equivalence.reflexive eq))) (Equivalence.transitive eq groupIsAbelian (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) (invLeft)) identRight))) (orderRespectsAddition pr (b + inverse e/2)))
  r<CWellDefinedLemma a b c e e/2 prE/2 0<e pr c+e<a | inl (inr a-b<0) = SetoidPartialOrder.<Transitive pOrder (SetoidPartialOrder.<Transitive pOrder (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (halfLess e/2 e 0<e prE/2) c)) c+e<a) (<WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) invLeft)) identRight) identLeft (orderRespectsAddition a-b<0 b))
  r<CWellDefinedLemma a b c e e/2 prE/2 0<e pr c+e<a | inr 0=a-b = SetoidPartialOrder.<Transitive pOrder (<WellDefined groupIsAbelian (Equivalence.reflexive eq) (orderRespectsAddition (halfLess e/2 e 0<e prE/2) c)) (<WellDefined (groupIsAbelian {c} {e}) (transferToRight additiveGroup (Equivalence.symmetric eq 0=a-b)) c+e<a)

r<CWellDefinedRight : (a b : CauchyCompletion) (c : A) → Setoid._∼_ cauchyCompletionSetoid a b → c r<C a → c r<C b
r<CWellDefinedRight a b c a=b record { e = e ; 0<e = 0<e ; N = N ; pr = pr } with halve charNot2 e
... | e/2 , prE/2 with halvePositive e/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/2) 0<e)
... | 0<e/2 with a=b e/2 0<e/2
... | N2 , prN2 = record { e = e/2 ; 0<e = 0<e/2 ; N = N +N N2 ; pr = ans }
  where
    ans : (m : ℕ) → (N<m : (N +N N2) <N m) → (c + e/2) < index (CauchyCompletion.elts b) m
    ans m N<m with prN2 {m} (inequalityShrinkRight N<m)
    ... | bl rewrite indexAndApply (CauchyCompletion.elts a) (map inverse (CauchyCompletion.elts b)) _+_ {m} | equalityCommutative (mapAndIndex (CauchyCompletion.elts b) inverse m) = r<CWellDefinedLemma (index (CauchyCompletion.elts a) m) (index (CauchyCompletion.elts b) m) c e e/2 prE/2 0<e bl (pr m (inequalityShrinkLeft N<m))

record _<C_ (a : CauchyCompletion) (b : CauchyCompletion) : Set (m ⊔ o) where
  field
    i : A
    a<i : a <Cr i
    i<b : i r<C b

<CWellDefined : {a b c d : CauchyCompletion} → Setoid._∼_ cauchyCompletionSetoid a b → Setoid._∼_ cauchyCompletionSetoid c d → a <C c → b <C d
<CWellDefined {a} {b} {c} {d} a=b c=d record { i = bound ; a<i = a<bound ; i<b = bound<b } = record { i = bound ; a<i = <CrWellDefinedLeft a b bound a=b a<bound ; i<b = r<CWellDefinedRight c d bound c=d bound<b }

<CInheritedL : {a b : A} → a < b → injection a <Cr b
<CInheritedL {a} {b} a<b with dense charNot2 a<b
... | between , (a<between ,, between<b) = record { e = between + inverse a ; 0<e = <WellDefined invRight (Equivalence.reflexive eq) (orderRespectsAddition a<between (inverse a)) ; N = 0 ; property = λ m _ → <WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq identRight) (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) (ans a m)) +Associative)) (Equivalence.reflexive eq) between<b }
  where
    ans : (x : A) (m : ℕ) → 0G ∼ inverse x + index (constSequence x) m
    ans x m rewrite indexAndConst x m = Equivalence.symmetric eq invLeft

<CInheritedR : {a b : A} → a < b → a r<C injection b
<CInheritedR {a} {b} a<b with dense charNot2 a<b
... | between , (a<between ,, between<b) = record { e = between + inverse a ; 0<e = <WellDefined invRight (Equivalence.reflexive eq) (orderRespectsAddition a<between (inverse a)) ; N = 0 ; pr = λ m _ → <WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq identRight) (+WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq invLeft))) +Associative) groupIsAbelian) (identityOfIndiscernablesLeft _∼_ (Equivalence.reflexive eq) (indexAndConst b m)) between<b }

<CInherited : {a b : A} → a < b → (injection a) <C (injection b)
<CInherited {a} {b} a<b with dense charNot2 a<b
... | between , (a<between ,, between<b) = record { i = between ; a<i = <CInheritedL a<between ; i<b = <CInheritedR between<b }

<CCollapsesL : (a b : A) → (injection a) <Cr b → a < b
<CCollapsesL a b record { e = e ; 0<e = 0<i ; N = N ; property = pr } with pr (succ N) (le 0 refl)
... | bl rewrite indexAndConst a N = <Transitive (<WellDefined identLeft reflexive (orderRespectsAddition 0<i a)) bl

<CCollapsesR : (a b : A) → a r<C injection b → a < b
<CCollapsesR a b record { e = e ; 0<e = 0<e ; N = N ; pr = pr } with pr (succ N) (le 0 refl)
... | bl rewrite indexAndConst b N = <Transitive (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<e a)) bl

<CCollapses : {a b : A} → (injection a) <C (injection b) → a < b
<CCollapses {a} {b} record { i = inter ; a<i = pr1 ; i<b = pr2 } = <Transitive (<CCollapsesL a inter pr1) (<CCollapsesR inter b pr2)

<CRelaxL : {a : A} {b : CauchyCompletion} → a r<C b → injection a <C b
<CRelaxL {a} {b} record { e = e ; 0<e = 0<e ; N = N ; pr = pr } with halve charNot2 e
... | e/2 , e/2pr = record { i = a + e/2 ; a<i = <CInheritedL (<WellDefined identLeft groupIsAbelian (orderRespectsAddition (halvePositive' e/2pr 0<e) a)) ; i<b = record { e = e/2 ; 0<e = halvePositive' e/2pr 0<e ; N = N ; pr = λ m N<m → <WellDefined (transitive (+WellDefined reflexive (symmetric e/2pr)) +Associative) reflexive (pr m N<m) } }

<CRelaxL' : {a : A} {b : CauchyCompletion} → injection a <C b → a r<C b
<CRelaxL' {a} {b} record { i = i ; a<i = a<i ; i<b = record { e = e ; 0<e = 0<e ; N = N ; pr = pr } } = record { e = e ; 0<e = 0<e ; N = N ; pr = λ m N<m → <Transitive (orderRespectsAddition (<CCollapsesL _ _ a<i) e) (pr m N<m) }

<CRelaxR : {a : CauchyCompletion} {b : A} → a <Cr b → a <C injection b
<CRelaxR {a} {b} record { e = ε ; 0<e = 0<ε ; N = N ; property = property } with halve charNot2 ε
... | e/2 , e/2+e/2=e = record { i = b + inverse e/2 ; a<i = record { e = e/2 ; 0<e = halvePositive' e/2+e/2=e 0<ε ; N = N ; property = λ m N<m → <WellDefined (transitive groupIsAbelian (transitive +Associative (+WellDefined (transitive (+WellDefined reflexive (symmetric e/2+e/2=e)) (transitive +Associative (transitive (+WellDefined invLeft reflexive) identLeft))) reflexive))) reflexive (orderRespectsAddition (property m N<m) (inverse e/2)) } ; i<b = <CInheritedR (<WellDefined groupIsAbelian identLeft (orderRespectsAddition (<WellDefined reflexive (invIdent additiveGroup) (ringSwapNegatives (<WellDefined (symmetric (invTwice additiveGroup 0R)) (symmetric (invTwice additiveGroup e/2)) (halvePositive' e/2+e/2=e 0<ε)))) b)) }

<CRelaxR' : {a : CauchyCompletion} {b : A} → a <C injection b → a <Cr b
<CRelaxR' {a} {b} record { i = i ; a<i = record { e = ε ; 0<e = 0<ε ; N = N ; property = property } ; i<b = i<b } = record { e = ε ; 0<e = 0<ε ; N = N ; property = λ m N<m → <Transitive (property m N<m) (<CCollapsesR _ _ i<b) }

flip<CR : {a : CauchyCompletion} {b : A} → a <Cr b → inverse b r<C Group.inverse CGroup a
_r<C_.e (flip<CR {a} {b} record { e = e ; 0<e = 0<e ; N = N ; property = property }) = e
_r<C_.0<e (flip<CR {a} {b} record { e = e ; 0<e = 0<e ; N = N ; property = property }) = 0<e
_r<C_.N (flip<CR {a} {b} record { e = e ; 0<e = 0<e ; N = N ; property = property }) = N
_r<C_.pr (flip<CR {a} {b} record { e = e ; 0<e = 0<e ; N = N ; property = property }) m N<m with property m N<m
... | bl = <WellDefined (transitive (transitive (symmetric +Associative) (+WellDefined reflexive (transitive groupIsAbelian (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invLeft) identRight))))) groupIsAbelian) (transitive +Associative (transitive (+WellDefined invRight reflexive) (transitive identLeft (identityOfIndiscernablesRight _∼_ reflexive (mapAndIndex (CauchyCompletion.elts a) inverse m))))) (orderRespectsAddition bl (inverse b + inverse (index (CauchyCompletion.elts a) m)))

flipR<C : {a : A} {b : CauchyCompletion} → a r<C b → Group.inverse CGroup b <Cr inverse a
_<Cr_.e (flipR<C record { e = e ; 0<e = 0<e ; N = N ; pr = pr }) = e
_<Cr_.0<e (flipR<C record { e = e ; 0<e = 0<e ; N = N ; pr = pr }) = 0<e
_<Cr_.N (flipR<C record { e = e ; 0<e = 0<e ; N = N ; pr = pr }) = N
_<Cr_.property (flipR<C {a} {b} record { e = e ; 0<e = 0<e ; N = N ; pr = pr }) m N<m with pr m N<m
... | t = <WellDefined (transitive (+WellDefined groupIsAbelian (+WellDefined reflexive (identityOfIndiscernablesRight _∼_ reflexive (mapAndIndex (CauchyCompletion.elts b) inverse m)))) (transitive (symmetric +Associative) (+WellDefined reflexive (transitive +Associative (transitive (+WellDefined invRight reflexive) identLeft))))) (transitive groupIsAbelian (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invLeft) identRight))) (orderRespectsAddition t (inverse a + inverse (index (CauchyCompletion.elts b) m)))

flip<C : {a b : CauchyCompletion} → a <C b → Group.inverse CGroup b <C Group.inverse CGroup a
flip<C {a} {b} record { i = i ; a<i = a<i ; i<b = i<b } = record { i = inverse i ; a<i = flipR<C i<b ; i<b = flip<CR a<i }

flip<C' : {a b : CauchyCompletion} → Group.inverse CGroup b <C Group.inverse CGroup a → a <C b
flip<C' {a} {b} a<b = <CWellDefined (invTwice CGroup a) (invTwice CGroup b) (flip<C a<b)

<CIrreflexive : {a : CauchyCompletion} → a <C a → False
<CIrreflexive {a} record { i = bound ; a<i = record { e = bA ; 0<e = 0<bA ; N = Na ; property = prA } ; i<b = record { e = bB ; 0<e = 0<bB ; N = Nb ; pr = prB } } with prA (succ Na +N Nb) (le Nb (applyEquality succ (Semiring.commutative ℕSemiring Nb Na)))
... | bl with prB (succ Na +N Nb) (le Na refl)
... | bl2 with <WellDefined (Equivalence.transitive eq +Associative (+WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) groupIsAbelian) (Equivalence.reflexive eq))) groupIsAbelian (ringAddInequalities bl bl2)
... | bad = irreflexive (SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft +Associative (<WellDefined (Equivalence.reflexive eq) groupIsAbelian (orderRespectsAddition (<WellDefined identLeft (Equivalence.reflexive eq) (ringAddInequalities 0<bA 0<bB)) (index (CauchyCompletion.elts a) (succ Na +N Nb) + bound)))) bad)

<CTransitive : {a b c : CauchyCompletion} → a <C b → b <C c → a <C c
<CTransitive {a} {b} {c} record { i = boundA ; a<i = record { e = eL ; 0<e = 0<eL ; N = NL ; property = prL } ; i<b = record { e = eR ; 0<e = 0<eR ; N = Nr ; pr = prR } } record { i = boundB ; a<i = record { e = fL ; 0<e = 0<fL ; N = Nfl ; property = prFl } ; i<b = record { e = fR ; 0<e = 0<fR ; N = N ; pr = prFR } } = record { i = boundA ; a<i = record { e = eL ; 0<e = 0<eL ; N = NL ; property = prL } ; i<b = record { e = eR ; 0<e = 0<eR ; N = (Nr +N Nfl) +N N ; pr = λ m N<m → SetoidPartialOrder.<Transitive pOrder (SetoidPartialOrder.<Transitive pOrder (SetoidPartialOrder.<Transitive pOrder (SetoidPartialOrder.<Transitive pOrder (prR m (inequalityShrinkLeft {Nr} (inequalityShrinkLeft N<m))) (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<fL (index (CauchyCompletion.elts b) m)))) (prFl m (inequalityShrinkRight {Nr} (inequalityShrinkLeft N<m)))) (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<fR boundB))) (prFR m (inequalityShrinkRight N<m)) } }

<COrder : SetoidPartialOrder cauchyCompletionSetoid _<C_
SetoidPartialOrder.<WellDefined <COrder {a} {b} {c} {d} a=b c=d a<c = <CWellDefined {a} {b} {c} {d} a=b c=d a<c
SetoidPartialOrder.irreflexive <COrder {a} a<a = <CIrreflexive {a} a<a
SetoidPartialOrder.<Transitive <COrder {a} {b} {c} a<b b<c = <CTransitive {a} {b} {c} a<b b<c


text:
{-# OPTIONS --without-K --safe #-}

open import Categories.Category

module Categories.Morphism.Duality {o ℓ e} (C : Category o ℓ e) where

open Category C

import Categories.Morphism as M
private
  module Op = M op
open M C

open import Categories.Morphism.Properties C

private
  variable
    A B X Y : Obj
    f g h : A ⇒ B

Mono⇒op-Epi : Mono f → Op.Epi f
Mono⇒op-Epi mono = mono

Epi⇒op-Mono : Epi f → Op.Mono f
Epi⇒op-Mono epi = epi

Iso⇒op-Iso : Iso f g → Op.Iso g f
Iso⇒op-Iso iso = record
  { isoˡ = isoˡ
  ; isoʳ = isoʳ
  }
  where open Iso iso

op-Iso⇒Iso : Op.Iso g f → Iso f g
op-Iso⇒Iso iso = record
  { isoˡ = isoˡ
  ; isoʳ = isoʳ
  }
  where open Op.Iso iso

≅⇒op-≅ : A ≅ B → A Op.≅ B
≅⇒op-≅ A≅B = record
  { from = to
  ; to   = from
  ; iso  = record -- I don't understand why Agda doesn't allow me to apply Iso⇒op-Iso
    { isoˡ = isoˡ
    ; isoʳ = isoʳ
    }
  }
  where open _≅_ A≅B

op-≅⇒≅ : A Op.≅ B → A ≅ B
op-≅⇒≅ A≅B = record
  { from = to
  ; to   = from
  ; iso  = record
    { isoˡ = isoˡ
    ; isoʳ = isoʳ
    }
  }
  where open Op._≅_ A≅B

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
-- Andreas, 2012-10-02
-- {-# OPTIONS -v tc.conv.level:100 -v tc.constr.add:40 -v tc.meta:50 -v tc.inj.use:30 -v 80 #-}
module Issue689 where

open import Common.Level

data Bad : Set₁ where
  c : Set₁ → Bad

-- this should not leave unsolvable constraints, but report an error

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The sequential colimit HIT with an erased higher constructor
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --safe #-}

-- The definition of sequential colimits and the statement of the
-- non-dependent universal property are based on those in van Doorn's
-- "Constructing the Propositional Truncation using Non-recursive
-- HITs".

-- The module is parametrised by a notion of equality. The higher
-- constructor of the HIT defining sequential colimits uses path
-- equality, but the supplied notion of equality is used for many
-- other things.

import Equality.Path as P

module Colimit.Sequential.Erased
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq hiding (elim)

open import Prelude

open import Bijection equality-with-J using (_↔_)
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq using (_≃_)
open import Erased.Cubical eq

private
  variable
    a b p q : Level
    A B     : Type a
    P       : A → Type p
    n       : ℕ
    e x     : A

------------------------------------------------------------------------
-- The type

-- Sequential colimits, with an erased higher constructor.

data Colimitᴱ (P : ℕ → Type p) (@0 step : ∀ {n} → P n → P (suc n)) :
             Type p where
  ∣_∣       : P n → Colimitᴱ P step
  @0 ∣∣≡∣∣ᴾ : (x : P n) → ∣ step x ∣ P.≡ ∣ x ∣

-- A variant of ∣∣≡∣∣ᴾ.

@0 ∣∣≡∣∣ :
  {step : ∀ {n} → P n → P (suc n)} (x : P n) →
  _≡_ {A = Colimitᴱ P step} ∣ step x ∣ ∣ x ∣
∣∣≡∣∣ x = _↔_.from ≡↔≡ (∣∣≡∣∣ᴾ x)

------------------------------------------------------------------------
-- Eliminators

-- A dependent eliminator, expressed using paths.

record Elimᴾ
         {P : ℕ → Type p} {@0 step : ∀ {n} → P n → P (suc n)}
         (Q : Colimitᴱ P step → Type q) : Type (p ⊔ q) where
  no-eta-equality
  field
    ∣∣ʳ       : (x : P n) → Q ∣ x ∣
    @0 ∣∣≡∣∣ʳ :
      (x : P n) →
      P.[ (λ i → Q (∣∣≡∣∣ᴾ x i)) ] ∣∣ʳ (step x) ≡ ∣∣ʳ x

open Elimᴾ public

elimᴾ :
  {@0 step : ∀ {n} → P n → P (suc n)} {Q : Colimitᴱ P step → Type q} →
  Elimᴾ Q → (x : Colimitᴱ P step) → Q x
elimᴾ {P = P} {step = step} {Q = Q} e = helper
  where
  module E = Elimᴾ e

  helper : (x : Colimitᴱ P step) → Q x
  helper ∣ x ∣        = E.∣∣ʳ x
  helper (∣∣≡∣∣ᴾ x i) = E.∣∣≡∣∣ʳ x i

-- A non-dependent eliminator, expressed using paths.

record Recᴾ
         (P : ℕ → Type p) (@0 step : ∀ {n} → P n → P (suc n))
         (B : Type b) : Type (p ⊔ b) where
  no-eta-equality
  field
    ∣∣ʳ       : P n → B
    @0 ∣∣≡∣∣ʳ : (x : P n) → ∣∣ʳ (step x) P.≡ ∣∣ʳ x

open Recᴾ public

recᴾ :
  {@0 step : ∀ {n} → P n → P (suc n)} →
  Recᴾ P step B → Colimitᴱ P step → B
recᴾ r = elimᴾ λ where
    .∣∣ʳ    → R.∣∣ʳ
    .∣∣≡∣∣ʳ → R.∣∣≡∣∣ʳ
  where
  module R = Recᴾ r

-- A dependent eliminator.

record Elim
         {P : ℕ → Type p} {@0 step : ∀ {n} → P n → P (suc n)}
         (Q : Colimitᴱ P step → Type q) : Type (p ⊔ q) where
  no-eta-equality
  field
    ∣∣ʳ       : (x : P n) → Q ∣ x ∣
    @0 ∣∣≡∣∣ʳ : (x : P n) → subst Q (∣∣≡∣∣ x) (∣∣ʳ (step x)) ≡ ∣∣ʳ x

open Elim public

elim :
  {@0 step : ∀ {n} → P n → P (suc n)} {Q : Colimitᴱ P step → Type q} →
  Elim Q → (x : Colimitᴱ P step) → Q x
elim e = elimᴾ λ where
    .∣∣ʳ      → E.∣∣ʳ
    .∣∣≡∣∣ʳ x → subst≡→[]≡ (E.∣∣≡∣∣ʳ x)
  where
  module E = Elim e

-- A "computation" rule.

@0 elim-∣∣≡∣∣ : dcong (elim e) (∣∣≡∣∣ x) ≡ Elim.∣∣≡∣∣ʳ e x
elim-∣∣≡∣∣ = dcong-subst≡→[]≡ (refl _)

-- A non-dependent eliminator.

record Rec
         (P : ℕ → Type p) (@0 step : ∀ {n} → P n → P (suc n))
         (B : Type b) : Type (p ⊔ b) where
  no-eta-equality
  field
    ∣∣ʳ    : P n → B
    @0 ∣∣≡∣∣ʳ : (x : P n) → ∣∣ʳ (step x) ≡ ∣∣ʳ x

open Rec public

rec :
  {@0 step : ∀ {n} → P n → P (suc n)} →
  Rec P step B → Colimitᴱ P step → B
rec r = recᴾ λ where
    .∣∣ʳ      → R.∣∣ʳ
    .∣∣≡∣∣ʳ x → _↔_.to ≡↔≡ (R.∣∣≡∣∣ʳ x)
  where
  module R = Rec r

-- A "computation" rule.

@0 rec-∣∣≡∣∣ :
  {step : ∀ {n} → P n → P (suc n)} {r : Rec P step B} {x : P n} →
  cong (rec r) (∣∣≡∣∣ x) ≡ Rec.∣∣≡∣∣ʳ r x
rec-∣∣≡∣∣ = cong-≡↔≡ (refl _)

------------------------------------------------------------------------
-- The universal property

-- The universal property of the sequential colimit.

universal-property :
  {@0 step : ∀ {n} → P n → P (suc n)} →
  (Colimitᴱ P step → B) ≃
  (∃ λ (f : ∀ n → P n → B) →
     Erased (∀ n x → f (suc n) (step x) ≡ f n x))
universal-property {P = P} {B = B} {step = step} =
  Eq.↔→≃ to from to∘from from∘to
  where
  to :
    (Colimitᴱ P step → B) →
    ∃ λ (f : ∀ n → P n → B) →
      Erased (∀ n x → f (suc n) (step x) ≡ f n x)
  to h = (λ _ → h ∘ ∣_∣)
       , [ (λ _ x →
              h ∣ step x ∣  ≡⟨ cong h (∣∣≡∣∣ x) ⟩∎
              h ∣ x ∣       ∎)
         ]

  from :
    (∃ λ (f : ∀ n → P n → B) →
       Erased (∀ n x → f (suc n) (step x) ≡ f n x)) →
    Colimitᴱ P step → B
  from (f , g) = rec λ where
    .∣∣ʳ    → f _
    .∣∣≡∣∣ʳ → erased g _

  to∘from : ∀ p → to (from p) ≡ p
  to∘from (f , g) =
    cong (f ,_) $
    []-cong
      [ (⟨ext⟩ λ n → ⟨ext⟩ λ x →
           cong (rec _) (∣∣≡∣∣ x)  ≡⟨ rec-∣∣≡∣∣ ⟩∎
           erased g n x            ∎)
      ]

  from∘to : ∀ h → from (to h) ≡ h
  from∘to h = ⟨ext⟩ $ elim λ where
    .∣∣ʳ _    → refl _
    .∣∣≡∣∣ʳ x →
      subst (λ z → from (to h) z ≡ h z) (∣∣≡∣∣ x) (refl _)  ≡⟨ subst-in-terms-of-trans-and-cong ⟩

      trans (sym (cong (from (to h)) (∣∣≡∣∣ x)))
        (trans (refl _) (cong h (∣∣≡∣∣ x)))                 ≡⟨ cong₂ (λ p q → trans (sym p) q)
                                                                 rec-∣∣≡∣∣
                                                                 (trans-reflˡ _) ⟩

      trans (sym (cong h (∣∣≡∣∣ x))) (cong h (∣∣≡∣∣ x))     ≡⟨ trans-symˡ _ ⟩∎

      refl _                                                ∎

-- A dependently typed variant of the sequential colimit's universal
-- property.

universal-property-Π :
  {@0 step : ∀ {n} → P n → P (suc n)} →
  {Q : Colimitᴱ P step → Type q} →
  ((x : Colimitᴱ P step) → Q x) ≃
  (∃ λ (f : ∀ n (x : P n) → Q ∣ x ∣) →
     Erased (∀ n x → subst Q (∣∣≡∣∣ x) (f (suc n) (step x)) ≡ f n x))
universal-property-Π {P = P} {step = step} {Q = Q} =
  Eq.↔→≃ to from to∘from from∘to
  where
  to :
    ((x : Colimitᴱ P step) → Q x) →
    ∃ λ (f : ∀ n (x : P n) → Q ∣ x ∣) →
      Erased (∀ n x → subst Q (∣∣≡∣∣ x) (f (suc n) (step x)) ≡ f n x)
  to h = (λ _ → h ∘ ∣_∣)
       , [ (λ _ x →
              subst Q (∣∣≡∣∣ x) (h ∣ step x ∣)  ≡⟨ dcong h (∣∣≡∣∣ x) ⟩∎
              h ∣ x ∣                           ∎)
         ]

  from :
    (∃ λ (f : ∀ n (x : P n) → Q ∣ x ∣) →
       Erased (∀ n x →
               subst Q (∣∣≡∣∣ x) (f (suc n) (step x)) ≡ f n x)) →
    (x : Colimitᴱ P step) → Q x
  from (f , [ g ]) = elim λ where
    .∣∣ʳ    → f _
    .∣∣≡∣∣ʳ → g _

  to∘from : ∀ p → to (from p) ≡ p
  to∘from (f , [ g ]) = cong (f ,_) $ []-cong
    [ (⟨ext⟩ λ n → ⟨ext⟩ λ x →
         dcong (elim _) (∣∣≡∣∣ x)  ≡⟨ elim-∣∣≡∣∣ ⟩∎
         g n x                     ∎)
    ]

  from∘to : ∀ h → from (to h) ≡ h
  from∘to h = ⟨ext⟩ $ elim λ where
    .∣∣ʳ    _ → refl _
    .∣∣≡∣∣ʳ x →
      subst (λ z → from (to h) z ≡ h z) (∣∣≡∣∣ x) (refl _)  ≡⟨ subst-in-terms-of-trans-and-dcong ⟩

      trans (sym (dcong (from (to h)) (∣∣≡∣∣ x)))
        (trans (cong (subst Q (∣∣≡∣∣ x)) (refl _))
           (dcong h (∣∣≡∣∣ x)))                             ≡⟨ cong₂ (λ p q → trans (sym p) q)
                                                                 elim-∣∣≡∣∣
                                                                 (trans (cong (flip trans _) $
                                                                         cong-refl _) $
                                                                  trans-reflˡ _) ⟩

      trans (sym (dcong h (∣∣≡∣∣ x))) (dcong h (∣∣≡∣∣ x))   ≡⟨ trans-symˡ _ ⟩∎

      refl _                                                ∎

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module _ where

record Pair (A B : Set) : Set where
  field
    π₁ : A
    π₂ : B

open Pair

foo : {A B : Set} → Pair A B  → Pair A B
foo = λ { x → {!x!} }
{- Case splitting on x produces:
   foo = λ { record { π₁ = π₃ ; π₂ = π₃ } → ? }
   Repeated variables in pattern: π₃
-}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Prelude hiding (id; Bool)

module Implicits.Resolution.Undecidable.Expressiveness where

open import Implicits.Syntax
open import Implicits.Substitutions
open import Extensions.ListFirst

open import Implicits.Resolution.Ambiguous.Resolution as A
open import Implicits.Resolution.Deterministic.Resolution as D
open import Implicits.Resolution.Undecidable.Resolution as I

mutual
  ↓-sound : ∀ {ν} {Δ : ICtx ν} {a r} → Δ D.⊢ r ↓ a → Δ I.⊢ r ↓ a
  ↓-sound (i-simp a) = i-simp a
  ↓-sound (i-iabs x x₁) = i-iabs (≥-deterministic x) (↓-sound x₁)
  ↓-sound (i-tabs b x) = i-tabs b (↓-sound x)

  Δ⟨τ⟩-sound : ∀ {ν} {Δ Δ' : ICtx ν} {a r} → Δ D.⟨ a ⟩= r → Δ' D.⊢ r ↓ a →
              first r ∈ Δ ⇔ (λ r' → Δ' I.⊢ r' ↓ a)
  Δ⟨τ⟩-sound (here p v) y = here (↓-sound y) v
  Δ⟨τ⟩-sound (there x ¬x◁τ p) y = there x (¬◁-¬↓ ¬x◁τ) (Δ⟨τ⟩-sound p y)
    where
      ↓-◁ : ∀ {ν} {Δ : ICtx ν} {a r} → Δ I.⊢ r ↓ a → r ◁ a
      ↓-◁ (i-simp _) = m-simp
      ↓-◁ (i-iabs _ r2↓a) = m-iabs (↓-◁ r2↓a)
      ↓-◁ (i-tabs b r↓a) = m-tabs b (↓-◁ r↓a)

      ¬◁-¬↓ : ∀ {ν} {Δ : ICtx ν} {a r} → ¬ r ◁ a → ¬ Δ I.⊢ r ↓ a
      ¬◁-¬↓ ¬a◁a (i-simp a) = ¬a◁a m-simp
      ¬◁-¬↓ ¬r◁a (i-iabs ⊢ᵣr₁ r₂↓a) = ¬r◁a (m-iabs (↓-◁ r₂↓a))
      ¬◁-¬↓ ¬r◁a (i-tabs b r[/]↓a) = ¬r◁a (m-tabs b (↓-◁ r[/]↓a))

  ≥-deterministic : ∀ {ν} {Δ : ICtx ν} {a} → Δ D.⊢ᵣ a → Δ I.⊢ᵣ a
  ≥-deterministic (r-simp {τ = a} Δ⟨a⟩=r r↓a) = r-simp (Δ⟨τ⟩-sound Δ⟨a⟩=r r↓a)
  ≥-deterministic (r-iabs ρ₁ x) = r-iabs ρ₁ (≥-deterministic x)
  ≥-deterministic (r-tabs x) = r-tabs (≥-deterministic x)


text:
{-# OPTIONS --cubical --safe #-}

module Hyper where

open import Prelude hiding (⊥)
open import Data.Empty.UniversePolymorphic
open import Data.List using (List; _∷_; [])
open import Data.Vec.Iterated
open import Data.Nat using (_*_; _+_)
open import Data.Nat.Properties using (Even; Odd)

private
  variable n m : ℕ

infixr 4 _#_↬_
_#_↬_ : ℕ → Type a → Type b → Type (a ℓ⊔ b)
zero  # A ↬ B = ⊥
suc n # A ↬ B = n # B ↬ A → B

module _ {a b} {A : Type a} {B : Type b} where
  yfld : Vec B n → 1 + (n * 2) # List (A × B) ↬ (A → List (A × B))
  yfld =
    foldr
      (λ n → 1 + (n * 2) # List (A × B) ↬ (A → List (A × B)))
      (λ y yk xk x → (x , y) ∷ xk yk)
      (λ ())

  xfld : Vec A n → (1 + n) * 2 # (A → List (A × B)) ↬ List (A × B)
  xfld =
    foldr
      (λ n → (1 + n) * 2 # (A → List (A × B)) ↬ List (A × B))
      (λ x xk yk → yk xk x)
      (λ _ → [])

  zip : Vec A n → Vec B n → List (A × B)
  zip xs ys = xfld xs (yfld ys)

cata : Even n → (((C → A) → B) → C) → n # A ↬ B → C
cata {n = suc (suc n)} e ϕ h = ϕ (λ g → h (g ∘ cata e ϕ))

push : (A → B) → n # A ↬ B → 2 + n # A ↬ B
push {n = suc n} f q k = f (k q)

one : Odd n → n # A ↬ A
one {n = suc zero} o ()
one {n = suc (suc n)} o k = k (one o)

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
open import Agda.Builtin.Char
open import Agda.Builtin.List
open import Agda.Builtin.Equality
open import Agda.Builtin.String
open import Agda.Builtin.String.Properties

data ⊥ : Set where

∷⁻¹ : ∀ {A : Set} {x y : A} {xs ys} → x ∷ xs ≡ y ∷ ys → x ≡ y
∷⁻¹ refl = refl

xD800 = primNatToChar 0xD800
xD801 = primNatToChar 0xD801

legit : '\xD800' ∷ [] ≡ '\xD801' ∷ []
legit = primStringFromListInjective _ _ refl

actually : xD800 ≡ xD801
actually = refl

nope : xD800 ≡ xD801 → ⊥
nope ()

boom : ⊥
boom = nope (∷⁻¹ legit)

errorAlsoInLHS : Char → String
errorAlsoInLHS '\xD8AA' = "bad"
errorAlsoInLHS _        = "meh"

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
module CTL.Modalities.AN where

open import FStream.Core
open import Library

-- Always (in) Next : p ⊧ φ ⇔ p[1] ⊧ φ
AN' : ∀ {ℓ₁ ℓ₂} {C : Container ℓ₁}
    → FStream' C (Set ℓ₂) → Set (ℓ₁ ⊔ ℓ₂)
AN' props = APred head (inF (tail props))

AN : ∀ {ℓ₁ ℓ₂} {C : Container ℓ₁}
   → FStream C (Set ℓ₂) → Set (ℓ₁ ⊔ ℓ₂)
AN props = APred AN' (inF props)

mutual
  AN'ₛ : ∀ {i} {ℓ₁ ℓ₂} {C : Container ℓ₁}
       → FStream' C (Set ℓ₂) → FStream' {i} C (Set (ℓ₁ ⊔ ℓ₂))
  head (AN'ₛ props) = AN' props
  tail (AN'ₛ props) = ANₛ (tail props)

  ANₛ : ∀ {i} {ℓ₁ ℓ₂} {C : Container ℓ₁}
      → FStream C (Set ℓ₂) → FStream {i} C (Set (ℓ₁ ⊔ ℓ₂))
  inF (ANₛ props) = fmap AN'ₛ (inF props)

max_stars_repo_name: Aerate/condatis

max_issues_repo_name: zimbatm/condatis

max_forks_repo_name: zimbatm/condatis


text:
{-# OPTIONS --without-K --exact-split --safe #-}

module Fragment.Algebra.Signature where

open import Data.Nat using (ℕ)

record Signature : Set₁ where
  field
    ops : ℕ → Set

open Signature public

data ExtendedOp (Σ : Signature) (O : ℕ → Set) : ℕ → Set where
  newₒ : ∀ {n} → O n → ExtendedOp Σ O n
  oldₒ : ∀ {n} → ops Σ n → ExtendedOp Σ O n

_⦅_⦆ : (Σ : Signature) → (ℕ → Set) → Signature
Σ ⦅ O ⦆ = record { ops = ExtendedOp Σ O }

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
-- Andreas, 2017-08-10, issue #2664, reported by csetzer
-- Test case by Ulf

-- {-# OPTIONS -v tc.rec:40 #-}
-- {-# OPTIONS -v tc.cc:60 #-}

open import Agda.Builtin.IO
open import Agda.Builtin.String
open import Agda.Builtin.Unit
open import Agda.Builtin.Nat

mutual
  -- Error WAS:
  -- The presence of mutual affected the compilation of the projections
  -- since it triggered a record pattern translation for them.

  record R : Set where
    constructor mkR
    field
      dummy : Nat
      str : String

helloWorld : R
helloWorld = mkR 0 "Hello World!"

postulate
  putStrLn : String → IO ⊤

{-# FOREIGN GHC import qualified Data.Text.IO as Text #-}
{-# COMPILE GHC putStrLn = Text.putStrLn #-}
{-# COMPILE JS  putStrLn = function(x) { return function(cb) { process.stdout.write(x + "\n"); cb(0); }; } #-}

{-# FOREIGN OCaml
  let printEndline y world = Lwt.return (print_endline y)
#-}
{-# COMPILE OCaml putStrLn = printEndline #-}

main : IO ⊤
main = putStrLn (R.str helloWorld)

-- Expected: Should print
--
--   Hello World!

max_stars_repo_name: xekoukou/agda-ocaml

max_issues_repo_name: xekoukou/agda-ocaml

max_forks_repo_name: xekoukou/agda-ocaml


text:
module OList {A : Set}(_≤_ : A → A → Set) where

open import Data.List
open import Bound.Lower A
open import Bound.Lower.Order _≤_

data OList : Bound → Set where
  onil : {b : Bound}
                   → OList b
  :< : {b : Bound}{x : A}
                   → LeB b (val x)
                   → OList (val x)
                   → OList b

forget : {b : Bound} → OList b → List A
forget onil = []
forget ( :< {x = x} _  xs) = x ∷ forget xs

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
------------------------------------------------------------------------
-- Formalisation of subtyping for recursive types
--
-- Nils Anders Danielsson
------------------------------------------------------------------------

-- This formalisation is explained in "Subtyping, Declaratively—An
-- Exercise in Mixed Induction and Coinduction" (coauthored with
-- Thorsten Altenkirch). The code is partly based on "Coinductive
-- Axiomatization of Recursive Type Equality and Subtyping" by Michael
-- Brandt and Fritz Henglein.

module RecursiveTypes where

-- Recursive types and potentially infinite trees.

import RecursiveTypes.Syntax

-- Substitutions.

import RecursiveTypes.Substitution

-- The semantics of recursive types, defined in terms of the trees
-- that you get when unfolding them.

import RecursiveTypes.Semantics

-- The definition of subtyping which, in my eyes, is the most obvious.
-- Some people may dislike coinductive definitions, though.

import RecursiveTypes.Subtyping.Semantic.Coinductive

-- An example.

import RecursiveTypes.Subtyping.Example

-- Another definition of subtyping, this time in terms of finite
-- approximations. According to Brandt and Henglein this definition is
-- due to Amadio and Cardelli.

import RecursiveTypes.Subtyping.Semantic.Inductive

-- The two semantical definitions of subtyping above can easily be
-- proved equivalent.

import RecursiveTypes.Subtyping.Semantic.Equivalence

-- An axiomatisation of subtyping which is inspired by Brandt and
-- Henglein's. The main difference is that their axiomatisation is
-- inductive, using explicit hypotheses to get a coinductive flavour,
-- whereas mine is mixed inductive/coinductive, using no explicit
-- hypotheses. The axiomatisation is proved equivalent to the
-- coinductive semantic definition of subtyping. The proof is a lot
-- simpler than Brandt and Henglein's, but their proof includes a
-- decision procedure for subtyping.

import RecursiveTypes.Subtyping.Axiomatic.Coinductive

-- Brandt and Henglein's axiomatisation, plus some proofs:
-- • A proof showing that the axiomatisation is sound with respect to
--   the ones above. The soundness proof is different from the one
--   given by Brandt and Henglein: it is cyclic (but productive).
-- • Proofs of decidability and completeness, based on Brandt and
--   Henglein's algorithm.

import RecursiveTypes.Subtyping.Axiomatic.Inductive

-- Some modules containing supporting code for the proof of
-- decidability, including Brandt and Henglein's subterm relation.

import RecursiveTypes.Subterm
import RecursiveTypes.Subterm.RestrictedHypothesis
import RecursiveTypes.Syntax.UnfoldedOrFixpoint

-- An incorrect "subtyping" relation which illustrates the fact that
-- taking the transitive closure of a coinductively defined relation
-- is not in general equivalent to adding an inductive transitivity
-- constructor to it.

import RecursiveTypes.Subtyping.Axiomatic.Incorrect

-- Finally some code which is not directly related to subtyping or
-- recursive types: an example which shows that, in a coinductive
-- setting, it is not always sound to postulate admissible rules
-- (inductively).

import AdmissibleButNotPostulable

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
{-# OPTIONS --prop --rewriting #-}

module Examples.Sorting.Parallel.Comparable where

open import Calf.CostMonoid
open import Calf.CostMonoids

parCostMonoid = ℕ²-ParCostMonoid
costMonoid = ParCostMonoid.costMonoid parCostMonoid

open import Data.Nat using (ℕ)
open ParCostMonoid parCostMonoid using (ℂ)
open import Data.Product using (_,_)

fromℕ : ℕ → ℂ
fromℕ n = n , n

open import Examples.Sorting.Comparable costMonoid fromℕ public

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
module Highlighting where

Set-one : Set₂
Set-one = Set₁

record R (A : Set) : Set-one where
  constructor con

  field X : Set

  F : Set → Set → Set
  F A B = B

  field P : F A X → Set

  -- highlighting of non-terminating definition
  Q : F A X → Set
  Q = Q

postulate P : _

open import Highlighting.M using (ℕ) renaming
  ( _+_ to infixl 5 _⊕_
  ; _*_ to infixl 7 _⊗_
  )

data D (A : Set) : Set-one where
  d : let X = D in X A

postulate _+_ _×_ : Set → Set → Set

infixl 4 _×_ _+_
  -- Issue #2140: the operators should be highlighted also in the
  -- fixity declaration.

-- Issue #3120, jump-to-definition for record field tags
-- in record expressions and patterns.

anR : ∀ A → R A
anR A = record { X = A ; P = λ _ → A }

idR : ∀ A → R A → R A
idR A r@record { X = X; P = P } = record r { X = X }

record S (A : Set) : Set where
  field
    X : A

idR' : ∀ A → R A → R A
idR' A r@record { X = X; P = P } = record r { X = X }

open S

bla : ∀{A} → A → S A
bla x .X = x

-- Issue #3825: highlighting of unsolved metas in record{M} expressions

record R₂ (A : Set) : Set where
  field
    impl : {a : A} → A

module M {A : Set} where
  impl : {a : A} → A   -- yellow should not be here
  impl {a} = a

r₂ : ∀{A} → R₂ A
r₂ = record {M}  -- just because there is an unsolved meta here

-- End issue #3825

-- Issue #3855: highlighting of quantity attributes.
-- @0 and @erased should be highlighted as symbols.

idPoly0 : {@0 A : Set} → A → A
idPoly0 x = x

idPolyE : {@erased A : Set} → A → A
idPolyE x = x

-- Issue #3989: Shadowed repeated variables in telescopes should by
-- default /not/ be highlighted.

Issue-3989 : (A A : Set) → Set
Issue-3989 _ A = A

-- Issue #4356.

open import Agda.Builtin.Sigma

Issue-4356₁ : Σ Set (λ _ → Set) → Σ Set (λ _ → Set)
Issue-4356₁ = λ P@(A , B) → P

Issue-4356₂ : Σ Set (λ _ → Set) → Set
Issue-4356₂ = λ (A , B) → A

Issue-4356₃ : Σ Set (λ _ → Set) → Σ Set (λ _ → Set)
Issue-4356₃ P = let Q@(A , B) = P in Q

Issue-4356₄ : Σ Set (λ _ → Set) → Set
Issue-4356₄ P = let (A , B) = P in B

Issue-4356₅ : Σ Set (λ _ → Set) → Σ Set (λ _ → Set)
Issue-4356₅ P@(A , B) = P

Issue-4356₆ : Σ Set (λ _ → Set) → Set
Issue-4356₆ (A , B) = B

-- Issue #4361: Highlighting builtins.

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

{-# BUILTIN NATURAL Nat -#}  -- NATURAL should be highlighted as keyword.

max_stars_repo_name: Soares/agda

max_issues_repo_name: Soares/agda

max_forks_repo_name: Soares/agda


text:
------------------------------------------------------------------------
-- This module proves that the recognisers correspond exactly to
-- decidable predicates of type List Bool → Bool (when the alphabet is
-- Bool)
------------------------------------------------------------------------

-- This result could be generalised to other finite alphabets.

module TotalRecognisers.Simple.ExpressiveStrength where

open import Codata.Musical.Notation
open import Data.Bool
open import Data.Bool.Properties
open import Function.Base
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence
  using (_⇔_; equivalence; module Equivalence)
open import Data.List
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Decidable

import TotalRecognisers.Simple
open TotalRecognisers.Simple Bool _≟_

-- One direction of the correspondence has already been established:
-- For every grammar there is an equivalent decidable predicate.

grammar⇒pred : ∀ {n} (p : P n) →
               ∃ λ (f : List Bool → Bool) → ∀ s → s ∈ p ⇔ T (f s)
grammar⇒pred p =
  ((λ s → ⌊ s ∈? p ⌋) , λ _ → equivalence fromWitness toWitness)

-- For every decidable predicate there is a corresponding grammar.
-- Note that these grammars are all "infinite LL(1)".

pred⇒grammar : (f : List Bool → Bool) →
               ∃ λ (p : P (f [])) → ∀ s → s ∈ p ⇔ T (f s)
pred⇒grammar f =
  (grammar f , λ s → equivalence (sound f) (complete f s))
  where
  accept-if-true : ∀ b → P b
  accept-if-true true  = empty
  accept-if-true false = fail

  grammar : (f : List Bool → Bool) → P (f [])
  grammar f = tok true  · ♯ grammar (f ∘ _∷_ true )
            ∣ tok false · ♯ grammar (f ∘ _∷_ false)
            ∣ accept-if-true (f [])

  accept-if-true-sound :
    ∀ b {s} → s ∈ accept-if-true b → s ≡ [] × T b
  accept-if-true-sound true  empty = (refl , _)
  accept-if-true-sound false ()

  accept-if-true-complete : ∀ {b} → T b → [] ∈ accept-if-true b
  accept-if-true-complete ok with Equivalence.to T-≡ ⟨$⟩ ok
  ... | refl = empty

  sound : ∀ f {s} → s ∈ grammar f → T (f s)
  sound f (∣-right s∈) with accept-if-true-sound (f []) s∈
  ... | (refl , ok) = ok
  sound f (∣-left (∣-left  (tok · s∈))) = sound (f ∘ _∷_ true ) s∈
  sound f (∣-left (∣-right (tok · s∈))) = sound (f ∘ _∷_ false) s∈

  complete : ∀ f s → T (f s) → s ∈ grammar f
  complete f [] ok =
    ∣-right {n₁ = false} $ accept-if-true-complete ok
  complete f (true ∷ bs) ok =
    ∣-left {n₁ = false} $ ∣-left {n₁ = false} $
      tok · complete (f ∘ _∷_ true ) bs ok
  complete f (false ∷ bs) ok =
    ∣-left {n₁ = false} $ ∣-right {n₁ = false} $
      tok · complete (f ∘ _∷_ false) bs ok

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
-- {-# OPTIONS --show-implicit #-}

module Issue89 where

open import Common.Coinduction renaming (∞ to ∞_)

------------------------------------------------------------------------
-- Streams

infixr 5 _≺_

data Stream A : Set where
  _≺_ : (x : A) (xs : ∞ (Stream A)) -> Stream A

head : forall {A} -> Stream A -> A
head (x ≺ xs) = x

tail : forall {A} -> Stream A -> Stream A
tail (x ≺ xs) = ♭ xs

------------------------------------------------------------------------
-- Stream programs

infix  8 _∞
infixr 5 _⋎_
infix  4 ↓_

mutual

  data Stream′ A : Set1 where
    _≺_ : (x : A) (xs : ∞ (StreamProg A)) -> Stream′ A

  data StreamProg (A : Set) : Set1 where
    ↓_  : (xs : Stream′ A) -> StreamProg A
    _∞  : (x : A) -> StreamProg A
    _⋎_ : (xs ys : StreamProg A) -> StreamProg A

head′ : ∀ {A} → Stream′ A → A
head′ (x ≺ xs) = x

tail′ : ∀ {A} → Stream′ A → StreamProg A
tail′ (x ≺ xs) = ♭ xs

P⇒′ : forall {A} -> StreamProg A -> Stream′ A
P⇒′ (↓ xs)    = xs
P⇒′ (x ∞)     = x ≺ ♯ (x ∞)
P⇒′ (xs ⋎ ys) with P⇒′ xs
P⇒′ (xs ⋎ ys) | xs′ = head′ xs′ ≺ ♯ (ys ⋎ tail′ xs′)

mutual

  ′⇒ : forall {A} -> Stream′ A -> Stream A
  ′⇒ (x ≺ xs) = x ≺ ♯ P⇒ (♭ xs)

  P⇒ : forall {A} -> StreamProg A -> Stream A
  P⇒ xs = ′⇒ (P⇒′ xs)

------------------------------------------------------------------------
-- Stream equality

infix 4 _≡_ _≈_ _≊_

data _≡_ {a : Set} (x : a) : a -> Set where
  ≡-refl : x ≡ x

data _≈_ {A} (xs ys : Stream A) : Set where
  _≺_ : (x≡ : head xs ≡ head ys) (xs≈ : ∞ (tail xs ≈ tail ys)) ->
        xs ≈ ys

_≊_ : forall {A} (xs ys : StreamProg A) -> Set
xs ≊ ys = P⇒ xs ≈ P⇒ ys

foo : forall {A} (x : A) -> x ∞ ⋎ x ∞ ≊ x ∞
foo x = ≡-refl ≺ ♯ foo x

-- The first goal has goal type
--   head (′⇒ (x ≺ x ∞ ⋎ x ∞)) ≡ head (′⇒ (x ≺ x ∞)).
-- The normal form of the left-hand side is x, and the normal form of
-- the right-hand side is x (both according to Agda), but ≡-refl is
-- not accepted by the type checker:
--   x != head (′⇒ (P⇒′ (x ∞))) of type .A
--   when checking that the expression ≡-refl has type
--   (head (P⇒ (x ∞ ⋎ x ∞)) ≡ head (P⇒ (x ∞)))

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
import Relation.Binary.Reasoning.Setoid as SetoidR
open import MultiSorted.AlgebraicTheory

import MultiSorted.Interpretation as Interpretation
import MultiSorted.Model as Model
import MultiSorted.UniversalInterpretation as UniversalInterpretation
import MultiSorted.Substitution as Substitution
import MultiSorted.SyntacticCategory as SyntacticCategory

module MultiSorted.UniversalModel
  {ℓt}
  {𝓈 ℴ}
  {Σ : Signature {𝓈} {ℴ}}
  (T : Theory ℓt Σ) where

  open Theory T
  open Substitution T
  open UniversalInterpretation T
  open Interpretation.Interpretation ℐ
  open SyntacticCategory T

  𝒰 : Model.Is-Model T ℐ
  𝒰 =
     record
        { model-eq = λ ε var-var →
                       let open SetoidR (eq-setoid (ax-ctx ε) (sort-of (ctx-slot (ax-sort ε)) var-var)) in
                         begin
                         interp-term (ax-lhs ε) var-var ≈⟨ interp-term-self (ax-lhs ε) var-var ⟩
                         ax-lhs ε ≈⟨ id-action ⟩
                         ax-lhs ε [ id-s ]s ≈⟨ eq-axiom ε id-s ⟩
                         ax-rhs ε [ id-s ]s ≈˘⟨ id-action ⟩
                         ax-rhs ε ≈˘⟨ interp-term-self (ax-rhs ε) var-var ⟩
                         interp-term (ax-rhs ε) var-var ∎
        }

  -- The universal model is universal
  universality : ∀ (ε : Equation Σ) → ⊨ ε → ⊢ ε
  universality ε p =
    let open Equation in
    let open SetoidR (eq-setoid (eq-ctx ε) (eq-sort ε)) in
      (begin
        eq-lhs ε ≈˘⟨ interp-term-self (eq-lhs ε) var-var ⟩
        interp-term (eq-lhs ε) var-var ≈⟨ p var-var ⟩
        interp-term (eq-rhs ε) var-var ≈⟨ interp-term-self (eq-rhs ε) var-var ⟩
        eq-rhs ε ∎)

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
module InstanceArgumentsModNotParameterised where

postulate A : Set
          a : A

record B : Set where
  field bA : A

b : B
b = record {bA = a}

module C = B b

open C {{...}}


text:
{-# OPTIONS --without-K #-}

open import Types

module Functions where

-- Identity functions
id : ∀ {i} (A : Set i) → (A → A)
id A = λ x → x

-- Constant functions
cst : ∀ {i j} {A : Set i} {B : Set j} (b : B) → (A → B)
cst b = λ _ → b

-- Composition of dependent functions
_◯_ : ∀ {i j k} {A : Set i} {B : A → Set j} {C : (a : A) → (B a → Set k)}
  → (g : {a : A} → Π (B a) (C a)) → (f : Π A B) → Π A (λ a → C a (f a))
g ◯ f = λ x → g (f x)

-- Application
infixr 0 _$_
_$_ : ∀ {i j} {A : Set i} {B : A → Set j} → (∀ x → B x) → (∀ x → B x)
f $ x = f x

-- Curry! Can't live without it!
curry : ∀ {i j k} {A : Set i} {B : A → Set j} {C : Σ A B → Set k}
  → (∀ s → C s) → (∀ x y → C (x , y))
curry f x y = f (x , y)

uncurry : ∀ {i j k} {A : Set i} {B : A → Set j} {C : ∀ x → B x → Set k}
  → (∀ x y → C x y) → (∀ s → C (π₁ s) (π₂ s))
uncurry f (x , y) = f x y

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module Peano where
  open import IPL

  data ℕ : Set where
    zero : ℕ -- Axiom 2.1. 0 is a natural number
    _++ : ℕ → ℕ -- Axiom 2.2. If n is a natural number, then n++ is also a natural number

  data _≡_ : ℕ → ℕ → Set where
    refl : {a : ℕ} → a ≡ a

  axiom23 : {n : ℕ} → ¬ (zero ≡ (n ++))
  axiom23 = λ ()

  axiom24 : {n m : ℕ} → (n ++) ≡ (m ++) → n ≡ m
  axiom24 refl = refl

  _+_ : ℕ → ℕ → ℕ -- Definition 2.2.1
  zero + m = m
  (n ++) + m = (n + m) ++

  ≡-sec : {n m : ℕ} → n ≡ m → (n ++) ≡ (m ++)
  ≡-sec refl = refl

  ≡-comm : {n m : ℕ} → n ≡ m → m ≡ n
  ≡-comm refl = refl

  ≡-trans : {n m p : ℕ} → n ≡ m → m ≡ p → n ≡ p
  ≡-trans refl refl = refl

  lemma222 : (n : ℕ) → (n + zero) ≡ n
  lemma222 zero = refl
  lemma222 (n ++) = ≡-sec (lemma222 n)

  lemma223 : (n m : ℕ) → (n + (m ++)) ≡ ((n + m) ++)
  lemma223 zero m = refl
  lemma223 (n ++) m = ≡-sec (lemma223 n m)

  -- Addition is commutative
  prop224 : (n m : ℕ) → (n + m) ≡ (m + n)
  prop224 zero m = ≡-comm (lemma222 m)
  prop224 (n ++) m = ≡-trans (≡-sec (prop224 n m)) (≡-comm (lemma223 m n))

  -- Addition is associative
  prop225 : (a b c : ℕ) → ((a + b) + c) ≡ (a + (b + c))
  prop225 zero b c = refl
  prop225 (a ++) b c = ≡-sec (prop225 a b c)

  -- Cancellation law
  prop226 : (a b c : ℕ) → (a + b) ≡ (a + c) → b ≡ c
  prop226 zero b c = λ z → z
  prop226 (a ++) b c = λ z → (prop226 a b c) (axiom24 z)


text:
{-# OPTIONS --without-K #-}
open import Type
open import Data.Bits    using (Bits)
open import Data.Bit     using (Bit)
open import Data.Zero   using (𝟘)
open import Data.Fin     using (Fin)
open import Data.Maybe   using (Maybe)
open import Data.Nat     using (ℕ)
open import Data.Product using (Σ; _×_)
open import Data.Sum     using (_⊎_)
open import Data.One    using (𝟙)
open import Data.Vec     using (Vec)

module Explore.Syntax where

-- this is to be imported from the appropriate module
postulate
  S : ★₀ → ★₀
  S𝟙 : S 𝟙
  SBit : S Bit
  SFin : ∀ n → S (Fin n)
  SBits : ∀ n → S (Bits n)
  SVec : ∀ {A} → S A → ∀ n → S (Vec A n)
  _S×_ : ∀ {A B} → S A → S B → S (A × B)
  _S⊎_ : ∀ {A B} → S A → S B → S (A ⊎ B)
  SMaybe : ∀ {A} → S A → S (Maybe A)
  SΣ : ∀ {A} {B : A → _} → S A → (∀ x → S (B x)) → S (Σ A B)
  S𝟙→ : ∀ {A} → S A → S (𝟙 → A)
  SBit→ : ∀ {A} → S A → S (Bit → A)
  S𝟘→ : ∀ A → S (𝟘 → A)
  S×→ : ∀ {A B C} → S (A → B → C) → S (A × B → C)
  S⟨_⊎_⟩→ : ∀ {A B C} → S (A → C) → S (B → C) → S (A ⊎ B → C)

module Fin-universe where

    `★ : ★₀
    `★ = ℕ

    -- decoding
    El : `★ → ★₀
    El = Fin

    `S : ∀ `A → S (El `A)
    `S = SFin

module Bits-universe where

    `★ : ★₀
    `★ = ℕ

    -- decoding
    El : `★ → ★₀
    El = Bits

    `S : ∀ `A → S (El `A)
    `S = SBits

module ⊎×-universe where

    data `★ : ★₀ where
      `𝟙 : `★
      _`×_ _`⊎_ : `★ → `★ → `★

    -- decoding
    El : `★ → ★₀
    El `𝟙 = 𝟙
    El (s `× t) = El s × El t
    El (s `⊎ t) = El s ⊎ El t

    `S : ∀ `A → S (El `A)
    `S `𝟙       = S𝟙
    `S (s `× t) = `S s S× `S t
    `S (s `⊎ t) = `S s S⊎ `S t

module 𝟙-Maybe-universe where

    data `★ : ★₀ where
      -- one element
      `𝟙     : `★
      -- one element more
      `Maybe : `★ → `★

    -- decoding
    El : `★ → ★₀
    El `𝟙 = 𝟙
    El (`Maybe t) = Maybe (El t)

    `S : ∀ `A → S (El `A)
    `S `𝟙 = S𝟙
    `S (`Maybe t) = SMaybe (`S t)

module ΣBit-universe where

    data `★ : ★₀
    El : `★ → ★₀

    data `★ where
      `Bit : `★
      `Σ   : (s : `★) → (El s → `★) → `★

    -- decoding
    El `Bit     = Bit
    El (`Σ s t) = Σ (El s) λ x → El (t x)

    `S : ∀ `A → S (El `A)
    `S `Bit = SBit
    `S (`Σ s t) = SΣ (`S s) λ x → `S (t x)

module ⊎×→-universe where

    -- Types appearing on the left of an arrow
    data `★⁻ : ★₀ where
      -- zero and elements
      `𝟘 `𝟙 : `★⁻

      -- products and co-products
      _`×_ _`⊎_ : `★⁻ → `★⁻ → `★⁻

    -- decoding of negative types
    El⁻ : `★⁻ → ★₀
    El⁻ `𝟘 = 𝟘
    El⁻ `𝟙 = 𝟙
    El⁻ (s `× t) = El⁻ s × El⁻ t
    El⁻ (s `⊎ t) = El⁻ s ⊎ El⁻ t

    `S⟨_⟩→_ : ∀ `A {B} (sB : S B) → S (El⁻ `A → B)
    `S⟨ `𝟘 ⟩→ t = S𝟘→ _
    `S⟨ `𝟙 ⟩→ t = S𝟙→ t
    `S⟨ s `× t ⟩→ u = S×→ (`S⟨ s ⟩→ `S⟨ t ⟩→ u)
    `S⟨ s `⊎ t ⟩→ u = S⟨ `S⟨ s ⟩→ u ⊎ `S⟨ t ⟩→ u ⟩→

    data `★ : ★₀ where
      -- one element
      `𝟙     : `★

      -- products and co-products
      _`×_ _`⊎_ : `★ → `★ → `★

      -- functions
      _`→_ : `★⁻ → `★ → `★

    -- decoding of positive types
    El : `★ → ★₀
    El `𝟙 = 𝟙
    El (s `× t) = El s × El t
    El (s `⊎ t) = El s ⊎ El t
    El (s `→ t) = El⁻ s → El t

    `S : ∀ `A → S (El `A)
    `S `𝟙 = S𝟙
    `S (s `× t) = `S s S× `S t
    `S (s `⊎ t) = `S s S⊎ `S t
    `S (s `→ t) = `S⟨ s ⟩→ `S t

module Σ⊎×→-universe where

    -- Types appearing on the left of an arrow
    data `★⁻ : ★₀ where
      -- zero, one, and two elements
      `𝟘 `𝟙 `Bit : `★⁻

      -- products and co-products
      _`×_ _`⊎_ : `★⁻ → `★⁻ → `★⁻

      -- Σ?

    -- decoding of negative types
    El⁻ : `★⁻ → ★₀
    El⁻ `𝟘 = 𝟘
    El⁻ `𝟙 = 𝟙
    El⁻ `Bit = Bit
    El⁻ (s `× t) = El⁻ s × El⁻ t
    El⁻ (s `⊎ t) = El⁻ s ⊎ El⁻ t

    `S⟨_⟩→_ : ∀ `A {B} (sB : S B) → S (El⁻ `A → B)
    `S⟨ `𝟘 ⟩→ t = S𝟘→ _
    `S⟨ `𝟙 ⟩→ t = S𝟙→ t
    `S⟨ `Bit ⟩→ t = SBit→ t
    `S⟨ s `× t ⟩→ u = S×→ (`S⟨ s ⟩→ `S⟨ t ⟩→ u)
    `S⟨ s `⊎ t ⟩→ u = S⟨ `S⟨ s ⟩→ u ⊎ `S⟨ t ⟩→ u ⟩→

    data `★ : ★₀
    El : `★ → ★₀

    data `★ where
      -- one and two elements
      `𝟙 `Bit : `★

      -- 'n' elements
      `Fin : ℕ → `★

      -- one element more
      `Maybe : `★ → `★

      -- products and co-products
      _`×_ _`⊎_ : `★ → `★ → `★

      -- dependent pairs
      `Σ   : (s : `★) → (El s → `★) → `★

      -- vectors
      `Vec : `★ → ℕ → `★

      -- functions
      _`→_ : `★⁻ → `★ → `★

    -- decoding of positive types
    El `𝟙 = 𝟙
    El `Bit = Bit
    El (`Fin n) = Fin n
    El (`Maybe t) = Maybe (El t)
    El (s `× t) = El s × El t
    El (s `⊎ t) = El s ⊎ El t
    El (`Σ s t) = Σ (El s) λ x → El (t x)
    El (s `→ t) = El⁻ s → El t
    El (`Vec t n) = Vec (El t) n

    `Bits = `Vec `Bit

    `S : ∀ `A → S (El `A)
    `S `𝟙 = S𝟙
    `S `Bit = SBit
    `S (`Fin n) = SFin n
    `S (`Maybe `A) = SMaybe (`S `A)
    `S (`A `× `B) = `S `A S× `S `B
    `S (`A `⊎ `B) = `S `A S⊎ `S `B
    `S (`Σ `A `B) = SΣ (`S `A) λ x → `S (`B x)
    `S (`Vec `A n) = SVec (`S `A) n
    `S (`A `→ `B) = `S⟨ `A ⟩→ `S `B

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
{-# OPTIONS --no-termination-check #-}

module Pi-abstract-machine where

open import Data.Empty
open import Data.Unit
open import Data.Sum hiding (map)
open import Data.Product hiding (map)

infixr 30 _⟷_
infixr 30 _⟺_
infixr 20 _◎_

------------------------------------------------------------------------------
-- A universe of our value types

data B : Set where
  ZERO  : B
  ONE   : B
  PLUS  : B → B → B
  TIMES : B → B → B

data VB : (b : B) → Set where
  unitB : VB ONE
  inlB  : {b₁ b₂ : B} → VB b₁ → VB (PLUS b₁ b₂)
  inrB  : {b₁ b₂ : B} → VB b₂ → VB (PLUS b₁ b₂)
  pairB : {b₁ b₂ : B} → VB b₁ → VB b₂ → VB (TIMES b₁ b₂)

------------------------------------------------------------------------------
-- Primitive isomorphisms

data _⟷_ : B → B → Set where
  -- (+,0) commutative monoid
  unite₊  : { b : B } → PLUS ZERO b ⟷ b
  uniti₊  : { b : B } → b ⟷ PLUS ZERO b
  swap₊   : { b₁ b₂ : B } → PLUS b₁ b₂ ⟷ PLUS b₂ b₁
  assocl₊ : { b₁ b₂ b₃ : B } → PLUS b₁ (PLUS b₂ b₃) ⟷ PLUS (PLUS b₁ b₂) b₃
  assocr₊ : { b₁ b₂ b₃ : B } → PLUS (PLUS b₁ b₂) b₃ ⟷ PLUS b₁ (PLUS b₂ b₃)
  -- (*,1) commutative monoid
  unite⋆  : { b : B } → TIMES ONE b ⟷ b
  uniti⋆  : { b : B } → b ⟷ TIMES ONE b
  swap⋆   : { b₁ b₂ : B } → TIMES b₁ b₂ ⟷ TIMES b₂ b₁
  assocl⋆ : { b₁ b₂ b₃ : B } → TIMES b₁ (TIMES b₂ b₃) ⟷ TIMES (TIMES b₁ b₂) b₃
  assocr⋆ : { b₁ b₂ b₃ : B } → TIMES (TIMES b₁ b₂) b₃ ⟷ TIMES b₁ (TIMES b₂ b₃)
  -- * distributes over +
  dist    : { b₁ b₂ b₃ : B } →
            TIMES (PLUS b₁ b₂) b₃ ⟷ PLUS (TIMES b₁ b₃) (TIMES b₂ b₃)
  factor  : { b₁ b₂ b₃ : B } →
            PLUS (TIMES b₁ b₃) (TIMES b₂ b₃) ⟷ TIMES (PLUS b₁ b₂) b₃
  -- id
  id⟷   : { b : B } → b ⟷ b

adjointP : { b₁ b₂ : B } → (b₁ ⟷ b₂) → (b₂ ⟷ b₁)
adjointP unite₊    = uniti₊
adjointP uniti₊    = unite₊
adjointP swap₊     = swap₊
adjointP assocl₊   = assocr₊
adjointP assocr₊   = assocl₊
adjointP unite⋆    = uniti⋆
adjointP uniti⋆    = unite⋆
adjointP swap⋆     = swap⋆
adjointP assocl⋆   = assocr⋆
adjointP assocr⋆   = assocl⋆
adjointP dist      = factor
adjointP factor    = dist
adjointP id⟷      = id⟷

evalP : { b₁ b₂ : B } → (b₁ ⟷ b₂) → VB b₁ → VB b₂
evalP unite₊ (inlB ())
evalP unite₊ (inrB v) = v
evalP uniti₊ v = inrB v
evalP swap₊ (inlB v) = inrB v
evalP swap₊ (inrB v) = inlB v
evalP assocl₊ (inlB v) = inlB (inlB v)
evalP assocl₊ (inrB (inlB v)) = inlB (inrB v)
evalP assocl₊ (inrB (inrB v)) = inrB v
evalP assocr₊ (inlB (inlB v)) = inlB v
evalP assocr₊ (inlB (inrB v)) = inrB (inlB v)
evalP assocr₊ (inrB v) = inrB (inrB v)
evalP unite⋆ (pairB unitB v) = v
evalP uniti⋆ v = (pairB unitB v)
evalP swap⋆ (pairB v₁ v₂) = pairB v₂ v₁
evalP assocl⋆ (pairB v₁ (pairB v₂ v₃)) = pairB (pairB v₁ v₂) v₃
evalP assocr⋆ (pairB (pairB v₁ v₂) v₃) = pairB v₁ (pairB v₂ v₃)
evalP dist (pairB (inlB v₁) v₃) = inlB (pairB v₁ v₃)
evalP dist (pairB (inrB v₂) v₃) = inrB (pairB v₂ v₃)
evalP factor (inlB (pairB v₁ v₃)) = pairB (inlB v₁) v₃
evalP factor (inrB (pairB v₂ v₃)) = pairB (inrB v₂) v₃
evalP id⟷ v = v

-- Backwards evaluator

bevalP : { b₁ b₂ : B } → (b₁ ⟷ b₂) → VB b₂ → VB b₁
bevalP c v = evalP (adjointP c) v

------------------------------------------------------------------------------
-- Closure combinators

data _⟺_ : B → B → Set where
  iso : { b₁ b₂ : B } → (b₁ ⟷ b₂) → (b₁ ⟺ b₂)
  sym : { b₁ b₂ : B } → (b₁ ⟺ b₂) → (b₂ ⟺ b₁)
  _◎_ : { b₁ b₂ b₃ : B } → (b₁ ⟺ b₂) → (b₂ ⟺ b₃) → (b₁ ⟺ b₃)
  _⊕_ : { b₁ b₂ b₃ b₄ : B } → (b₁ ⟺ b₃) → (b₂ ⟺ b₄) → (PLUS b₁ b₂ ⟺ PLUS b₃ b₄)
  _⊗_ : { b₁ b₂ b₃ b₄ : B } → (b₁ ⟺ b₃) → (b₂ ⟺ b₄) → (TIMES b₁ b₂ ⟺ TIMES b₃ b₄)

--

adjoint : { b₁ b₂ : B } → (b₁ ⟺ b₂) → (b₂ ⟺ b₁)
adjoint (iso c) = iso (adjointP c)
adjoint (sym c) = c
adjoint (c₁ ◎ c₂) = adjoint c₂ ◎ adjoint c₁
adjoint (c₁ ⊕ c₂) = adjoint c₁ ⊕ adjoint c₂
adjoint (c₁ ⊗ c₂) = adjoint c₁ ⊗ adjoint c₂

------------------------------------------------------------------------------
-- Operational semantics

-- (Context a b c d) represents a combinator (c <=> d) with a hole
-- requiring something of type (a <=> b). When we use these contexts,
-- it is always the case that the (c <=> a) part of the computation
-- has ALREADY been done and that we are about to evaluate (a <=> b)
-- using a given 'a'. The continuation takes the output 'b' and
-- produces a 'd'.

data Context : B → B → B → B → Set where
  emptyC : {a b : B} → Context a b a b
  seqC₁ : {a b c i o : B} → (b ⟺ c) → Context a c i o → Context a b i o
  seqC₂ : {a b c i o : B} → (a ⟺ b) → Context a c i o → Context b c i o
  leftC : {a b c d i o : B} →
          (c ⟺ d) → Context (PLUS a c) (PLUS b d) i o → Context a b i o
  rightC : {a b c d i o : B} →
           (a ⟺ b) → Context (PLUS a c) (PLUS b d) i o → Context c d i o
  -- the (i <-> a) part of the computation is completely done; so we must store
  -- the value of type [[ c ]] as part of the context
  fstC : {a b c d i o : B} →
         VB c → (c ⟺ d) → Context (TIMES a c) (TIMES b d) i o → Context a b i o
  -- the (i <-> c) part of the computation and the (a <-> b) part of
  -- the computation are completely done; so we must store the value
  -- of type [[ b ]] as part of the context
  sndC : {a b c d i o : B} →
         (a ⟺ b) → VB b → Context (TIMES a c) (TIMES b d) i o → Context c d i o

-- Small-step evaluation

-- A computation (c <=> d) is split into:
--   - a history (c <==> a)
--   - a current computation in focus (a <==> b)
--   - a future (b <==> d)

record BState (a b c d : B) : Set where
  constructor <_!_!_>
  field
    comb : a ⟺ b
    val : VB a
    context :  Context a b c d

record AState (a b c d : B) : Set where
  constructor [_!_!_]
  field
    comb : a ⟺ b
    val : VB b
    context : Context a b c d

data State (d : B) : Set where
  before : {a b c : B} → BState a b c d → State d
  after : {a b c : B} → AState a b c d → State d
  final : VB d → State d

-- The (c <=> a) part of the computation has been done.
-- We are about to perform the (a <=> b) part of the computation.
beforeStep : {a b c d : B} → BState a b c d → State d
beforeStep < iso f ! v ! C > = after [ iso f ! (evalP f v) ! C ]
beforeStep < sym c ! v ! C > = before < adjoint c ! v ! C >
beforeStep < _◎_ {b₂ = _} f g ! v ! C > = before < f ! v ! seqC₁ g C >
beforeStep < _⊕_ {b₁} {b₂} {b₃} {b₄} f g ! inlB v ! C > = before < f ! v ! leftC g C >
beforeStep < _⊕_ {b₁} {b₂} {b₃} {b₄} f g ! inrB v ! C > = before < g ! v ! rightC f C >
beforeStep < _⊗_ f g ! (pairB v₁ v₂ ) ! C > = before < f ! v₁ ! fstC v₂ g C >

-- The (c <=> a) part of the computation has been done.
-- The (a <=> b) part of the computation has been done.
-- We need to examine the context to get the 'd'.
-- We rebuild the combinator on the way out.
afterStep : {a b c d : B} → AState a b c d → State d
afterStep {d = d} [ f ! v ! emptyC ] = final v
afterStep [ f ! v ! seqC₁ g C ] = before <  g ! v ! seqC₂ f C >
afterStep [ g ! v ! seqC₂ f C ] = after [ f ◎ g ! v ! C ]
afterStep [ f ! v ! leftC g C ] = after [ f ⊕ g ! inlB v ! C ]
afterStep [ g ! v ! rightC f C ] = after [ f ⊕ g ! inrB v ! C ]
afterStep [ f ! v₁ ! fstC v₂ g C ] = before < g ! v₂ ! sndC f v₁ C >
afterStep [ g ! v₂ ! sndC f v₁ C ] = after [ f ⊗ g ! (pairB v₁ v₂) ! C ]

-- Backwards evaluator
-- Re-use AState and BState, but use them 'backwards'

-- this one is different as it produces a 'c' rather than a 'd'
data Stateb (c : B) : Set where
  before : {a b d : B} → AState a b c d → Stateb c
  after : {a b d : B} → BState a b c d → Stateb c
  final : VB c → Stateb c

-- The (d <=> b) part of the computation has been done.
-- We have a 'b' and we are about to do the (a <=> b) computation backwards.
-- We get an 'a' and examine the context to get the 'c'

beforeStepb : { a b c d : B } → AState a b c d → Stateb c
beforeStepb [ iso f ! v ! C ] = after < iso f ! bevalP f v ! C >
beforeStepb [ sym c ! v ! C ] = before [ adjoint c ! v ! C ]
beforeStepb [ f ◎ g ! v ! C ] = before [ g ! v ! seqC₂ f C ]
beforeStepb [ f ⊕ g ! inlB v ! C ] = before [ f ! v ! leftC g C ]
beforeStepb [ f ⊕ g ! inrB v ! C ] = before [ g ! v ! rightC f C ]
beforeStepb [ f ⊗ g ! pairB v₁ v₂ ! C ] = before [ g ! v₂ ! sndC f v₁ C ]

-- The (d <-> b) part of the computation has been done.
-- The (a <-> b) backwards computation has been done.
-- We have an 'a' and examine the context to get the 'c'

afterStepb : { a b c d : B } → BState a b c d → Stateb c
afterStepb < f ! v ! emptyC > = final v
afterStepb < g ! v ! seqC₂ f C > = before [ f ! v ! seqC₁ g C ]
afterStepb < f ! v ! seqC₁ g C > = after < f ◎ g ! v ! C >
afterStepb < f ! v ! leftC g C > = after < f ⊕ g ! inlB v ! C >
afterStepb < g ! v ! rightC f C > = after < f ⊕ g ! inrB v ! C >
afterStepb < g ! v₂ ! sndC f v₁ C > = before [ f ! v₁ ! fstC v₂ g C ]
afterStepb < f ! v₁ ! fstC v₂ g C > = after < f ⊗ g ! pairB v₁ v₂ ! C >

------------------------------------------------------------------------------
-- A single step of a machine

step : {d : B} → State d → State d
step (before st) = beforeStep st
step (after st) = afterStep st
step (final v) = final v

stepb : {c : B} → Stateb c → Stateb c
stepb (before st) = beforeStepb st
stepb (after st) = afterStepb st
stepb (final v) = final v

-- Forward and backwards evaluators loop until final state

eval : {a b : B} → (a ⟺ b) → VB a → VB b
eval f v = loop (before < f ! v ! emptyC > )
  where
    loop : {b : B} → State b  → VB b
    loop (final v) = v
    loop st = loop (step st)

evalb : {a b : B} → (a ⟺ b) → VB b → VB a
evalb f v = loop (before [ f ! v ! emptyC ] )
  where
    loop : {b : B} → Stateb b  → VB b
    loop (final v) = v
    loop st = loop (stepb st)

------------------------------------------------------------------------------

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
------------------------------------------------------------------------------
-- Well-founded induction on the lexicographic order on natural numbers
------------------------------------------------------------------------------

{-# OPTIONS --allow-unsolved-metas     #-}
{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

-- From the thesis: The induction principle $\Conid{Lexi-wfind}$ is
-- proved by well-founded induction on the usual order $\Conid{LT}$ on
-- (partial) natural numbers which, in turn, can be proved by pattern
-- matching on the proof that the numbers are total.

module FOT.FOTC.Data.Nat.Induction.NonAcc.LexicographicI where

open import FOTC.Base
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.EliminationPropertiesI
open import FOTC.Data.Nat.Inequalities.PropertiesI

open import FOTC.Data.Nat.Induction.NonAcc.WF-I
open module WFI = FOTC.Data.Nat.Induction.NonAcc.WF-I.WFInd

open import FOTC.Data.Nat.Type

------------------------------------------------------------------------------

Lexi-wfind :
  (A : D → D → Set) →
  (∀ {m₁ n₁} → N m₁ → N n₁ →
     (∀ {m₂ n₂} → N m₂ → N n₂ → Lexi m₂ n₂ m₁ n₁ → A m₂ n₂) → A m₁ n₁) →
  ∀ {m n} → N m → N n → A m n
Lexi-wfind A h {m} Nm Nn = <-wfind {!!} {!!} {!!}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --without-K #-}

module Circuits where

open import PiLevel0
  using (U; ZERO; ONE; PLUS; TIMES; BOOL; BOOL²;
         _⟷_;
        unite₊; uniti₊; swap₊; assocl₊; assocr₊;
        unite⋆; uniti⋆; swap⋆; assocl⋆; assocr⋆;
        absorbr; absorbl; factorzr; factorzl; dist; factor;
        id⟷; _◎_; _⊕_; _⊗_;
        _⟷⟨_⟩_; _□;
        NOT; CNOT; TOFFOLI)

------------------------------------------------------------------------------

SWAP : BOOL² ⟷ BOOL²
SWAP = swap⋆

CONTROL : {t : U} → (t ⟷ t) → (TIMES BOOL t ⟷ TIMES BOOL t)
CONTROL {t} f = TIMES BOOL t
                  ⟷⟨ id⟷ ⟩
                TIMES (PLUS x y) t
                  ⟷⟨ dist ⟩
                PLUS (TIMES x t) (TIMES y t)
                  ⟷⟨ id⟷ ⊕ (id⟷ ⊗ f) ⟩
                PLUS (TIMES x t) (TIMES y t)
                  ⟷⟨ factor ⟩
                TIMES (PLUS x y) t
                  ⟷⟨ id⟷ ⟩
                TIMES BOOL t □
  where x = ONE; y = ONE

FREDKIN : TIMES BOOL BOOL² ⟷ TIMES BOOL BOOL²
FREDKIN = CONTROL SWAP

------------------------------------------------------------------------------
-- Fig. 4 in http://arxiv.org/pdf/1110.2574v2.pdf

-- (e) cycles

-- (c) reversible truth table

------------------------------------------------------------------------------